we restored the scripts of \lambda\delta version 1

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
deleted file mode 100644 (file)
index 640b56f..0000000
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
+++ /dev/null
@@ -1,101 +0,0 @@
-Require Export subst0_defs.
-
-(*#* #caption "axioms for the relation $\\PrZ{}{}$",
-   "reflexivity", "compatibility", "$\\beta$-contraction", "$\\upsilon$-swap", 
-   "$\\delta$-expansion", "$\\zeta$-contraction", "$\\epsilon$-contraction"
-*)
-(*#* #cap #cap t, t1, t2 #alpha u in V, u1 in V1, u2 in V2, v1 in W1, v2 in W2, w in T, k in z *)
-
-      Inductive pr0 : T -> T -> Prop :=
-(* structural rules *)
-         | pr0_refl   : (t:?) (pr0 t t)
-         | pr0_comp   : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
-                        (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
-(* axiom rules *)
-         | pr0_beta   : (u,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
-                        (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) u t1))
-                             (TTail (Bind Abbr) v2 t2))
-         | pr0_upsilon: (b:?) ~b=Abst -> (v1,v2:?) (pr0 v1 v2) ->
-                        (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
-                        (pr0 (TTail (Flat Appl) v1 (TTail (Bind b) u1 t1))
-                             (TTail (Bind b) u2 (TTail (Flat Appl) (lift (1) (0) v2) t2)))
-         | pr0_delta  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
-                        (w:?) (subst0 (0) u2 t2 w) ->
-                        (pr0 (TTail (Bind Abbr) u1 t1) (TTail (Bind Abbr) u2 w))
-         | pr0_zeta   : (b:?) ~b=Abst -> (t1,t2:?) (pr0 t1 t2) ->
-                        (u:?) (pr0 (TTail (Bind b) u (lift (1) (0) t1)) t2)
-         | pr0_epsilon: (t1,t2:?) (pr0 t1 t2) ->
-                        (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
-
-(*#* #stop file *)
-
-      Hint pr0 : ltlc := Constructors pr0.
-
-   Section pr0_gen_base. (***************************************************)
-
-      Theorem pr0_gen_sort : (x:?; n:?) (pr0 (TSort n) x) -> x = (TSort n).
-      Intros; Inversion H; XAuto.
-      Qed.
-
-      Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
-      Intros; Inversion H; XAuto.
-      Qed.
-
-      Theorem pr0_gen_abst : (u1,t1,x:?) (pr0 (TTail (Bind Abst) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
-                                         (pr0 u1 u2) & (pr0 t1 t2)
-                             ).
-
-      Intros; Inversion H; Clear H.
-(* case 1 : pr0_refl *)
-      XEAuto.
-(* case 2 : pr0_cont *)
-      XEAuto.
-(* case 3 : pr0_zeta *)
-      XElim H4; XAuto.
-      Qed.
-
-      Theorem pr0_gen_appl : (u1,t1,x:?) (pr0 (TTail (Flat Appl) u1 t1) x) -> (OR
-                             (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
-                                         (pr0 u1 u2) & (pr0 t1 t2)
-                             ) |
-                             (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
-                                               x = (TTail (Bind Abbr) u2 t2) &
-                                               (pr0 u1 u2) & (pr0 z1 t2)
-                             ) |
-                             (EX b y1 z1 u2 v2 t2 |
-                                ~b=Abst &
-                                t1 = (TTail (Bind b) y1 z1) &
-                                x = (TTail (Bind b) v2 (TTail (Flat Appl) (lift (1) (0) u2) t2)) &
-                                (pr0 u1 u2) & (pr0 y1 v2) & (pr0 z1 t2))
-                             ).
-      Intros; Inversion H; XEAuto.
-      Qed.
-
-      Theorem pr0_gen_cast : (u1,t1,x:?) (pr0 (TTail (Flat Cast) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
-                                         (pr0 u1 u2) & (pr0 t1 t2)
-                             ) \/
-                            (pr0 t1 x).
-      Intros; Inversion H; XEAuto.
-      Qed.
-
-   End pr0_gen_base.
-
-      Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
-
-      Tactic Definition Pr0GenBase :=
-         Match Context With
-            | [ H: (pr0 (TSort ?1) ?2) |- ? ] ->
-              LApply (pr0_gen_sort ?2 ?1); [ Clear H; Intros | XAuto ]
-            | [ H: (pr0 (TLRef ?1) ?2) |- ? ] ->
-              LApply (pr0_gen_lref ?2 ?1); [ Clear H; Intros | XAuto ]        
-           | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
-               LApply (pr0_gen_abst ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros
-            | [ H: (pr0 (TTail (Flat Appl) ?1 ?2) ?3) |- ? ] ->
-               LApply (pr0_gen_appl ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros H; XElim H; Intros
-            | [ H: (pr0 (TTail (Flat Cast) ?1 ?2) ?3) |- ? ] ->
-               LApply (pr0_gen_cast ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; [ Intros H; XElim H; Intros | Intros ].