we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v
deleted file mode 100644 (file)
index 073a328..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/ty0_defs.v
+++ /dev/null
@@ -1,125 +0,0 @@
-Require Export pc3_defs.
-
-(*#* #stop record *)
-
-      Record G : Set := {
-         next     : nat -> nat;
-        base     : nat;
-         next_lt  : (n:?) (lt n (next n));
-        base_next: (n:?) (le base n) -> (next n) = (S n)
-      }.
-
-(*#* #start record *)
-
-(*#* #caption "current axioms for typing",
-   "well formed context sort", "well formed context binder", 
-   "conversion rule", "typed sort", "typed reference to abbreviation",
-   "typed reference to abstraction", "typed binder", "typed application", 
-   "typed cast" 
-*)
-(*#* #cap #cap c, d, t, t0, t1, t2, w #alpha m in h, n in i, u in V, v in U *)
-
-      Inductive wf0 [g:G] : C -> Prop :=
-         | wf0_sort: (m:?) (wf0 g (CSort m))
-         | wf0_bind: (c:?; u,t:?) (ty0 g c u t) ->
-                     (b:?) (wf0 g (CTail c (Bind b) u))
-      with ty0 [g:G] : C -> T -> T -> Prop :=
-(* structural rules *)
-         | ty0_conv: (c:?; t2,t:?) (ty0 g c t2 t) ->
-                     (u,t1:?) (ty0 g c u t1) -> (pc3 c t1 t2) ->
-                     (ty0 g c u t2)
-(* axiom rules *)
-         | ty0_sort: (c:?) (wf0 g c) ->
-                     (m:?) (ty0 g c (TSort m) (TSort (next g m)))
-         | ty0_abbr: (c:?) (wf0 g c) ->
-                     (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abbr) u)) ->
-                     (t:?) (ty0 g d u t) ->
-                     (ty0 g c (TLRef n) (lift (S n) (0) t))
-         | ty0_abst: (c:?) (wf0 g c) ->
-                     (n:?; d:?; u:?) (drop n (0) c (CTail d (Bind Abst) u)) ->
-                     (t:?) (ty0 g d u t) ->
-                     (ty0 g c (TLRef n) (lift (S n) (0) u))
-         | ty0_bind: (c:?; u,t:?) (ty0 g c u t) ->
-                     (b:?; t1,t2:?) (ty0 g (CTail c (Bind b) u) t1 t2) ->
-                     (t0:?) (ty0 g (CTail c (Bind b) u) t2 t0) ->
-                     (ty0 g c (TTail (Bind b) u t1) (TTail (Bind b) u t2))
-         | ty0_appl: (c:?; w,u:?) (ty0 g c w u) ->
-                     (v,t:?) (ty0 g c v (TTail (Bind Abst) u t)) ->
-                     (ty0 g c (TTail (Flat Appl) w v)
-                              (TTail (Flat Appl) w (TTail (Bind Abst) u t))
-                     )
-         | ty0_cast: (c:?; t1,t2:?) (ty0 g c t1 t2) ->
-                     (t0:?) (ty0 g c t2 t0) ->
-                     (ty0 g c (TTail (Flat Cast) t2 t1) t2).
-
-(*#* #stop file *)
-
-      Hint wf0 : ltlc := Constructors wf0.
-
-      Hint ty0 : ltlc := Constructors ty0.
-
-   Section wf0_props. (******************************************************)
-
-      Theorem wf0_ty0: (g:?; c:?; u,t:?) (ty0 g c u t) -> (wf0 g c).
-      Intros; XElim H; XAuto.
-      Qed.
-
-      Hints Resolve wf0_ty0 : ltlc.
-
-      Theorem wf0_drop_O: (c,e:?; h:?) (drop h (0) c e) ->
-                          (g:?) (wf0 g c) -> (wf0 g e).
-      XElim c.
-(* case 1 : CSort *)
-      Intros; DropGenBase; Rewrite H; XAuto.
-(* case 2 : CTail k *)
-      Intros c IHc; XElim k; (
-      XElim h; Intros; DropGenBase;
-      [ Rewrite H in H0; XAuto | Inversion H1; XEAuto ] ).
-      Qed.
-
-   End wf0_props.
-
-      Hints Resolve wf0_ty0 wf0_drop_O : ltlc.
-
-      Tactic Definition Wf0Ty0 :=
-         Match Context With
-            [ _: (ty0 ?1 ?2 ?3 ?4) |- ? ] ->
-               LApply (wf0_ty0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
-               Inversion_clear H_x.
-
-      Tactic Definition Wf0DropO :=
-         Match Context With
-            | [ _: (drop ?1 (0) ?2 ?3); _: (wf0 ?4 ?2) |- ? ] ->
-               LApply (wf0_drop_O ?2 ?3 ?1); [ Intros H_x | XAuto ];
-               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
-
-   Section wf0_facilities. (*************************************************)
-
-      Theorem wf0_drop_wf0: (g:?; c:?) (wf0 g c) ->
-                            (b:?; e:?; u:?; h:?)
-                            (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
-      Intros.
-      Wf0DropO; Inversion H1; XEAuto.
-      Qed.
-
-      Theorem ty0_drop_wf0: (g:?; c:?; t1,t2:?) (ty0 g c t1 t2) ->
-                            (b:?; e:?; u:?; h:?)
-                            (drop h (0) c (CTail e (Bind b) u)) -> (wf0 g e).
-      Intros.
-      EApply wf0_drop_wf0; [ Idtac | EApply H0 ]; XEAuto.
-      Qed.
-
-   End wf0_facilities.
-
-      Hints Resolve wf0_drop_wf0 ty0_drop_wf0 : ltlc.
-
-      Tactic Definition DropWf0 :=
-         Match Context With
-            | [ _: (ty0 ?1 ?2 ?3 ?4);
-                _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
-               LApply (ty0_drop_wf0 ?1 ?2 ?3 ?4); [ Intros H_x | XAuto ];
-               LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ]
-            | [ _: (wf0 ?1 ?2);
-                _: (drop ?5 (0) ?2 (CTail ?6 (Bind ?7) ?8)) |- ? ] ->
-               LApply (wf0_drop_wf0 ?1 ?2); [ Intros H_x | XAuto ];
-               LApply (H_x ?7 ?6 ?8 ?5); [ Clear H_x; Intros | XAuto ].