we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
deleted file mode 100644 (file)
index 2949e83..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
+++ /dev/null
@@ -1,114 +0,0 @@
-(*#* #stop file *)
-
-Require Export ty0_defs.
-
-      Inductive csub0 [g:G] : C -> C -> Prop :=
-(* structural rules *)
-         | csub0_sort: (n:?) (csub0 g (CSort n) (CSort n))
-         | csub0_tail: (c1,c2:?) (csub0 g c1 c2) -> (k,u:?)
-                       (csub0 g (CTail c1 k u) (CTail c2 k u))
-(* axioms *)
-         | csub0_void: (c1,c2:?) (csub0 g c1 c2) -> (b:?) ~b=Void -> (u1,u2:?)
-                       (csub0 g (CTail c1 (Bind Void) u1) (CTail c2 (Bind b) u2))
-         | csub0_abst: (c1,c2:?) (csub0 g c1 c2) -> (u,t:?) (ty0 g c2 u t) ->
-                        (csub0 g (CTail c1 (Bind Abst) t) (CTail c2 (Bind Abbr) u)).
-
-      Hint csub0 : ltlc := Constructors csub0.
-
-   Section csub0_props. (****************************************************)
-
-      Theorem csub0_refl: (g:?; c:?) (csub0 g c c).
-      XElim c; XAuto.
-      Qed.
-
-   End csub0_props.
-
-      Hints Resolve csub0_refl : ltlc.
-
-   Section csub0_drop. (*****************************************************)
-
-      Theorem csub0_drop_abbr: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,u:?)
-                               (drop n (0) c1 (CTail d1 (Bind Abbr) u)) ->
-                               (EX d2 | (csub0 g d1 d2) &
-                                        (drop n (0) c2 (CTail d2 (Bind Abbr) u))
-                               ).
-      XElim n.
-(* case 1 : n = 0 *)
-      Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
-(* case 2 : n > 0 *)
-      Intros until 2; XElim H0.
-(* case 2.1 : csub0_sort *)
-      Intros; Inversion H0.
-(* case 2.2 : csub0_tail *)
-      XElim k; Intros; DropGenBase.
-(* case 2.2.1 : Bind *)
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
-      XElim H; XEAuto.
-(* case 2.2.2 : Flat *)
-      LApply (H1 d1 u0); [ Clear H1; Intros H1 | XAuto ].
-      XElim H1; XEAuto.
-(* case 2.3 : csub0_void *)
-      Intros; DropGenBase.
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 u); [ Clear H; Intros H | XAuto ].
-      XElim H; XEAuto.
-(* case 2.4 : csub0_abst *)
-      Intros; DropGenBase.
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 u0); [ Clear H; Intros H | XAuto ].
-      XElim H; XEAuto.
-      Qed.
-
-      Theorem csub0_drop_abst: (g:?; n:?; c1,c2:?) (csub0 g c1 c2) -> (d1,t:?)
-                               (drop n (0) c1 (CTail d1 (Bind Abst) t)) ->
-                               (EX d2 | (csub0 g d1 d2) &
-                                        (drop n (0) c2 (CTail d2 (Bind Abst) t))
-
-                               ) \/
-                               (EX d2 u | (csub0 g d1 d2) &
-                                          (drop n (0) c2 (CTail d2 (Bind Abbr) u)) &
-                                          (ty0 g d2 u t)
-                               ).
-      XElim n.
-(* case 1 : n = 0 *)
-      Intros; DropGenBase; Rewrite H0 in H; Inversion H; XEAuto.
-(* case 2 : n > 0 *)
-      Intros until 2; XElim H0.
-(* case 2.1 : csub0_sort *)
-      Intros; Inversion H0.
-(* case 2.2 : csub0_tail *)
-      XElim k; Intros; DropGenBase.
-(* case 2.2.1 : Bind *)
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 t); [ Clear H; Intros H | XAuto ].
-      XElim H; Intros; XElim H; XEAuto.
-(* case 2.2.2 : Flat *)
-      LApply (H1 d1 t); [ Clear H1; Intros H1 | XAuto ].
-      XElim H1; Intros; XElim H1; XEAuto.
-(* case 2.3 : csub0_void *)
-      Intros; DropGenBase.
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 t); [ Clear H; Intros H | XAuto ].
-      XElim H; Intros; XElim H; XEAuto.
-(* case 2.4 : csub0_abst *)
-      Intros; DropGenBase.
-      LApply (H c0 c3); [ Clear H; Intros H | XAuto ].
-      LApply (H d1 t0); [ Clear H; Intros H | XAuto ].
-      XElim H; Intros; XElim H; XEAuto.
-      Qed.
-
-   End csub0_drop.
-
-      Tactic Definition CSub0Drop :=
-         Match Context With
-            | [ H1: (csub0 ?1 ?2 ?3);
-                H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abbr) ?6)) |- ? ] ->
-               LApply (csub0_drop_abbr ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros
-            | [ H1: (csub0 ?1 ?2 ?3);
-                H2: (drop ?4 (0) ?2 (CTail ?5 (Bind Abst) ?6)) |- ? ] ->
-               LApply (csub0_drop_abst ?1 ?4 ?2 ?3); [ Clear H1; Intros H1 | XAuto ];
-               LApply (H1 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
-               XElim H1; Intros H1; XElim H1; Intros.