X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fcoq-contribs%2FLAMBDA-TYPES%2Fpc3_gen.v;h=8a27227e6d0607ae1dd6a0a8ca1a9bf68158d9b4;hb=5a7ff7a3ce24bd14385d2295a1c77fad4b876cb8;hp=4e5dabaaa45b06c467bb9ef77e27b294096c7f94;hpb=1b21075e987872a2e3103203b4e67c939e4a9f6a;p=helm.git

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v
index 4e5dabaaa..8a27227e6 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_gen.v
@@ -8,16 +8,22 @@ Require pc3_props.
 
    Section pc3_gen. (********************************************************)
 
-      Theorem pc3_gen_abst : (c:?; u1,u2,t1,t2:?)
-                             (pc3 c (TTail (Bind Abst) u1 t1)
-                                    (TTail (Bind Abst) u2 t2)
-                             ) ->
-                             (pc3 c u1 u2) /\
-                             (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
+      Theorem pc3_gen_sort: (c:?; m,n:?) (pc3 c (TSort m) (TSort n)) -> m = n.
+      Intros; Pc3Unfold; Repeat Pr3GenBase.
+      Rewrite H0 in H; Clear H0 x c.
+      TGenBase; XAuto.
+      Qed.
+
+      Theorem pc3_gen_abst: (c:?; u1,u2,t1,t2:?)
+                            (pc3 c (TTail (Bind Abst) u1 t1)
+                                   (TTail (Bind Abst) u2 t2)
+                            ) ->
+                            (pc3 c u1 u2) /\
+                            (b:?; u:?) (pc3 (CTail c (Bind b) u) t1 t2).
       Intros.
-      Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H0 in H; Clear H0 x.
-      Inversion H; Rewrite H5 in H1; Rewrite H6 in H2.
-      Split; XEAuto.
+      Pc3Unfold; Repeat Pr3GenBase; Rewrite H1 in H; Clear H1 x.
+      TGenBase; Rewrite H1 in H4; Rewrite H6 in H5.
+      XEAuto.
       Qed.
 
       Theorem pc3_gen_lift: (c:?; t1,t2:?; h,d:?)
@@ -25,43 +31,44 @@ Require pc3_props.
                             (e:?) (drop h d c e) ->
                             (pc3 e t1 t2).
       Intros.
-      Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
-      LiftGen; Rewrite H in H2; XEAuto.
+      Pc3Unfold; Repeat Pr3Gen; Rewrite H2 in H; Clear H2 x.
+      LiftGen; Rewrite H in H4; XEAuto.
       Qed.
 
-      Theorem pc3_gen_not_abst : (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
-                                 (pc3 c (TTail (Bind b) u1 t1)
-                                        (TTail (Bind Abst) u2 t2)
-                                 ) ->
-                                 (pc3 (CTail c (Bind b) u1) t1
-                                      (lift (1) (0) (TTail (Bind Abst) u2 t2))
-                                 )
-             .
-      Intros b; XElim b; Intros;
-      Try EqFalse; Pc3Confluence; Pr3Gen; Pr3Gen;
-      Try (Rewrite H1 in H0; Inversion H0);
-      Rewrite H1 in H4; Pr3Context;
+      Theorem pc3_gen_not_abst: (b:?) ~b=Abst -> (c:?; t1,t2,u1,u2:?)
+                                (pc3 c (TTail (Bind b) u1 t1)
+                                       (TTail (Bind Abst) u2 t2)
+                                ) ->
+                                (pc3 (CTail c (Bind b) u1) t1
+                                     (lift (1) (0) (TTail (Bind Abst) u2 t2))
+                                ).
+      XElim b; Intros;
+      Try EqFalse; Pc3Unfold; Repeat Pr3Gen;
+      Try (Rewrite H0 in H3; TGenBase);
+      Rewrite H1 in H0; Clear H H1 x;
       EApply pc3_pr3_t; XEAuto.
       Qed.
 
-      Theorem pc3_gen_lift_abst : (c:?; t,t2,u2:?; h,d:?)
-                                  (pc3 c (lift h d t)
-                                         (TTail (Bind Abst) u2 t2)
-                                  ) ->
-                                  (e:?) (drop h d c e) ->
-                                  (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
-                                              (pr3 c u2 (lift h d u1)) &
-                                              (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
-                                  ).
+      Theorem pc3_gen_lift_abst: (c:?; t,t2,u2:?; h,d:?)
+                                 (pc3 c (lift h d t)
+                                        (TTail (Bind Abst) u2 t2)
+                                 ) ->
+                                 (e:?) (drop h d c e) ->
+                                 (EX u1 t1 | (pr3 e t (TTail (Bind Abst) u1 t1)) &
+                                             (pr3 c u2 (lift h d u1)) &
+                                             (b:B; u:T)(pr3 (CTail c (Bind b) u) t2 (lift h (S d) t1))
+                                 ).
       Intros.
-      Pc3Confluence; Pr3Gen; Pr3Gen; Rewrite H1 in H; Clear H1 x.
-      LiftGenBase; Rewrite H in H4; Rewrite H1 in H2; Rewrite H5 in H3; XEAuto.
+      Pc3Unfold; Repeat Pr3Gen; Rewrite H1 in H; Clear H1 x.
+      LiftGenBase; Rewrite H in H3; Rewrite H1 in H4; Rewrite H2 in H5; XEAuto.
       Qed.
 
    End pc3_gen.
 
       Tactic Definition Pc3Gen :=
          Match Context With
+	    | [H: (pc3 ?1 (TSort ?2) (TSort ?3)) |- ? ] ->
+	       LApply (pc3_gen_sort ?1 ?2 ?3); [ Clear H; Intros | XAuto ]
             | [ _: (pc3 ?1 (lift ?2 ?3 ?4) (lift ?2 ?3 ?5));
                 _: (drop ?2 ?3 ?1 ?6) |- ? ] ->
                LApply (pc3_gen_lift ?1 ?4 ?5 ?2 ?3); [ Intros H_x | XAuto ];
@@ -77,4 +84,5 @@ Require pc3_props.
                 _: (drop ?2 ?3 ?1 ?7) |- ? ] ->
                LApply (pc3_gen_lift_abst ?1 ?4 ?6 ?5 ?2 ?3); [ Intros H_x | XAuto ];
                LApply (H_x ?7); [ Clear H_x; Intros H_x | XAuto ];
-               XElim H_x; Intros.
+               XElim H_x; Intros
+	    | _ -> Pr3Gen.