ocaml 3.09 transition

[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
index e96bef4a70a81ecbc1876aab4444379464fbaa98..2949e83d986cbd6fbda470aa2c2c43911b62edfd 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/csub0_defs.v
@@ -4,20 +4,20 @@ 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))
+         | 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_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).
+      Theorem csub0_refl: (g:?; c:?) (csub0 g c c).
       XElim c; XAuto.
       Qed.
 
@@ -27,11 +27,11 @@ Require Export ty0_defs.
 
    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))
-                                ).
+      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.
@@ -60,16 +60,16 @@ Require Export ty0_defs.
       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))
+      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)
-                                ).
+                               ) \/
+                               (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.
@@ -112,75 +112,3 @@ Require Export ty0_defs.
                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.
-
-   Section csub0_pc3. (*****************************************************)
-
-      Theorem csub0_pr2 : (g:?; c1:?; t1,t2:?) (pr2 c1 t1 t2) ->
-                          (c2:?) (csub0 g c1 c2) -> (pr2 c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1 : pr2_free *)
-      XAuto.
-(* case 2 : pr2_delta *)
-      CSub0Drop; XEAuto.
-      Qed.
-
-      Theorem csub0_pc2 : (g:?; c1:?; t1,t2:?) (pc2 c1 t1 t2) ->
-                          (c2:?) (csub0 g c1 c2) -> (pc2 c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1 : pc2_r *)
-      Apply pc2_r; EApply csub0_pr2; XEAuto.
-(* case 2 : pc2_x *)
-      Apply pc2_x; EApply csub0_pr2; XEAuto.
-      Qed.
-
-      Theorem csub0_pc3 : (g:?; c1:?; t1,t2:?) (pc3 c1 t1 t2) ->
-                          (c2:?) (csub0 g c1 c2) -> (pc3 c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1 : pc3_r *)
-      XAuto.
-(* case 2 : pc3_u *)
-      EApply pc3_u; [ EApply csub0_pc2; XEAuto | XAuto ].
-      Qed.
-
-   End csub0_pc3.
-
-      Hints Resolve csub0_pc3 : ltlc.
-
-   Section csub0_ty0. (*****************************************************)
-
-      Theorem csub0_ty0 : (g:?; c1:?; t1,t2:?) (ty0 g c1 t1 t2) ->
-                          (c2:?) (wf0 g c2) -> (csub0 g c1 c2) ->
-                          (ty0 g c2 t1 t2).
-      Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
-      EApply ty0_conv; XEAuto.
-(* case 2 : ty0_sort *)
-      XEAuto.
-(* case 3 : ty0_abbr *)
-      CSub0Drop; EApply ty0_abbr; XEAuto.
-(* case 4 : ty0_abst *)
-      CSub0Drop; [ EApply ty0_abst | EApply ty0_abbr ]; XEAuto.
-(* case 5 : ty0_bind *)
-      EApply ty0_bind; XEAuto.
-(* case 6 : ty0_appl *)
-      EApply ty0_appl; XEAuto.
-(* case 7 : ty0_cast *)
-      EApply ty0_cast; XAuto.
-      Qed.
-
-      Theorem csub0_ty0_ld : (g:?; c:?; u,v:?) (ty0 g c u v) -> (t1,t2:?)
-                             (ty0 g (CTail c (Bind Abst) v) t1 t2) ->
-                             (ty0 g (CTail c (Bind Abbr) u) t1 t2).
-      Intros; EApply csub0_ty0; XEAuto.
-      Qed.
-
-   End csub0_ty0.
-
-      Hints Resolve csub0_ty0 csub0_ty0_ld : ltlc.
-
-      Tactic Definition CSub0Ty0 :=
-         Match Context With
-            [ _: (ty0 ?1 ?2 ?4 ?); _: (ty0 ?1 ?2 ?3 ?7); _: (pc3 ?2 ?4 ?7);
-              H: (ty0 ?1 (CTail ?2 (Bind Abst) ?4) ?5 ?6) |- ? ] ->
-               LApply (csub0_ty0_ld ?1 ?2 ?3 ?4); [ Intros H_x | EApply ty0_conv; XEAuto ];
-               LApply (H_x ?5 ?6); [ Clear H_x H; Intros | XAuto ].