we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
deleted file mode 100644 (file)
index ab4b006..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_props.v
+++ /dev/null
@@ -1,110 +0,0 @@
-Require drop_props.
-Require pc3_props.
-Require ty0_defs.
-Require ty0_gen.
-Require ty0_lift.
-
-   Section ty0_correct. (****************************************************)
-
-(*#* #caption "correctness of types" *)
-(*#* #cap #cap c, t1, t2  #alpha t in T3 *)
-
-      Theorem ty0_correct : (g:?; c:?; t1,t2:?)
-                            (ty0 g c t1 t2) -> (EX t | (ty0 g c t2 t)).
-
-(*#* #stop file *)
-
-      Intros; XElim H; Intros.
-(* case 1 : ty0_conv *)
-      XEAuto.
-(* case 2 : ty0_sort *)
-      XEAuto.
-(* case 3 : ty0_abbr *)
-      XElim H2; XEAuto.
-(* case 4 : ty0_abst *)
-      XEAuto.
-(* case 5 : ty0_bind *)
-      XElim H4; XEAuto.
-(* case 6 : ty0_appl *)
-      XElim H0; XElim H2; Intros.
-      Ty0GenBase; XEAuto.
-(* case 7 : ty0_cast *)
-      XAuto.
-      Qed.
-
-   End ty0_correct.
-
-      Tactic Definition Ty0Correct :=
-         Match Context With
-            [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
-               LApply (ty0_correct ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
-               XElim H_x; Intros.
-
-(*#* #start file *)
-
-   Section ty0_shift. (******************************************************)
-
-(*#* #caption "shift lemma for types" *)
-(*#* #cap #cap t1, t2 #alpha c in C1, e in C2 *)
-
-      Theorem ty0_shift : (h:?; c,e:?) (drop h (0) c e) ->
-                          (g:?; t1,t2:?) (ty0 g c t1 t2) -> (wf0 g e) ->
-                          (ty0 g e (app c h t1) (app c h t2)).
-
-(*#* #stop file *)
-
-      XElim h.
-(* case 1 : h = 0 *)
-      Intros; DropGenBase; Rewrite <- H.
-      Repeat Rewrite app_O; XAuto.
-(* case 2 : h > 0 *)
-      Intros h IHh; XElim c.
-(* case 2.1 : CSort *)
-      Intros; DropGenBase; Rewrite H.
-      Simpl; XAuto.
-(* case 2.2 : CTail k *)
-      Intros c IHc; Clear IHc; XElim k; Intros; Wf0Ty0.
-      DropGenBase; Move H0 after H2; Ty0Correct.
-      Simpl; Apply IHh; [ Idtac | EApply ty0_bind | Idtac ]; XEAuto.
-      Qed.
-
-   End ty0_shift.
-
-      Hints Resolve ty0_shift : ltlc.
-
-   Section ty0_unique. (*****************************************************)
-
-      Opaque pc3.
-
-(*#* #start file *)
-
-(*#* #caption "uniqueness of types" *)
-(*#* #cap #cap c, t1, t2 #alpha u in T *)
-
-      Theorem ty0_unique : (g:?; c:?; u,t1:?) (ty0 g c u t1) ->
-                           (t2:?) (ty0 g c u t2) -> (pc3 c t1 t2).
-
-(*#* #stop file *)
-
-      Intros until 1; XElim H; Intros.
-(* case 1 : ty0_conv *)
-      XEAuto.
-(* case 2 : ty0_sort *)
-      Ty0GenBase; XAuto.
-(* case 3 : ty0_abbr *)
-      Ty0GenBase; DropDis; Inversion H4.
-      Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
-(* case 4 : ty0_abst *)
-      Ty0GenBase; DropDis; Inversion H4.
-      Rewrite H7 in H2; Rewrite H8 in H2; XEAuto.
-(* case 5 : ty0_bind *)
-      Ty0GenBase; XEAuto.
-(* case 6 : ty0_appl *)
-      Ty0GenBase; EApply pc3_t; [ Idtac | EApply H3 ]; XEAuto.
-(* case 7 : ty0_cast *)
-      Ty0GenBase; XEAuto.
-      Qed.
-
-   End ty0_unique.
-
-      Hints Resolve ty0_unique : ltlc.