(* Lambek calculus *) Add LoadPath "../Light". Require Import Forms. Definition structrules := Form -> Form -> Set. Definition extends (R1 R2 :structrules): Type := forall A B, R1 A B -> R2 A B. Inductive union (R1 R2:structrules):structrules := | union_l : forall A B, R1 A B -> union R1 R2 A B | union_r : forall A B, R2 A B -> union R1 R2 A B. Inductive NL : structrules :=. Inductive L : structrules := L1 : forall A B C, L (A o (B o C)) ((A o B) o C) | L2 : forall A B C, L ((A o B) o C) (A o (B o C)). Inductive P : structrules := P1 : forall A B, P (A o B) (B o A). Definition LP : structrules := union L P. Inductive derives(R: structrules) : Form -> Form -> Set := | one : forall A, derives R A A | comp : forall A B C, derives R A B -> derives R B C -> derives R A C | beta : forall A B C, derives R (A o B) C -> derives R A (C // B) | beta' : forall A B C , derives R A (C // B) -> derives R (A o B) C | gamma : forall A B C, derives R (A o B) C -> derives R B (A \\ C) | gamma' : forall A B C, derives R B (A \\ C) -> derives R (A o B) C | by_rule : forall A B, R A B -> derives R A B. Hint Resolve one comp beta gamma : ctl. Definition structrules_mono : forall R R', extends R R' -> forall A B, derives R A B -> derives R' A B. intros R R' H A B d; elim d. constructor 1. intros; apply comp with B0; auto. intros; apply beta; auto. intros; apply beta'; auto. intros; apply gamma; auto. intros; apply gamma'; auto. intros; apply by_rule ; eauto. Defined. Lemma Dot_mono_left : forall R A B C, derives R A C -> derives R (A o B) ( C o B). intros A B C R H . apply beta'. eapply comp. (* or apply comp with C *) eexact H. auto with ctl. (* another proof *) Restart. intros; apply beta'; eauto with ctl. Defined. Lemma Dot_mono_right : forall R A B C, derives R B C -> derives R (A o B) (A o C). intros R A B C H . apply gamma'. eapply comp. (* or apply comp with C *) eexact H. auto with ctl. Defined. Hint Resolve Dot_mono_left Dot_mono_right :ctl. Lemma Dot_mono : forall R A B C D, derives R A B -> derives R C D -> derives R (A o C) (B o D). intros R A B C D H H'. eapply comp; eauto with ctl. Defined. Lemma Slash_isotonicity : forall R A B C, derives R A B -> derives R (A // C) (B // C). intros R A B C H. apply beta. apply comp with A; auto with ctl. apply beta'. auto with ctl. Defined. Lemma Slash_antitonicity : forall R A B C, derives R C B -> derives R (A // B) (A // C). intros R A B C H. apply beta. apply comp with (A // B o B); eauto with ctl. apply beta'; auto with ctl. Defined. Definition Backslash_antitonicity : forall R A B C , derives R A B -> derives R (B \\ C) (A \\ C). intros R A B C H. apply gamma. apply comp with (B o B \\ C); eauto with ctl. apply gamma'; auto with ctl. Defined. Definition Backslash_isotonicity : forall R A B C, derives R B C -> derives R (A \\ B) (A \\ C). intros R A B C H. apply gamma. apply comp with B;eauto with ctl. apply gamma';auto with ctl. Defined. Definition Slash_Geach : forall R, extends L R -> forall A B C, derives R (A//B) ((A//C)//(B//C)). intros R H A B C. apply beta. apply beta. eapply comp. eapply structrules_mono with L. eauto. eapply by_rule. econstructor. apply beta'. apply Slash_antitonicity. apply beta'; eauto with ctl. Defined.