we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csubst1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csubst1_defs.v
deleted file mode 100644 (file)
index 8d1e570..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/csubst1_defs.v
+++ /dev/null
@@ -1,101 +0,0 @@
-(*#* #stop file *)
-
-Require Export subst1_defs.
-Require Export csubst0_defs.
-
-      Inductive csubst1 [i:nat; v:T; c1:C] : C -> Prop :=
-         | csubst1_refl   : (csubst1 i v c1 c1)
-         | csubst1_single : (c2:?) (csubst0 i v c1 c2) -> (csubst1 i v c1 c2).
-
-      Hint csubst1 : ltlc := Constructors csubst1.
-
-   Section csubst1_props. (**************************************************)
-
-      Theorem csubst1_tail: (k:?; i:?; v,u1,u2:?) (subst1 (r k i) v u1 u2) ->
-                            (c1,c2:?) (csubst1 (r k i) v c1 c2) ->
-                            (csubst1 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
-      Intros until 1; XElim H; Clear u2.
-(* case 1: csubst1_refl *)
-      Intros until 1; XElim H; Clear c2; XAuto.
-(* case 2: csubst1_single *)
-      Intros until 2; XElim H0; Clear c2; XAuto.
-      Qed.
-
-   End csubst1_props.
-
-      Hints Resolve csubst1_tail : ltlc.
-
-   Section csubst1_gen_base. (***********************************************)
-
-      Theorem csubst1_gen_tail: (k:?; c1,x:?; u1,v:?; i:?)
-                                (csubst1 (S i) v (CTail c1 k u1) x) ->
-                                (EX u2 c2 | x = (CTail c2 k u2) &
-                                            (subst1 (r k i) v u1 u2) &
-                                            (csubst1 (r k i) v c1 c2)
-                                ).
-      Intros; InsertEq H '(CTail c1 k u1); InsertEq H '(S i);
-      XElim H; Clear x; Intros.
-(* case 1: csubst1_refl *)
-      Rewrite H0; XEAuto.
-(* case 2: csubst1_single *)
-      Rewrite H0 in H; Rewrite H1 in H; Clear H0 H1 y y0.
-      CSubst0GenBase; Rewrite H; XEAuto.
-      Qed.
-
-   End csubst1_gen_base.
-
-      Tactic Definition CSubst1GenBase :=
-         Match Context With
-            | [ H: (csubst1 (S ?1) ?2 (CTail ?3 ?4 ?5) ?6) |- ? ] ->
-               LApply (csubst1_gen_tail ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros.
-
-   Section csubst1_drop. (***************************************************)
-
-      Theorem csubst1_drop_ge : (i,n:?) (le i n) ->
-                                (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
-                                (e:?) (drop n (0) c1 e) ->
-                                (drop n (0) c2 e).
-      Intros until 2; XElim H0; Intros;
-      Try CSubst0Drop; XAuto.
-      Qed.
-
-      Theorem csubst1_drop_lt : (i,n:?) (lt n i) ->
-                                (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
-                                (e1:?) (drop n (0) c1 e1) ->
-                                (EX e2 | (csubst1 (minus i n) v e1 e2) &
-                                         (drop n (0) c2 e2)
-                                ).
-      Intros until 2; XElim H0; Intros;
-      Try (
-         CSubst0Drop; Try Rewrite H1; Try Rewrite minus_x_Sy;
-         Try Rewrite r_minus in H3; Try Rewrite r_minus in H4
-      ); XEAuto.
-      Qed.
-
-      Theorem csubst1_drop_ge_back : (i,n:?) (le i n) ->
-                                     (c1,c2:?; v:?) (csubst1 i v c1 c2) ->
-                                     (e:?) (drop n (0) c2 e) ->
-                                     (drop n (0) c1 e).
-      Intros until 2; XElim H0; Intros;
-      Try CSubst0Drop; XAuto.
-      Qed.
-
-   End csubst1_drop.
-
-      Tactic Definition CSubst1Drop :=
-         Match Context With
-            | [ H1: (lt ?2 ?1);
-                H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
-               LApply (csubst1_drop_lt ?1 ?2); [ Intros H_x | XAuto ];
-               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
-               LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
-               XElim H3; Intros
-            | [H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
-               LApply (csubst1_drop_ge ?1 ?1); [ Intros H_x | XAuto ];
-               LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
-               LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
-            | [ H2: (csubst1 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
-               LApply (csubst1_drop_ge ?1 ?2); [ Intros H_x | XAuto ];
-               LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
-               LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ].