Require Import Forms. Require Export Contexts. Set Implicit Arguments. Inductive sequent : context -> Form -> Set := | Ax : forall A : Form , sequent (form A) A | SlashR : forall Gamma A B, sequent (Gamma oo (form B)) A -> sequent Gamma (A // B) | BackslashR : forall Gamma A B, sequent ((form B) oo Gamma) A -> sequent Gamma (B \\ A) | DotR : forall Gamma Delta A B , sequent Gamma A -> sequent Delta B -> sequent (Gamma oo Delta) (A o B) | SlashL : forall Delta Gamma Gamma' A B C, replace (form A) ((form (A // B)) oo Delta) Gamma Gamma' -> sequent Delta B -> sequent Gamma C -> sequent Gamma' C | BackslashL : forall Delta Gamma Gamma' A B C, replace (form A) (Delta oo (form (B \\ A))) Gamma Gamma' -> sequent Delta B -> sequent Gamma C -> sequent Gamma' C | DotL : forall Gamma Gamma' A B C , replace ((form A) oo (form B)) (form (A o B)) Gamma Gamma' -> sequent Gamma C -> sequent Gamma' C | CutRule : forall Delta Gamma Gamma' A C, replace (form A) Delta Gamma Gamma' -> sequent Delta A -> sequent Gamma C -> sequent Gamma' C. Hint Resolve Ax SlashR BackslashR DotR: ctl. Notation "Gamma ==> A" := (sequent Gamma A) (at level 51) : lbk_scope. Inductive natded : context -> Form -> Set := | Axn : forall A, natded (^A) A | SlashI : forall Gamma A B, natded (Gamma oo ^B) A -> natded Gamma (A // B) | BackslashI : forall Gamma A B, natded (^ B oo Gamma) A -> natded Gamma (B \\ A) | DotI : forall Gamma Delta A B, natded Gamma A -> natded Delta B -> natded (Gamma oo Delta) (A o B) | SlashE : forall Gamma Delta A B, natded Gamma (A // B) -> natded Delta B -> natded (Gamma oo Delta) A | BackslashE : forall Gamma Delta A B, natded Gamma B -> natded Delta (B \\ A) -> natded (Gamma oo Delta) A | DotE : forall Gamma Gamma' Delta A B C, replace (^A oo ^B) Delta Gamma Gamma'-> natded Delta (A o B) -> natded Gamma C -> natded Gamma' C. Notation "Gamma |-- A" := (natded Gamma A) (at level 51) : lbk_scope. Hint Resolve Axn SlashI BackslashI DotI SlashE BackslashE. Definition seq0 : ^(np \\ s) ==> np \\ s. apply Ax. Defined. Definition ded0 : ^(np \\ s) |-- np \\ s. apply Axn. Defined. Definition seq1 : ^s ==> (s o np)//np. auto with ctl. Defined. Definition ded1 : ^s |-- (s o np)//np. auto with ctl. Defined. Definition seq2 : ^(s//np) oo ^np ==> s. eapply SlashL. constructor 1. auto with ctl. auto with ctl. Defined. Definition ded2 : ^(s//np) oo ^np |-- s. eauto with ctl. Defined. Print ded2. (* tactics for replace *) Ltac r_here := constructor 1. Ltac r_left := constructor 2. Ltac r_right := constructor 3. Definition seq2' : ^(s//np) oo ^np ==> s. eapply SlashL. r_here. auto with ctl. auto with ctl. Defined. Definition simpleDotL : forall A B C , (^A oo ^B) ==> C -> ^(A o B) ==> C. intros A B C H. eapply DotL. r_here. trivial. Defined. Definition seq_transitivity: forall Gamma A C, Gamma ==> A -> ^A ==> C -> Gamma ==> C. intros Gamma A C H H0. apply CutRule with Gamma (^ A) A. r_here. assumption. assumption. Defined. (* new tactics *) Ltac unfocus := match goal with | |- (natded (zfill ?zgamma ?Gamma) ?F) => let Gamma' := eval simpl in (zfill zgamma Gamma) in change (natded Gamma' F) | |- (sequent (zfill ?zgamma ?Gamma) ?F) => let Gamma' := eval simpl in (zfill zgamma Gamma) in change (sequent Gamma' F) | |- ?anygoal => idtac end. Ltac z_root := match goal with | |- (natded (zfill ?zgamma ?Gamma) ?F) => let Gamma' := eval simpl in (zfill zgamma Gamma) in change (natded (zfill zroot Gamma') F) | |- natded ?Gamma ?F => change (natded (zfill zroot Gamma) F) | |- (sequent (zfill ?zgamma ?Gamma) ?F) => let Gamma' := eval simpl in (zfill zgamma Gamma) in change (sequent (zfill zroot Gamma') F) | |- sequent ?Gamma ?F => change (sequent (zfill zroot Gamma) F) end. Ltac z_left := match goal with | |- natded (zfill ?z (?G1 oo ?G2)) ?F => change (natded (zfill (zleft z G2) G1) F) | |- sequent (zfill ?z (?G1 oo ?G2)) ?F => change (sequent (zfill (zleft z G2) G1) F) (* a completer *) end. Ltac z_right := match goal with | |- natded (zfill ?z (?G1 oo ?G2)) ?F => change (natded (zfill (zright G1 z) G2) F) | |- sequent (zfill ?z (?G1 oo ?G2)) ?F => change (sequent (zfill (zright G1 z) G2) F) (* a completer *) end. Ltac axiom := unfocus; match goal with | |- natded (form ?A) ?B => eapply Axn | |- sequent (form ?A) ?B => eapply Ax end. Ltac slashI := unfocus; match goal with | |- natded ?Gamma (?F // ?G) => apply SlashI end. Ltac backI := unfocus; match goal with | |- natded ?Gamma (?F \\ ?G) => apply BackslashI end. Ltac dotI := unfocus; eapply DotI. Definition DotE' : forall ZGamma Delta F G H, natded Delta (F o G) -> natded (zfill ZGamma (^F oo ^G)) H -> natded (zfill ZGamma Delta) H. intros. eapply DotE. generalize (zfill_to_replace ZGamma (^F oo ^G) Delta). intros. 2:eexact H0. 2:eexact H1. auto. Defined. Ltac dotE := match goal with | |- natded (zfill ?z ?gamma) ?F => eapply DotE' | |- ?other => eapply DotE end. Ltac eslashE := unfocus; eapply SlashE. Ltac slashE G1 := unfocus; apply SlashE with (G:=G1). Ltac ebackE := unfocus; eapply BackslashE. Ltac backE G1 := unfocus; apply BackslashE with (G:=G1). Ltac slashR := unfocus; eapply SlashR. Ltac backR := unfocus; eapply BackslashR. Ltac dotR := unfocus; eapply DotR. Definition SlashL' : forall ZGamma Delta A B C, sequent Delta B -> sequent (zfill ZGamma (^A)) C -> sequent (zfill ZGamma ((form (A // B)) oo Delta)) C. intros. eapply SlashL. generalize (zfill_to_replace ZGamma (^A) ((form (A // B)) oo Delta)). intro H1;eexact H1. auto. auto. Defined. Ltac slashL := match goal with | |- sequent (zfill ?z ?gamma) ?F => eapply SlashL' | |- ?other => eapply SlashL' end. Definition BackslashL' : forall ZGamma Delta A B C, sequent Delta B -> sequent (zfill ZGamma (^A)) C -> sequent (zfill ZGamma (Delta oo (form (B \\ A)) )) C. intros. eapply BackslashL. generalize (zfill_to_replace ZGamma (^A) (Delta oo (form (B \\ A)) )). intro H1;eexact H1. auto. auto. Defined. Ltac backL := match goal with | |- sequent (zfill ?z ?gamma) ?F => eapply BackslashL' | |- ?other => eapply BackslashL end. Definition DotL' : forall ZGamma A B C, sequent (zfill ZGamma (^A oo ^B)) C -> sequent (zfill ZGamma (^(A o B))) C. intros. eapply DotL. generalize (zfill_to_replace ZGamma (^A oo ^B) (^(A o B))). intro H1;eexact H1. auto. Defined. Ltac dotL := match goal with | |- sequent (zfill ?z ?gamma) ?F => eapply DotL' | |- ?other => eapply DotL end. Definition CutRule' : forall ZGamma Delta A C, sequent Delta A -> sequent (zfill ZGamma (^A)) C -> sequent (zfill ZGamma Delta) C. intros; eapply CutRule. generalize (zfill_to_replace ZGamma (^A) Delta). intro H1;eexact H1. auto. auto. Defined. Ltac cut_rule F:= match goal with | |- sequent (zfill ?z ?gamma) ?C => eapply CutRule' with (A:=F) | |- _ => eapply CutRule with (A:=F) end. Definition application : forall A B, ^(A//B o B) ==> A. intros A B. z_root. dotL. slashL; axiom. Defined. Definition application' : forall A B, ^(B o B\\A) ==>A. intros A B. dotL. r_here. backL. r_here. axiom. axiom. Defined. Definition coApplication : forall A B, ^A ==> (A o B)//B. auto with ctl. Defined. Definition coApplication' : forall A B, ^A ==> B\\(B o A). auto with ctl. Defined. Definition monotonicity : forall A B C D, ^A ==> B -> ^ C ==> D -> ^(A o C) ==> B o D. intros A B C D H H0. z_root; dotL. dotR;auto. Defined. Definition isotonicity : forall A B C, ^A ==> B -> ^(A//C) ==> (B//C). intros A B C H. slashR. z_root; cut_rule A. z_root; slashL. axiom. axiom. unfocus; auto. Defined. Definition isotonicity' : forall A B C, ^A ==> B -> ^(C\\A) ==> C\\B. intros A B C H. backR. z_root; cut_rule A. z_root; backL; axiom. unfocus ; auto. Defined. Definition antitonicity : forall A B C, ^A ==> B -> ^(C// B) ==> C // A. intros A B C H. slashR. z_root. cut_rule (C//B o B). dotR. axiom. assumption. unfocus;apply application. Defined. Definition antitonicity' : forall A B C, ^A ==>B -> ^(B\\C) ==> A\\C. intros A B C H. backR. z_root; cut_rule (B o (B\\C)). dotR. assumption. axiom. unfocus; apply application'. Defined. Definition lifting : forall A B, ^A ==> B // (A \\ B). intros A B . slashR. z_root; cut_rule (A o (A \\ B)). dotR; axiom. unfocus; apply application'. Defined. Definition lifting' : forall A B, ^A ==> (B//A)\\B. intros A B. backR. z_root; cut_rule (B//A o A). dotR; axiom. unfocus; apply application. Defined. (* using natural deduction *) Definition application_d : forall A B, ^(A//B o B) |-- A. intros A B. z_root. dotE. axiom. eslashE; axiom. Defined. Definition application_d' : forall A B, ^(B o B\\A) |-- A. intros A B. z_root. dotE. axiom. ebackE; axiom. Defined. Definition coApplication_d : forall A B, ^A |-- (A o B)//B. auto with ctl. Defined. Definition coApplication_d' : forall A B, ^A |-- B\\(B o A). auto with ctl. Defined. Definition monotonicity_d : forall A B C D, ^A |-- B -> ^ C |-- D -> ^(A o C)|-- B o D. intros A B C D H H0. z_root; dotE. axiom. dotI;auto. Defined. Definition isotonicity_d : forall A B C, ^A|-- B -> ^(A//C) |-- (B//C). intros A B C H. slashI. eslashE. 2:axiom. Abort. Definition antitonicity_d : forall A B C, ^A |-- B -> ^(C// B) |-- C // A. intros A B C H. slashI. eslashE. axiom. assumption. Defined. Definition lifting_d : forall A B, ^A |-- B // (A \\ B). intros A B . slashI. ebackE;axiom. Defined. Require Import Hilbert. Definition NL_arrowToseq : forall (A B : Form), A -NL-> B -> (form A) ==> B. induction 1. axiom. cut_rule B. r_here. assumption. assumption. slashR. z_root; cut_rule (A o B). dotR ;auto with ctl. unfocus; assumption. z_root; cut_rule (C // B o B). z_root; dotL. dotR. assumption. axiom. dotL. slashL. axiom. axiom. backR. z_root; cut_rule (A o B). dotR;axiom. unfocus; assumption. z_root; cut_rule (A o A \\ C). z_root; dotL. dotR; auto with ctl. dotL; auto with ctl. backL; auto with ctl. axiom. Defined. Definition replace_NL_arrow : forall T1 T2 Gamma Gamma', replace T1 T2 Gamma Gamma' -> NL_arrow (context_to_form T2) (context_to_form T1) -> NL_arrow (context_to_form Gamma') (context_to_form Gamma). simple induction 1. auto. intros; auto with ctl. simpl;apply Dot_mono_left. auto. intros. simpl in |- *. apply Dot_mono_right. auto. Defined. Definition replace_NL_arrow' : forall T1 T2 Gamma Gamma' C, replace T1 T2 Gamma Gamma' -> NL_arrow (context_to_form T2) (context_to_form T1) -> NL_arrow (context_to_form Gamma) C -> NL_arrow (context_to_form Gamma') C. intros T1 T2 Gamma. intros. apply comp with (context_to_form Gamma). eapply replace_NL_arrow; eauto. assumption. Defined. Definition seqToNL_arrow : forall Gamma A, Gamma ==> A -> (context_to_form Gamma) -NL-> A. intros Gamma A H. elim H. intros; simpl in |- *; auto with ctl. intros; simpl in |- *; auto with ctl. intros; simpl in |- *; auto with ctl. intros; simpl in |- *; apply Dot_mono; assumption. intros Delta Gamma0. intros. eapply replace_NL_arrow'; eauto. simpl in |- *. apply beta'. apply Slash_antitonicity. assumption. intros Delta Gamma0. intros. eapply replace_NL_arrow'; eauto. simpl in |- *. apply gamma'. apply Backslash_antitonicity. assumption. intro Gamma0; intros. eapply replace_NL_arrow'; eauto. simpl in |- *. apply one. intros Delta Gamma0; intros. eapply replace_NL_arrow'; eauto. Defined.