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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v
index a650dd26f..9dab9cafe 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_defs.v
@@ -1,120 +1,137 @@
-(*#* #stop file *)
-
 Require Export drop_defs.
 Require Export pr0_defs.
 
-      Inductive pr2 [c:C; t1,t2:T] : Prop :=
+(*#* #caption "current axioms for the relation $\\PrS{}{}{}$",
+   "context-free case", "context-dependent $\\delta$-expansion" 
+*)
+(*#* #cap #cap c, d, t, t1, t2 #alpha u in V *)
+
+      Inductive pr2 [c:C; t1:T] : T -> Prop :=
 (* structural rules *)
-         | pr2_pr0   : (pr0 t1 t2) -> (pr2 c t1 t2)
+         | pr2_free : (t2:?) (pr0 t1 t2) -> (pr2 c t1 t2)
 (* axiom rules *)
-         | pr2_delta : (d:?; u:?; i:?)
-                       (drop i (0) c (CTail d (Bind Abbr) u)) ->
-                       (subst0 i u t1 t2) -> (pr2 c t1 t2).
+         | pr2_delta: (d:?; u:?; i:?)
+                      (drop i (0) c (CTail d (Bind Abbr) u)) ->
+                      (t2:?) (pr0 t1 t2) -> (t:?) (subst0 i u t2 t) -> 
+		      (pr2 c t1 t).
+
+(*#* #stop file *)
 
       Hint pr2 : ltlc := Constructors pr2.
 
    Section pr2_gen_base. (***************************************************)
 
-      Theorem pr2_gen_sort : (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
-                             x = (TSort n).
-      Intros; Inversion H;
-      Try Subst0GenBase; XEAuto.
+      Theorem pr2_gen_sort: (c:?; x:?; n:?) (pr2 c (TSort n) x) ->
+                            x = (TSort n).
+      Intros; Inversion H; Pr0GenBase;
+      [ XAuto | Rewrite H1 in H2; Subst0GenBase ].
       Qed.
 
-      Theorem pr2_gen_bref : (c:?; x:?; n:?) (pr2 c (TBRef n) x) ->
-                             x = (TBRef n) \/
-                             (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
-                                        x = (lift (S n) (0) u)
-                             ).
-      Intros; Inversion H;
-      Try Subst0GenBase; Try Rewrite <- H1 in H0; XEAuto.
+      Theorem pr2_gen_lref: (c:?; x:?; n:?) (pr2 c (TLRef n) x) ->
+                            x = (TLRef n) \/
+                            (EX d u | (drop n (0) c (CTail d (Bind Abbr) u)) &
+                                       x = (lift (S n) (0) u)
+                            ).
+      Intros; Inversion H; Pr0GenBase; 
+      [ XAuto | Rewrite H1 in H2; Subst0GenBase; Rewrite <- H2 in H0; XEAuto ].
       Qed.
 
-      Theorem pr2_gen_abst : (c:?; u1,t1,x:?)
-                             (pr2 c (TTail (Bind Abst) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
-                                         (pr2 c u1 u2) & (b:?; u:?)
-                                         (pr2 (CTail c (Bind b) u) t1 t2)
-                             ).
-      Intros; Inversion H;
-      Try Pr0GenBase; Try Subst0GenBase; XDEAuto 6.
+      Theorem pr2_gen_abst: (c:?; u1,t1,x:?)
+                            (pr2 c (TTail (Bind Abst) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
+                                        (pr2 c u1 u2) & (b:?; u:?)
+                                        (pr2 (CTail c (Bind b) u) t1 t2)
+                            ).
+      Intros; Inversion H; Pr0GenBase;
+      [ XEAuto | Rewrite H1 in H2; Subst0GenBase; XDEAuto 6 ].
       Qed.
 
-      Theorem pr2_gen_appl : (c:?; u1,t1,x:?)
-                             (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
-                             (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
-                                         (pr2 c u1 u2) & (pr2 c 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;
-      Try Pr0GenBase; Try Subst0GenBase; XEAuto.
+      Theorem pr2_gen_appl: (c:?; u1,t1,x:?)
+                            (pr2 c (TTail (Flat Appl) u1 t1) x) -> (OR
+                            (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+                                        (pr2 c u1 u2) & (pr2 c t1 t2)
+                            ) |
+                            (EX y1 z1 u2 t2 | t1 = (TTail (Bind Abst) y1 z1) &
+                                              x = (TTail (Bind Abbr) u2 t2) &
+                                              (pr2 c u1 u2) & (b:?; u:?) 
+					      (pr2 (CTail c (Bind b) u) z1 t2)
+                            ) |
+                            (EX b y1 z1 z2 u2 v2 t2 |
+                               ~b=Abst &
+                               t1 = (TTail (Bind b) y1 z1) &
+                               x = (TTail (Bind b) v2 z2) & 
+                               (pr2 c u1 u2) & (pr2 c y1 v2) & (pr0 z1 t2))
+                            ).
+      Intros; Inversion H; Pr0GenBase;
+      Try Rewrite H1 in H2; Try Rewrite H4 in H2; Try Rewrite H5 in H2; 
+      Try Subst0GenBase; XDEAuto 7.
       Qed.
 
-      Theorem pr2_gen_cast : (c:?; u1,t1,x:?)
-                             (pr2 c (TTail (Flat Cast) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
-                                         (pr2 c u1 u2) & (pr2 c t1 t2)
-                             ) \/
-                            (pr0 t1 x).
-      Intros; Inversion H;
-      Try Pr0GenBase; Try Subst0GenBase; XEAuto.
+      Theorem pr2_gen_cast: (c:?; u1,t1,x:?)
+                            (pr2 c (TTail (Flat Cast) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+                                        (pr2 c u1 u2) & (pr2 c t1 t2)
+                            ) \/
+                            (pr2 c t1 x).
+      Intros; Inversion H; Pr0GenBase; 
+      Try Rewrite H1 in H2; Try Subst0GenBase; XEAuto. 
       Qed.
 
    End pr2_gen_base.
 
       Tactic Definition Pr2GenBase :=
          Match Context With
-            | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
+            | [ H: (pr2 ?1 (TSort ?2) ?3) |- ? ] ->
+               LApply (pr2_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
+            | [ H: (pr2 ?1 (TLRef ?2) ?3) |- ? ] ->
+               LApply (pr2_gen_lref ?1 ?3 ?2); [ Clear H; Intros H | XAuto ];
+	       XDecompose H 
+	    | [ H: (pr2 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
                LApply (pr2_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros.
+               XDecompose H
+	    | [ H: (pr2 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
+               LApply (pr2_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+               XDecompose H
+	    | [ H: (pr2 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
+               LApply (pr2_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+               XDecompose H.
 
    Section pr2_props. (******************************************************)
 
-      Theorem pr2_thin_dx : (c:?; t1,t2:?) (pr2 c t1 t2) ->
-                            (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
-                                              (TTail (Flat f) u t2)).
-      Intros; Inversion H; XEAuto.
+      Theorem pr2_thin_dx: (c:?; t1,t2:?) (pr2 c t1 t2) ->
+                           (u:?; f:?) (pr2 c (TTail (Flat f) u t1)
+                                             (TTail (Flat f) u t2)).
+      Intros; XElim H; XEAuto.
       Qed.
 
-      Theorem pr2_tail_1 : (c:?; u1,u2:?) (pr2 c u1 u2) ->
-                           (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
-      Intros; Inversion H; XEAuto.
+      Theorem pr2_tail_1: (c:?; u1,u2:?) (pr2 c u1 u2) ->
+                          (k:?; t:?) (pr2 c (TTail k u1 t) (TTail k u2 t)).
+      Intros; XElim H; XEAuto.
       Qed.
 
-      Theorem pr2_tail_2 : (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
-                           (pr2 c (TTail k u t1) (TTail k u t2)).
-      XElim k; Intros;
-      (Inversion H; [ XAuto | Clear H ];
-      (NewInduction i; DropGenBase; [ Inversion H; XEAuto | XEAuto ])).
+      Theorem pr2_tail_2: (c:?; u,t1,t2:?; k:?) (pr2 (CTail c k u) t1 t2) ->
+                          (pr2 c (TTail k u t1) (TTail k u t2)).
+      XElim k; Intros; (
+      XElim H; [ XAuto | XElim i; Intros; DropGenBase; CGenBase; XEAuto ]).
       Qed.
-
+      
       Hints Resolve pr2_tail_2 : ltlc.
 
-      Theorem pr2_shift : (i:?; c,e:?) (drop i (0) c e) ->
-                          (t1,t2:?) (pr2 c t1 t2) ->
-                          (pr2 e (app c i t1) (app c i t2)).
+      Theorem pr2_shift: (i:?; c,e:?) (drop i (0) c e) ->
+                         (t1,t2:?) (pr2 c t1 t2) ->
+                         (pr2 e (app c i t1) (app c i t2)).
       XElim i.
-(* case 1 : i = 0 *)
-      Intros.
-      DropGenBase; Rewrite H in H0.
+(* case 1: i = 0 *)
+      Intros; DropGenBase; Rewrite H in H0.
       Repeat Rewrite app_O; XAuto.
-(* case 2 : i > 0 *)
+(* case 2: i > 0 *)
       XElim c.
-(* case 2.1 : CSort *)
+(* case 2.1: CSort *)
       Intros; DropGenBase; Rewrite H0; XAuto.
-(* case 2.2 : CTail *)
+(* case 2.2: CTail *)
       XElim k; Intros; Simpl; DropGenBase; XAuto.
       Qed.
-
+      
    End pr2_props.
 
       Hints Resolve pr2_thin_dx pr2_tail_1 pr2_tail_2 pr2_shift : ltlc.