X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_confluence.v;fp=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_confluence.v;h=0000000000000000000000000000000000000000;hb=7dc9dcddc88440527569d2a7216461bcd7398ab2;hp=c23d6743fde4f5fc95dc83ba6d2cda2ef8e67caa;hpb=a57efb7e02d1c0af621ab36bd345f2f79f063a0c;p=helm.git diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v deleted file mode 100644 index c23d6743f..000000000 --- a/helm/coq-contribs/LAMBDA-TYPES/pr0_confluence.v +++ /dev/null @@ -1,176 +0,0 @@ -(*#* #stop file *) - -Require tlt_defs. -Require lift_gen. -Require lift_tlt. -Require subst0_gen. -Require subst0_confluence. -Require pr0_defs. -Require pr0_lift. -Require pr0_gen. -Require pr0_subst0. - - Section pr0_confluence. (*************************************************) - - Tactic Definition SSubstInv := - Match Context With - | [ H0: (TTail ? ? ?) = (TTail ? ? ?) |- ? ] -> - Inversion H0; Clear H0 - | [ H0: (pr0 (TTail (Bind ?) ? ?) ?) |- ? ] -> - Inversion H0; Clear H0 - | _ -> EqFalse Orelse LiftGen Orelse Pr0Gen. - - Tactic Definition SSubstBack := - Match Context With - | [ H0: Abst = ?1; H1:? |- ? ] -> - Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1 - | [ H0: Abbr = ?1; H1:? |- ? ] -> - Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1 - | [ H0: (? ?) = ?1; H1:? |- ? ] -> - Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1 - | [ H0: (? ? ? ?) = ?1; H1:? |- ? ] -> - Rewrite <- H0 in H1 Orelse Rewrite <- H0 Orelse Clear H0 ?1. - - Tactic Definition SSubst := - Match Context With - [ H0: ?1 = ?; H1:? |- ? ] -> - Rewrite H0 in H1 Orelse Rewrite H0 Orelse Clear H0 ?1. - - Tactic Definition XSubst := - Repeat (SSubstInv Orelse SSubstBack Orelse SSubst). - - Tactic Definition IH := - Match Context With - | [ H0: (pr0 ?1 ?2); H1: (pr0 ?1 ?3) |- ? ] -> - LApply (H ?1); [ Intros H_x | XEAuto ]; - LApply (H_x ?2); [ Clear H_x; Intros H_x | XAuto ]; - LApply (H_x ?3); [ Clear H_x; Intros H_x | XAuto ]; - XElim H_x; Clear H0 H1; Intros. - -(* case pr0_cong pr0_upsilon pr0_refl ***************************************) - - Remark pr0_cong_upsilon_refl: (b:?) ~ b = Abst -> - (u0,u3:?) (pr0 u0 u3) -> - (t4,t5:?) (pr0 t4 t5) -> - (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) -> - (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u0 t4)) t) & - (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)). - Intros. - Apply ex2_intro with x:=(TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) x) t5)); XAuto. - Qed. - -(* case pr0_cong pr0_upsilon pr0_cong ***************************************) - - Remark pr0_cong_upsilon_cong: (b:?) ~ b = Abst -> - (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) -> - (t2,t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) -> - (u5,u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) -> - (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind b) u5 t2)) t) & - (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)). - Intros. - Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto. - Qed. - -(* case pr0_cong pr0_upsilon pr0_delta **************************************) - - Remark pr0_cong_upsilon_delta: ~ Abbr = Abst -> - (u5,t2,w:?) (subst0 (0) u5 t2 w) -> - (u2,v2,x:?) (pr0 u2 x) -> (pr0 v2 x) -> - (t5,x0:?) (pr0 t2 x0) -> (pr0 t5 x0) -> - (u3,x1:?) (pr0 u5 x1) -> (pr0 u3 x1) -> - (EX t:T | (pr0 (TTail (Flat Appl) u2 (TTail (Bind Abbr) u5 w)) t) & - (pr0 (TTail (Bind Abbr) u3 (TTail (Flat Appl) (lift (1) (0) v2) t5)) t)). - Intros; Pr0Subst0. -(* case 1: x0 is a lift *) - Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x0)); XAuto. -(* case 2: x0 is not a lift *) - Apply ex2_intro with x:=(TTail (Bind Abbr) x1 (TTail (Flat Appl) (lift (1) (0) x) x2)); XEAuto. - Qed. - -(* case pr0_cong pr0_upsilon pr0_zeta ***************************************) - - Remark pr0_cong_upsilon_zeta: (b:?) ~ b = Abst -> - (u0,u3:?) (pr0 u0 u3) -> - (u2,v2,x0:?) (pr0 u2 x0) -> (pr0 v2 x0) -> - (x,t3,x1:?) (pr0 x x1) -> (pr0 t3 x1) -> - (EX t:T | (pr0 (TTail (Flat Appl) u2 t3) t) & - (pr0 (TTail (Bind b) u3 (TTail (Flat Appl) (lift (1) (0) v2) (lift (1) (0) x))) t)). - Intros; LiftTailRwBack; XEAuto. - Qed. - -(* case pr0_cong pr0_delta **************************************************) - - Remark pr0_cong_delta: (u3,t5,w:?) (subst0 (0) u3 t5 w) -> - (u2,x:?) (pr0 u2 x) -> (pr0 u3 x) -> - (t3,x0:?) (pr0 t3 x0) -> (pr0 t5 x0) -> - (EX t:T | (pr0 (TTail (Bind Abbr) u2 t3) t) & - (pr0 (TTail (Bind Abbr) u3 w) t)). - Intros; Pr0Subst0; XEAuto. - Qed. - -(* case pr0_upsilon pr0_upsilon *********************************************) - - Remark pr0_upsilon_upsilon: (b:?) ~ b = Abst -> - (v1,v2,x0:?) (pr0 v1 x0) -> (pr0 v2 x0) -> - (u1,u2,x1:?) (pr0 u1 x1) -> (pr0 u2 x1) -> - (t1,t2,x2:?) (pr0 t1 x2) -> (pr0 t2 x2) -> - (EX t:T | (pr0 (TTail (Bind b) u1 (TTail (Flat Appl) (lift (1) (0) v1) t1)) t) & - (pr0 (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)) t)). - Intros. - Apply ex2_intro with x:=(TTail (Bind b) x1 (TTail (Flat Appl) (lift (1) (0) x0) x2)); XAuto. - Qed. - -(* case pr0_delta pr0_delta *************************************************) - - Remark pr0_delta_delta: (u2,t3,w:?) (subst0 (0) u2 t3 w) -> - (u3,t5,w0:?) (subst0 (0) u3 t5 w0) -> - (x:?) (pr0 u2 x) -> (pr0 u3 x) -> - (x0:?) (pr0 t3 x0) -> (pr0 t5 x0) -> - (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) & - (pr0 (TTail (Bind Abbr) u3 w0) t)). - Intros; Pr0Subst0; Pr0Subst0; Try Subst0Confluence; XSubst; XEAuto. - Qed. - -(* case pr0_delta pr0_epsilon ***********************************************) - - Remark pr0_delta_epsilon: (u2,t3,w:?) (subst0 (0) u2 t3 w) -> - (t4:?) (pr0 (lift (1) (0) t4) t3) -> - (t2:?) (EX t:T | (pr0 (TTail (Bind Abbr) u2 w) t) & (pr0 t2 t)). - Intros; Pr0Gen; XSubst; Subst0Gen. - Qed. - -(* main *********************************************************************) - - Hints Resolve pr0_cong_upsilon_refl pr0_cong_upsilon_cong : ltlc. - Hints Resolve pr0_cong_upsilon_delta pr0_cong_upsilon_zeta : ltlc. - Hints Resolve pr0_cong_delta : ltlc. - Hints Resolve pr0_upsilon_upsilon : ltlc. - Hints Resolve pr0_delta_delta pr0_delta_epsilon : ltlc. - -(*#* #start file *) - -(*#* #caption "confluence with itself: Church-Rosser property" *) -(*#* #cap #cap t0, t1, t2, t *) - - Theorem pr0_confluence: (t0,t1:?) (pr0 t0 t1) -> (t2:?) (pr0 t0 t2) -> - (EX t | (pr0 t1 t) & (pr0 t2 t)). - -(*#* #stop file *) - - XElimUsing tlt_wf_ind t0; Intros. - Inversion H0; Inversion H1; Clear H0 H1; - XSubst; Repeat IH; XDEAuto 4. - Qed. - - End pr0_confluence. - - Tactic Definition Pr0Confluence := - Match Context With - [ H1: (pr0 ?1 ?2); H2: (pr0 ?1 ?3) |-? ] -> - LApply (pr0_confluence ?1 ?2); [ Clear H1; Intros H1 | XAuto ]; - LApply (H1 ?3); [ Clear H1 H2; Intros H1 | XAuto ]; - XElim H1; Intros. - -(*#* #start file *) - -(*#* #single *)