contribution about \lambda-\delta

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / cpr0_props.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v b/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v
new file mode 100644 (file)
index 0000000..1050288
--- /dev/null
+++ b/helm/coq-contribs/LAMBDA-TYPES/cpr0_props.v
@@ -0,0 +1,103 @@
+(*#* #stop file *)
+
+Require pr0_subst0.
+Require pr3_defs.
+Require pr3_props.
+Require cpr0_defs.
+
+   Section cpr0_drop. (******************************************************)
+
+      Theorem cpr0_drop : (c1,c2:?) (cpr0 c1 c2) -> (h:?; e1:?; u1:?; k:?)
+                          (drop h (0) c1 (CTail e1 k u1)) ->
+                          (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
+                                      (cpr0 e1 e2) & (pr0 u1 u2)
+                          ).
+      Intros until 1; XElim H.
+(* case 1 : cpr0_refl *)
+      XEAuto.
+(* case 2 : cpr0_cont *)
+      XElim h.
+(* case 2.1 : h = 0 *)
+      Intros; DropGenBase.
+      Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
+(* case 2.2 : h > 0 *)
+      XElim k; Intros; DropGenBase.
+(* case 2.2.1 : Bind *)
+      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+      XElim H0; XEAuto.
+(* case 2.2.2 : Flat *)
+      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+      XElim H0; XEAuto.
+      Qed.
+
+      Theorem cpr0_drop_back : (c1,c2:?) (cpr0 c2 c1) -> (h:?; e1:?; u1:?; k:?)
+                               (drop h (0) c1 (CTail e1 k u1)) ->
+                               (EX e2 u2 | (drop h (0) c2 (CTail e2 k u2)) &
+                                           (cpr0 e2 e1) & (pr0 u2 u1)
+                               ).
+      Intros until 1; XElim H.
+(* case 1 : cpr0_refl *)
+      XEAuto.
+(* case 2 : cpr0_cont *)
+      XElim h.
+(* case 2.1 : h = 0 *)
+      Intros; DropGenBase.
+      Inversion H2; Rewrite H6 in H1; Rewrite H4 in H; XEAuto.
+(* case 2.2 : h > 0 *)
+      XElim k; Intros; DropGenBase.
+(* case 2.2.1 : Bind *)
+      LApply (H0 n e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+      XElim H0; XEAuto.
+(* case 2.2.2 : Flat *)
+      LApply (H0 (S n) e1 u0 k); [ Clear H0 H3; Intros H0 | XAuto ].
+      XElim H0; XEAuto.
+      Qed.
+
+   End cpr0_drop.
+
+      Tactic Definition Cpr0Drop :=
+         Match Context With
+            | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
+                _: (cpr0 ?2 ?6) |- ? ] ->
+               LApply (cpr0_drop ?2 ?6); [ Intros H_x | XAuto ];
+               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+               XElim H_x; Intros
+            | [ _: (drop ?1 (0) ?2 (CTail ?3 ?4 ?5));
+                _: (cpr0 ?6 ?2) |- ? ] ->
+               LApply (cpr0_drop_back ?2 ?6); [ Intros H_x | XAuto ];
+               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+               XElim H_x; Intros
+            | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
+                _: (cpr0 ?2 ?6) |- ? ] ->
+               LApply (cpr0_drop (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
+               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+               XElim H_x; Intros
+            | [ _: (drop ?1 (0) (CTail ?2 ?7 ?8) (CTail ?3 ?4 ?5));
+                _: (cpr0 ?6 ?2) |- ? ] ->
+               LApply (cpr0_drop_back (CTail ?2 ?7 ?8) (CTail ?6 ?7 ?8)); [ Intros H_x | XAuto ];
+               LApply (H_x ?1 ?3 ?5 ?4); [ Clear H_x; Intros H_x | XAuto ];
+               XElim H_x; Intros.
+
+   Section cpr0_pr3. (*******************************************************)
+
+      Theorem cpr0_pr3_t : (c1,c2:?) (cpr0 c2 c1) -> (t1,t2:?) (pr3 c1 t1 t2) ->
+                           (pr3 c2 t1 t2).
+      Intros until 1; XElim H; Intros.
+(* case 1 : cpr0_refl *)
+      XAuto.
+(* case 2 : cpr0_cont *)
+      Pr3Context.
+      XElim H1; Intros.
+(* case 2.1 : pr3_r *)
+      XAuto.
+(* case 2.2 : pr3_u *)
+      EApply pr3_t; [ Idtac | XEAuto ]. Clear H2 H3 c1 c2 t1 t2 t4 u2.
+      Inversion_clear H1.
+(* case 2.2.1 : pr2_pr0 *)
+      XAuto.
+(* case 2.2.1 : pr2_delta *)
+      Cpr0Drop; Pr0Subst0.
+      EApply pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
+      Qed.
+
+   End cpr0_pr3.