we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v
deleted file mode 100644 (file)
index 61d2ffe..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen_context.v
+++ /dev/null
@@ -1,62 +0,0 @@
-(*#* #stop file *)
-
-Require drop_props.
-Require subst1_gen.
-Require subst1_subst1.
-Require subst1_confluence.
-Require csubst1_defs.
-Require pr0_gen.
-Require pr0_subst1.
-Require pr2_defs.
-Require pr2_gen.
-Require pr2_subst1.
-
-   Section pr2_gen_context. (************************************************)
-
-      Theorem pr2_gen_cabbr: (c:?; t1,t2:?) (pr2 c t1 t2) -> (e:?; u:?; d:?)
-                             (drop d (0) c (CTail e (Bind Abbr) u)) ->
-                             (a0:?) (csubst1 d u c a0) ->
-                             (a:?) (drop (1) d a0 a) ->
-                             (x1:?) (subst1 d u t1 (lift (1) d x1)) ->
-                             (EX x2 | (subst1 d u t2 (lift (1) d x2)) &
-                                      (pr2 a x1 x2)
-                             ).
-      Intros until 1; XElim H; Intros;
-      Pr0Subst1; Pr0Gen.
-(* case 1: pr2_free *)
-      Rewrite H in H3; Clear H x; XEAuto.
-(* case 2: pr2_delta *)
-      Rewrite H0 in H5; Clear H0 x.  
-      Apply (lt_eq_gt_e i d0); Intros.
-(* case 2.1: i < d0 *)
-      Subst1Confluence; CSubst1Drop.
-      Rewrite minus_x_Sy in H; [ Idtac | XAuto ].
-      CSubst1GenBase; Rewrite H in H7; Clear H x2.
-      Rewrite (lt_plus_minus i d0) in H4; [ Idtac | XAuto ].
-      DropDis; Rewrite H in H8; Clear H x3.
-      Subst1Subst1; Pattern 2 d0 in H; Rewrite (lt_plus_minus i d0) in H; [ Idtac | XAuto ].
-      Subst1Gen; Rewrite H in H10; Simpl in H10; Clear H x3.
-      Rewrite <- lt_plus_minus in H10; [ Idtac | XAuto ].
-      Rewrite <- lt_plus_minus_r in H10; XEAuto.
-(* case 2.2: i = d0 *)
-      Rewrite H0 in H; Rewrite H0 in H1; Clear H0 i.
-      DropDis; Inversion H; Rewrite <- H8 in H1; Rewrite <- H8 in H2; Rewrite <- H8; Clear H H7 H8 e u.
-      Subst1Confluence; Subst1Gen; Rewrite H0 in H; Clear H0 x; XEAuto.
-(* case 2.3: i > d0 *)
-      Subst1Confluence; Subst1Gen; Rewrite H5 in H1; Clear H2 H5 x.
-      CSubst1Drop; DropDis; XEAuto.
-      Qed.
-
-   End pr2_gen_context.
-
-      Tactic Definition Pr2GenContext :=
-         Match Context With
-            | [ H0: (pr2 ?1 ?2 ?3); H1: (drop ?4 (0) ?1 (CTail ?5 (Bind Abbr) ?6));
-                H2: (csubst1 ?4 ?6 ?1 ?7); H3: (drop (1) ?4 ?7 ?8);
-                H4: (subst1 ?4 ?6 ?2 (lift (1) ?4 ?9)) |- ? ] ->
-               LApply (pr2_gen_cabbr ?1 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
-               LApply (H0 ?5 ?6 ?4); [ Clear H0; Intros H0 | XAuto ];
-               LApply (H0 ?7); [ Clear H0; Intros H0 | XAuto ];
-               LApply (H0 ?8); [ Clear H0; Intros H0 | XAuto ];
-               LApply (H0 ?9); [ Clear H0 H4; Intros H0 | XAuto ];
-               XElim H0; Intros.