X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr0_defs.v;h=640b56f1f02fd01759f4870f8d2a69b4b93b9ede;hb=97c2d258a5c524eb5c4b85208899d80751a2c82f;hp=3c7a96bbe3b2a081fec712691f7984f2001cd4e4;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
index 3c7a96bbe..640b56f1f 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr0_defs.v
@@ -1,37 +1,43 @@
-(*#* #stop file *)
-
 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_thin  : (u1,u2:?) (pr0 u1 u2) -> (t1,t2:?) (pr0 t1 t2) ->
-                       (k:?) (pr0 (TTail k u1 t1) (TTail k u2 t2))
+         | 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  : (k,v1,v2:?) (pr0 v1 v2) -> (t1,t2:?) (pr0 t1 t2) ->
-                       (pr0 (TTail (Flat Appl) v1 (TTail (Bind Abst) k t1))
-                            (TTail (Bind Abbr) v2 t2))
-         | pr0_gamma : (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_eps   : (t1,t2:?) (pr0 t1 t2) ->
-                       (u:?) (pr0 (TTail (Flat Cast) u t1) t2).
+         | 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. (********************************************************)
+   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_bref : (x:?; n:?) (pr0 (TBRef n) x) -> x = (TBRef n).
+      Theorem pr0_gen_lref : (x:?; n:?) (pr0 (TLRef n) x) -> x = (TLRef n).
       Intros; Inversion H; XAuto.
       Qed.
 
@@ -74,13 +80,17 @@ Require Export subst0_defs.
       Intros; Inversion H; XEAuto.
       Qed.
 
-   End pr0_gen.
+   End pr0_gen_base.
 
-      Hints Resolve pr0_gen_sort pr0_gen_bref : ltlc.
+      Hints Resolve pr0_gen_sort pr0_gen_lref : ltlc.
 
       Tactic Definition Pr0GenBase :=
          Match Context With
-            | [ H: (pr0 (TTail (Bind Abst) ?1 ?2) ?3) |- ? ] ->
+            | [ 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) |- ? ] ->