we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_gen.v
deleted file mode 100644 (file)
index 29e3d64..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_gen.v
+++ /dev/null
@@ -1,185 +0,0 @@
-Require pc3_props.
-Require ty0_defs.
-
-(*#* #caption "generation lemma of typing" #clauses *)
-
-   Section ty0_gen_base. (***************************************************)
-
-(*#* #caption "generation lemma for sorts" *)
-(*#* #cap #cap c #alpha x in T, n in h *)
-
-      Theorem ty0_gen_sort: (g:?; c:?; x:?; n:?)
-                            (ty0 g c (TSort n) x) ->
-                            (pc3 c (TSort (next g n)) x).
-                            
-(*#* #stop proof *) 
-
-      Intros until 1; InsertEq H '(TSort n); XElim H; Intros.
-(* case 1 : ty0_conv *)
-      XEAuto.
-(* case 2 : ty0_sort *)
-      Inversion H0; XAuto.
-(* case 3 : ty0_abbr *)
-      Inversion H3.
-(* case 4 : ty0_abst *)
-      Inversion H3.
-(* case 5 : ty0_bind *)
-      Inversion H5.
-(* case 6 : ty0_appl *)
-      Inversion H3.
-(* case 7 : ty0_cast *)
-      Inversion H3.
-      Qed.
-
-(*#* #start proof *) 
-
-(*#* #caption "generation lemma for bound references" *)
-(*#* #cap #cap c, e #alpha x in T, t in U, u in V, n in i *)
-
-      Theorem ty0_gen_lref: (g:?; c:?; x:?; n:?) (ty0 g c (TLRef n) x) ->
-                            (EX e u t | (pc3 c (lift (S n) (0) t) x) &
-                                        (drop n (0) c (CTail e (Bind Abbr) u)) &
-                                        (ty0 g e u t)
-                            ) \/
-                            (EX e u t | (pc3 c (lift (S n) (0) u) x) &
-                                        (drop n (0) c (CTail e (Bind Abst) u)) &
-                                        (ty0 g e u t)
-                            ).
-
-(*#* #stop proof *) 
-                            
-      Intros until 1; InsertEq H '(TLRef n); XElim H; Intros.
-(* case 1 : ty0_conv *)
-      LApply H2; [ Clear H2; Intros H2 | XAuto ].
-      XElim H2; Intros; XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
-      Inversion H0.
-(* case 3 : ty0_abbr *)
-      Inversion H3 ; Rewrite H5 in H0; XEAuto.
-(* case 4 : ty0_abst *)
-      Inversion H3; Rewrite H5 in H0; XEAuto.
-(* case 5 : ty0_bind *)
-      Inversion H5.
-(* case 6 : ty0_appl *)
-      Inversion H3.
-(* case 7 : ty0_cast *)
-      Inversion H3.
-      Qed.
-
-(*#* #start proof *) 
-
-(*#* #caption "generation lemma for binders" *)
-(*#* #cap #cap c #alpha x in T, t1 in U1, t2 in U2, u in V, t in U, t0 in U3 *)
-
-      Theorem ty0_gen_bind: (g:?; b:?; c:?; u,t1,x:?) (ty0 g c (TTail (Bind b) u t1) x) ->
-                            (EX t2 t t0 | (pc3 c (TTail (Bind b) u t2) x) &
-                                          (ty0 g c u t) &
-                                          (ty0 g (CTail c (Bind b) u) t1 t2) &
-                                          (ty0 g (CTail c (Bind b) u) t2 t0)
-                            ).
-      
-(*#* #stop proof *) 
-      
-      Intros until 1; InsertEq H '(TTail (Bind b) u t1); XElim H; Intros.
-(* case 1 : ty0_conv *)
-      LApply H2; [ Clear H2; Intros H2 | XAuto ].
-      XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
-      Inversion H0.
-(* case 3 : ty0_abbr *)
-      Inversion H3.
-(* case 4 : ty0_abst *)
-      Inversion H3.
-(* case 5 : ty0_bind *)
-      Inversion H5.
-      Rewrite H7 in H1; Rewrite H7 in H3.
-      Rewrite H8 in H; Rewrite H8 in H1; Rewrite H8 in H3.
-      Rewrite H9 in H1; XEAuto.
-(* case 6 : ty0_appl *)
-      Inversion H3.
-(* case 7 : ty0_cast *)
-      Inversion H3.
-      Qed.
-
-(*#* #start proof *) 
-
-(*#* #caption "generation lemma for applications" *)
-(*#* #cap #cap c #alpha x in T, v in U1, w in V1, u in V2, t in U2 *)
-
-      Theorem ty0_gen_appl: (g:?; c:?; w,v,x:?) (ty0 g c (TTail (Flat Appl) w v) x) ->
-                            (EX u t | (pc3 c (TTail (Flat Appl) w (TTail (Bind Abst) u t)) x) &
-                                      (ty0 g c v (TTail (Bind Abst) u t)) &
-                                      (ty0 g c w u)
-                            ).
-                            
-(*#* #stop proof *) 
-                            
-      Intros until 1; InsertEq H '(TTail (Flat Appl) w v); XElim H; Intros.
-(* case 1 : ty0_conv *)
-      LApply H2; [ Clear H2; Intros H2 | XAuto ].
-      XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
-      Inversion H0.
-(* case 3 : ty0_abbr *)
-      Inversion H3.
-(* case 4 : ty0_abst *)
-      Inversion H3.
-(* case 5 : ty0_bind *)
-      Inversion H5.
-(* case 6 : ty0_appl *)
-      Inversion H3; Rewrite H5 in H; Rewrite H6 in H1; XEAuto.
-(* case 7 : ty0_cast *)
-      Inversion H3.
-      Qed.
-
-(*#* #start proof *) 
-
-(*#* #caption "generation lemma for type casts" *)
-(*#* #cap #cap c #alpha x in T, t2 in V, t1 in U *)
-
-      Theorem ty0_gen_cast: (g:?; c:?; t1,t2,x:?)
-                            (ty0 g c (TTail (Flat Cast) t2 t1) x) ->
-                            (pc3 c t2 x) /\ (ty0 g c t1 t2).
-      
-(*#* #stop proof *) 
-
-      Intros until 1; InsertEq H '(TTail (Flat Cast) t2 t1); XElim H; Intros.
-(* case 1 : ty0_conv *)
-      LApply H2; [ Clear H2; Intros H2 | XAuto ].
-      XElim H2; XEAuto.
-(* case 2 : ty0_sort *)
-      Inversion H0.
-(* case 3 : ty0_abbr *)
-      Inversion H3.
-(* case 4 : ty0_abst *)
-      Inversion H3.
-(* case 5 : ty0_bind *)
-      Inversion H5.
-(* case 6 : ty0_appl *)
-      Inversion H3.
-(* case 7 : ty0_cast *)
-      Inversion H3; Rewrite H5 in H; Rewrite H5 in H1; Rewrite H6 in H; XAuto.
-      Qed.
-
-   End ty0_gen_base.
-
-      Tactic Definition Ty0GenBase :=
-         Match Context With
-            | [ H: (ty0 ?1 ?2 (TSort ?3) ?4) |- ? ] ->
-               LApply (ty0_gen_sort ?1 ?2 ?4 ?3); [ Clear H; Intros | XAuto ]
-            | [ H: (ty0 ?1 ?2 (TLRef ?3) ?4) |- ? ] ->
-               LApply (ty0_gen_lref ?1 ?2 ?4 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros H; XElim H; Intros
-            | [ H: (ty0 ?1 ?2 (TTail (Bind ?3) ?4 ?5) ?6) |- ? ] ->
-               LApply (ty0_gen_bind ?1 ?3 ?2 ?4 ?5 ?6); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros
-            | [ H: (ty0 ?1 ?2 (TTail (Flat Appl) ?3 ?4) ?5) |- ? ] ->
-               LApply (ty0_gen_appl ?1 ?2 ?3 ?4 ?5); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros
-            | [ H: (ty0 ?1 ?2 (TTail (Flat Cast) ?3 ?4) ?5) |- ? ] ->
-               LApply (ty0_gen_cast ?1 ?2 ?4 ?3 ?5); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros.
-
-(*#* #start file *)
-
-(*#* #single *)