X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpr2_gen.v;h=98d128233687625645a20152fb3551dbc07a5afc;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6fcb00c301ea73dac68d079e73bbd0fdf36e61bd;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v
index 6fcb00c30..98d128233 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr2_gen.v
@@ -1,61 +1,60 @@
 (*#* #stop file *)
 
 Require subst0_gen.
+Require subst0_lift.
 Require drop_props.
 Require pr0_gen.
+Require pr0_subst0.
 Require pr2_defs.
 
    Section pr2_gen. (********************************************************)
 
-      Theorem pr2_gen_abbr : (c:?; u1,t1,x:?)
-                             (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
-                                         (pr2 c u1 u2) &
-                                         ((b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2)) \/
-                                         (EX y | (pr0 t1 y) & (subst0 (0) u2 y t2))
-                             ) \/
-                             (pr0 t1 (lift (1) (0) x)).
-      Intros; Inversion H;
-      Try Pr0Gen; Try Subst0Gen; XDEAuto 8.
+      Theorem pr2_gen_abbr: (c:?; u1,t1,x:?)
+                            (pr2 c (TTail (Bind Abbr) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Bind Abbr) u2 t2) &
+                                        (pr2 c u1 u2) & (OR
+                                        (b:?; u:?) (pr2 (CTail c (Bind b) u) t1 t2) |
+			        	(EX u | (pr0 u1 u) & (pr2 (CTail c (Bind Abbr) u) t1 t2)) |
+				        (EX y z | (pr2 (CTail c (Bind Abbr) u1) t1 y) & (pr0 y z) & (pr2 (CTail c (Bind Abbr) u1) z t2))
+                            )) \/ (b:?; u:?)
+			    (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)).
+      Intros; Inversion H; 
+      Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; Try Pr0Subst0; XDEAuto 10.
       Qed.
 
-      Theorem pr2_gen_void : (c:?; u1,t1,x:?)
-                             (pr2 c (TTail (Bind Void) u1 t1) x) ->
-                             (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
-                                         (pr2 c u1 u2) & (b:?; u:?)
-                                         (pr2 (CTail c (Bind b) u) t1 t2)
-                             ) \/
-                             (pr0 t1 (lift (1) (0) x)).
-      Intros; Inversion H;
-      Try Pr0Gen; Try Subst0Gen; XDEAuto 7.
+      Theorem pr2_gen_void: (c:?; u1,t1,x:?)
+                            (pr2 c (TTail (Bind Void) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Bind Void) u2 t2) &
+                                        (pr2 c u1 u2) & (b:?; u:?)
+                                        (pr2 (CTail c (Bind b) u) t1 t2)
+                            ) \/ (b:?; u:?)
+                            (pr2 (CTail c (Bind b) u) t1 (lift (1) (0) x)).
+      Intros; Inversion H; 
+      Try Pr0Gen; Try Rewrite H1 in H2; Try Subst0Gen; XDEAuto 7.
       Qed.
 
-(*#* #start file *)
-
 (*#* #caption "generation lemma for lift" *)
 (*#* #cap #cap c #alpha e in D, t1 in U1, t2 in U2, x in T, d in i *)
 
-      Theorem pr2_gen_lift : (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
-                             (e:?) (drop h d c e) ->
-                             (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
-
-(*#* #stop file *)
-
+      Theorem pr2_gen_lift: (c:?; t1,x:?; h,d:?) (pr2 c (lift h d t1) x) ->
+                            (e:?) (drop h d c e) ->
+                            (EX t2 | x = (lift h d t2) & (pr2 e t1 t2)).
       Intros.
-      Inversion H; Clear H.
-(* case 1 : pr2_pr0 *)
-      Pr0Gen; XEAuto.
+      Inversion H; Clear H; Pr0Gen.
+(* case 1 : pr2_free *)
+      XEAuto.
 (* case 2 : pr2_delta *)
+      Rewrite H in H3; Clear H H4 t t2.
       Apply (lt_le_e i d); Intros.
 (* case 2.1 : i < d *)
-      Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ].
-      Rewrite (lt_plus_minus i d) in H2; [ Idtac | XAuto ].
-      DropDis; Rewrite H0 in H2; Clear H0 u.
+      Rewrite (lt_plus_minus i d) in H0; [ Idtac | XAuto ]. 
+      Rewrite (lt_plus_minus i d) in H3; [ Idtac | XAuto ].
+      DropDis; Rewrite H0 in H3; Clear H0 u. 
       Subst0Gen; Rewrite <- lt_plus_minus in H0; XEAuto.
 (* case 2.2 : i >= d *)
       Apply (lt_le_e i (plus d h)); Intros.
 (* case 2.2.1 : i < d + h *)
-      EApply subst0_gen_lift_false; [ Apply H | Apply H3 | XEAuto ].
+      EApply subst0_gen_lift_false; [ Apply H | Apply H4 | XEAuto ].
 (* case 2.2.2 : i >= d + h *)
       DropDis; Subst0Gen; XEAuto.
       Qed.
@@ -66,16 +65,14 @@ Require pr2_defs.
          Match Context With
             | [ H: (pr2 ?1 (TTail (Bind Abbr) ?2 ?3) ?4) |- ? ] ->
                LApply (pr2_gen_abbr ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
-               XElim H;
-               [ Intros H; XElim H; Do 4 Intro; Intros H_x; XElim H_x;
-                 [ Intros | Intros H_x; XElim H_x; Intros ]
-               | Intros ]
+               XDecompose H  
             | [ H: (pr2 ?1 (TTail (Bind Void) ?2 ?3) ?4) |- ? ] ->
                LApply (pr2_gen_void ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
-               XElim H; [ Intros H; XElim H; Intros | Intros ]
+               XDecompose H
             | [ H0: (pr2 ?1 (lift ?2 ?3 ?4) ?5);
                 H1: (drop ?2 ?3 ?1 ?6) |- ? ] ->
                LApply (pr2_gen_lift ?1 ?4 ?5 ?2 ?3); [ Clear H0; Intros H0 | XAuto ];
                LApply (H0 ?6); [ Clear H0; Intros H0 | XAuto ];
-               XElim H0; Intros
+               XDecompose H0
             | _ -> Pr2GenBase.
+