(* Playing with NL *) Add LoadPath "../Light". Require Import Forms. Require Import Hilbert. Require Import Semantics. Require Import Sequents. Require Import List. Require Import ZArith. Open Scope Z_scope. Open Scope lbk_scope. Ltac beta := apply beta. Ltac gamma := apply gamma. Ltac beta' := apply beta'. Ltac gamma' := apply gamma'. Ltac comp X := apply comp with (B:=X). Ltac ecomp := eapply comp. Ltac one := apply one. Definition deriv1 : s -NL-> (s o np) // np. beta. one. Defined. Definition deriv2 : (s//np) o np -NL-> s. beta'. one. Defined. Definition deriv3 : np o (np \\ (s // np)) o np -NL-> s. beta'. gamma'. one. Defined. Definition deriv4 : (np//n)o(n//n o n) -NL-> np. comp (np//n o n). Definition Dot_mono_right : forall A B C : Form, B -NL-> C -> A o B -NL-> A o C. intros A B C H. gamma'. comp C. assumption. gamma. one. Defined. Hint Resolve Dot_mono_right : ctl. apply Dot_mono_right. beta'; auto with ctl. beta'; auto with ctl. Defined. Definition Dot_mono : forall A B C D, A -NL-> B -> C -NL-> D -> A o C -NL-> B o D. intros A B C D H H0. ecomp. eapply Dot_mono_right. eauto. eauto with ctl. Defined. Definition isotonicity : forall A B C : Form , A -NL-> B -> A // C -NL-> B // C. intros A B C H. beta. comp A. beta'; auto with ctl. assumption. Defined. Definition antitonicity: forall A B C : Form , C -NL-> B -> A // B -NL-> A // C. intros A B C H. beta. ecomp. eapply Dot_mono_right. eexact H. beta'; auto with ctl. Defined. Definition antitonicity': forall A B C : Form , A -NL-> B -> B \\ C -NL-> A \\ C. intros A B C H. gamma. ecomp. eapply Dot_mono_left. eexact H. gamma'; auto with ctl. Defined. Definition isotonicity' : forall A B C : Form, B -NL-> C -> A \\ B -NL-> A \\ C. intros A B C H. gamma. comp B. gamma'; auto with ctl. assumption. Defined. Definition lifting: forall A B, A -NL-> B//(A\\B). intros A B; beta. gamma'; auto with ctl. Defined. Definition lifting': forall A B, A -NL-> (B//A)\\B. intros A B; gamma; beta'; auto with ctl. Defined. Lemma ex3' : np o (np \\ (s // np)) o np -NL-> s. beta'. gamma'. auto with ctl. Defined.