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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
index 1d67abfb1..df6764b3f 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pr3_defs.v
@@ -1,67 +1,186 @@
-(*#* #stop file *)
-
 Require Export pr1_defs.
 Require Export pr2_defs.
 
+(*#* #caption "axioms for the relation $\\PrT{}{}{}$",
+   "reflexivity", "single step transitivity" 
+*)
+(*#* #cap #cap c, t, t1, t2, t3 *)
+
       Inductive pr3 [c:C] : T -> T -> Prop :=
-         | pr3_r : (t:?) (pr3 c t t)
-         | pr3_u : (t2,t1:?) (pr2 c t1 t2) ->
-                   (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+         | pr3_refl: (t:?) (pr3 c t t)
+         | pr3_sing: (t2,t1:?) (pr2 c t1 t2) ->
+                     (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
+
+(*#* #stop file *)
 
       Hint pr3: ltlc := Constructors pr3.
 
+   Section pr3_gen_base. (***************************************************)
+
+      Theorem pr3_gen_sort: (c:?; x:?; n:?) (pr3 c (TSort n) x) ->
+                            x = (TSort n).
+      Intros; InsertEq H '(TSort n); XElim H; Clear y x; Intros.
+(* case 1: pr3_refl *)
+      XAuto.
+(* case 2: pr3_sing *)
+      Rewrite H2 in H; Clear H2 t1; Pr2GenBase; XAuto.
+      Qed.
+
+      Tactic Definition IH :=
+         Match Context With
+            | [ H: (u,t:T) (TTail (Bind Abst) ?1 ?2) = (TTail (Bind Abst) u t) -> ? |- ? ] ->
+               LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+               XDecompose H
+            | [ H: (u,t:T) (TTail (Flat Appl) ?1 ?2) = (TTail (Flat Appl) u t) -> ? |- ? ] ->
+               LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+               XDecompose H
+            | [ H: (u,t:T) (TTail (Flat Cast) ?1 ?2) = (TTail (Flat Cast) u t) -> ? |- ? ] ->
+               LApply (H ?1 ?2); [ Clear H; Intros H | XAuto ];
+               XDecompose H.
+
+      Theorem pr3_gen_abst: (c:?; u1,t1,x:?)
+                            (pr3 c (TTail (Bind Abst) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Bind Abst) u2 t2) &
+                                        (pr3 c u1 u2) & (b:?; u:?)
+                                        (pr3 (CTail c (Bind b) u) t1 t2)
+                            ).
+      Intros until 1; InsertEq H '(TTail (Bind Abst) u1 t1);
+      UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
+      Rename x into u0; Rename x0 into t0.
+(* case 1 : pr3_refl *)
+      XEAuto.
+(* case 2 : pr3_sing *)
+      Rewrite H2 in H; Clear H0 H2 t1; Pr2GenBase. 
+      Rewrite H0 in H1; Clear H0 t2; IH; XEAuto.
+      Qed.
+
+      Theorem pr3_gen_appl: (c:?; u1,t1,x:?)
+                            (pr3 c (TTail (Flat Appl) u1 t1) x) -> (OR
+                            (EX u2 t2 | x = (TTail (Flat Appl) u2 t2) &
+                                        (pr3 c u1 u2) & (pr3 c t1 t2)
+                            ) |
+                            (EX y1 z1 u2 t2 | (pr3 c (TTail (Bind Abbr) u2 t2) x) &
+			                      (pr3 c u1 u2) & 
+			       	              (pr3 c t1 (TTail (Bind Abst) y1 z1)) &
+                                              (b:?; u:?) (pr3 (CTail c (Bind b) u) z1 t2)
+                            ) |
+                            (EX b y1 z1 z2 u2 v2 t2 | 
+			       (pr3 c (TTail (Bind b) v2 z2) x) & ~b=Abst &
+                               (pr3 c u1 u2) & 
+			       (pr3 c t1 (TTail (Bind b) y1 z1)) &
+                               (pr3 c y1 v2) & (pr0 z1 t2))
+                            ).
+      Intros; InsertEq H '(TTail (Flat Appl) u1 t1).
+      UnIntro t1 H; UnIntro u1 H.
+      XElim H; Clear y x; Intros; 
+      Rename x into u0; Rename x0 into t0.
+(* case 1: pr3_refl *)
+      XEAuto.
+(* case 2: pr3_sing *)
+      Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: short step: compatibility *)
+      Rewrite H3 in H1; Clear H0 H3 t2.
+      IH; Try (Rewrite H0; Clear H0 t3); XDEAuto 6.
+(* case 2.2: short step: beta *)
+      Rewrite H4 in H0; Rewrite H3; Clear H1 H3 H4 t0 t2; XEAuto.
+(* case 2.3: short step: upsilon *)
+      Rewrite H5 in H0; Rewrite H4; Clear H1 H4 H5 t0 t2; XEAuto.
+      Qed.
+
+      Theorem pr3_gen_cast: (c:?; u1,t1,x:?)
+                            (pr3 c (TTail (Flat Cast) u1 t1) x) ->
+                            (EX u2 t2 | x = (TTail (Flat Cast) u2 t2) &
+                                        (pr3 c u1 u2) & (pr3 c t1 t2)
+                            ) \/
+                            (pr3 c t1 x).
+      Intros; InsertEq H '(TTail (Flat Cast) u1 t1); 
+      UnIntro H t1; UnIntro H u1; XElim H; Clear y x; Intros;
+      Rename x into u0; Rename x0 into t0.
+(* case 1: pr3_refl *)
+      Rewrite H; Clear H t; XEAuto.
+(* case 2: pr3_sing *)
+      Rewrite H2 in H; Clear H2 t1; Pr2GenBase.
+(* case 2.1: short step: compatinility *)
+      Rewrite H3 in H1; Clear H0 H3 t2; 
+      IH; Try Rewrite H0; XEAuto.
+(* case 2.2: short step: epsilon *)
+      XEAuto.
+      Qed.
+      
+   End pr3_gen_base.
+
+      Tactic Definition Pr3GenBase :=
+         Match Context With
+            | [ H: (pr3 ?1 (TSort ?2) ?3) |- ? ] ->
+               LApply (pr3_gen_sort ?1 ?3 ?2); [ Clear H; Intros | XAuto ]
+            | [ H: (pr3 ?1 (TTail (Bind Abst) ?2 ?3) ?4) |- ? ] ->
+               LApply (pr3_gen_abst ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+               XDecompose H
+            | [ H: (pr3 ?1 (TTail (Flat Appl) ?2 ?3) ?4) |- ? ] ->
+               LApply (pr3_gen_appl ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+               XDecompose H
+	    | [ H: (pr3 ?1 (TTail (Flat Cast) ?2 ?3) ?4) |- ? ] ->
+               LApply (pr3_gen_cast ?1 ?2 ?3 ?4); [ Clear H; Intros H | XAuto ];
+               XDecompose H.
+
    Section pr3_props. (******************************************************)
 
-      Theorem pr3_pr2 : (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
+      Theorem pr3_pr2: (c,t1,t2:?) (pr2 c t1 t2) -> (pr3 c t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pr3_t : (t2,t1,c:?) (pr3 c t1 t2) ->
+      Theorem pr3_t: (t2,t1,c:?) (pr3 c t1 t2) ->
                       (t3:?) (pr3 c t2 t3) -> (pr3 c t1 t3).
       Intros until 1; XElim H; XEAuto.
       Qed.
 
-      Theorem pr3_tail_1 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
-                           (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
+      Theorem pr3_thin_dx: (c:?; t1,t2:?) (pr3 c t1 t2) ->
+                           (u:?; f:?) (pr3 c (TTail (Flat f) u t1)
+                                             (TTail (Flat f) u t2)).
+      Intros; XElim H; XEAuto.
+      Qed.
+
+      Theorem pr3_tail_1: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                          (k:?; t:?) (pr3 c (TTail k u1 t) (TTail k u2 t)).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
-      EApply pr3_u; [ Apply pr2_tail_1; Apply H | XAuto ].
+(* case 2: pr3_sing *)
+      EApply pr3_sing; [ Apply pr2_tail_1; Apply H | XAuto ].
       Qed.
 
-      Theorem pr3_tail_2 : (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
-                           (pr3 c (TTail k u t1) (TTail k u t2)).
+      Theorem pr3_tail_2: (c:?; u,t1,t2:?; k:?) (pr3 (CTail c k u) t1 t2) ->
+                          (pr3 c (TTail k u t1) (TTail k u t2)).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
-      EApply pr3_u; [ Apply pr2_tail_2; Apply H | XAuto ].
+(* case 2: pr3_sing *)
+      EApply pr3_sing; [ Apply pr2_tail_2; Apply H | XAuto ].
       Qed.
 
       Hints Resolve pr3_tail_1 pr3_tail_2 : ltlc.
 
-      Theorem pr3_tail_21 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
-                            (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
-                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+      Theorem pr3_tail_21: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                           (k:?; t1,t2:?) (pr3 (CTail c k u1) t1 t2) ->
+                           (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
       Intros.
       EApply pr3_t; [ Apply pr3_tail_2 | Apply pr3_tail_1 ]; XAuto.
       Qed.
 
-      Theorem pr3_tail_12 : (c:?; u1,u2:?) (pr3 c u1 u2) ->
-                            (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
-                            (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
+      Theorem pr3_tail_12: (c:?; u1,u2:?) (pr3 c u1 u2) ->
+                           (k:?; t1,t2:?) (pr3 (CTail c k u2) t1 t2) ->
+                           (pr3 c (TTail k u1 t1) (TTail k u2 t2)).
       Intros.
       EApply pr3_t; [ Apply pr3_tail_1 | Apply pr3_tail_2 ]; XAuto.
       Qed.
 
-      Theorem pr3_shift : (h:?; c,e:?) (drop h (0) c e) ->
-                          (t1,t2:?) (pr3 c t1 t2) ->
-                          (pr3 e (app c h t1) (app c h t2)).
+      Theorem pr3_shift: (h:?; c,e:?) (drop h (0) c e) ->
+                         (t1,t2:?) (pr3 c t1 t2) ->
+                         (pr3 e (app c h t1) (app c h t2)).
       Intros until 2; XElim H0; Clear t1 t2; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
       XEAuto.
       Qed.
 
@@ -72,4 +191,4 @@ Require Export pr2_defs.
    End pr3_props.
 
       Hints Resolve pr3_pr2 pr3_t pr3_pr1
-                    pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.
+                    pr3_thin_dx pr3_tail_12 pr3_tail_21 pr3_shift : ltlc.