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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
index b2b530d59..35b114f40 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_defs.v
@@ -1,160 +1,84 @@
-(*#* #stop file *)
-
 Require Export pr2_defs.
 Require Export pr3_defs.
 Require Export pc1_defs.
 
-      Inductive pc2 [c:C; t1,t2:T] : Prop :=
-         | pc2_r : (pr2 c t1 t2) -> (pc2 c t1 t2)
-         | pc2_x : (pr2 c t2 t1) -> (pc2 c t1 t2).
-
-      Hint pc2 : ltlc := Constructors pc2.
-
-      Inductive pc3 [c:C] : T -> T -> Prop :=
-         | pc3_r : (t:?) (pc3 c t t)
-         | pc3_u : (t2,t1:?) (pc2 c t1 t2) ->
-                   (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+(*#* #caption "the relation $\\PcT{}{}{}$" *)
+(*#* #cap #cap c, t, t1, t2 *)
 
-      Hint pc3 : ltlc := Constructors pc3.
+      Definition pc3 := [c:?; t1,t2:?] (EX t | (pr3 c t1 t) & (pr3 c t2 t)). 
 
-   Section pc2_props. (******************************************************)
-
-      Theorem pc2_s : (c,t2,t1:?) (pc2 c t1 t2) -> (pc2 c t2 t1).
-      Intros.
-      Inversion H; XAuto.
-      Qed.
-
-      Theorem pc2_shift : (h:?; c,e:?) (drop h (0) c e) ->
-                          (t1,t2:?) (pc2 c t1 t2) ->
-                          (pc2 e (app c h t1) (app c h t2)).
-      Intros until 2; XElim H0; Intros.
-(* case 1 : pc2_r *)
-      XAuto.
-(* case 2 : pc2_x *)
-      XEAuto.
-      Qed.
+(*#* #stop file *)
 
-   End pc2_props.
+      Hints Unfold pc3 : ltlc.
 
-      Hints Resolve pc2_s pc2_shift : ltlc.
+      Tactic Definition Pc3Unfold :=
+         Match Context With
+            [ H: (pc3 ?1 ?2 ?3) |- ? ] -> Unfold pc3 in H; XDecompose H.
 
    Section pc3_props. (******************************************************)
 
-      Theorem pc3_pr2_r : (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
+      Theorem pc3_pr2_r: (c,t1,t2:?) (pr2 c t1 t2) -> (pc3 c t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pc3_pr2_x : (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
+      Theorem pc3_pr2_x: (c,t1,t2:?) (pr2 c t2 t1) -> (pc3 c t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pc3_pc2 : (c,t1,t2:?) (pc2 c t1 t2) -> (pc3 c t1 t2).
+      Theorem pc3_pr3_r: (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pc3_t : (t2,c,t1:?) (pc3 c t1 t2) ->
-                      (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
-      Intros t2 c t1 H; XElim H; XEAuto.
-      Qed.
-
-      Hints Resolve pc3_t : ltlc.
-
-      Theorem pc3_s : (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
-      Intros; XElim H; [ XAuto | XEAuto ].
-      Qed.
-
-      Hints Resolve pc3_s : ltlc.
-
-      Theorem pc3_pr3_r : (c:?; t1,t2) (pr3 c t1 t2) -> (pc3 c t1 t2).
-      Intros; XElim H; XEAuto.
-      Qed.
-
-      Theorem pc3_pr3_x : (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
-      Intros; XElim H; XEAuto.
-      Qed.
-
-      Hints Resolve pc3_pr3_r pc3_pr3_x : ltlc.
-
-      Theorem pc3_pr3_t : (c:?; t1,t0:?) (pr3 c t1 t0) ->
-                          (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
-      Intros; Apply (pc3_t t0); XAuto.
+      Theorem pc3_pr3_x: (c:?; t1,t2) (pr3 c t2 t1) -> (pc3 c t1 t2).
+      XEAuto.
       Qed.
 
-      Theorem pc3_thin_dx : (c:? ;t1,t2:?) (pc3 c t1 t2) ->
-                            (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
-                                              (TTail (Flat f) u t2)).
-      Intros; XElim H; [XAuto | Intros ].
-      EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
+      Theorem pc3_pr3_t: (c:?; t1,t0:?) (pr3 c t1 t0) ->
+                         (t2:?) (pr3 c t2 t0) -> (pc3 c t1 t2).
+      XEAuto.
       Qed.
 
-      Theorem pc3_tail_1 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
-                           (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
-      Intros until 1; XElim H; Intros.
-(* case 1 : pc3_r *)
-      XAuto.
-(* case 2 : pc3_u *)
-      EApply pc3_u; [ Inversion H | Apply H1 ]; XAuto.
+      Theorem pc3_pr2_u: (c:?; t2,t1:?) (pr2 c t1 t2) ->
+                         (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
-
-      Theorem pc3_tail_2 : (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
-                           (pc3 c (TTail k u t1) (TTail k u t2)).
-      Intros.
-      XElim H; [ Idtac | Intros; Inversion H ]; XEAuto.
+      
+      Theorem pc3_refl: (c:?; t:?) (pc3 c t t).
+      XEAuto.
       Qed.
 
-      Theorem pc3_tail_12 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
-                            (k:?; t1,t2:?) (pc3 (CTail c k u2) t1 t2) ->
-                            (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
-      Intros.
-      EApply pc3_t; [ Apply pc3_tail_1 | Apply pc3_tail_2 ]; XAuto.
+      Theorem pc3_s: (c,t2,t1:?) (pc3 c t1 t2) -> (pc3 c t2 t1).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
 
-      Theorem pc3_tail_21 : (c:?; u1,u2:?) (pc3 c u1 u2) ->
-                            (k:?; t1,t2:?) (pc3 (CTail c k u1) t1 t2) ->
-                            (pc3 c (TTail k u1 t1) (TTail k u2 t2)).
-      Intros.
-      EApply pc3_t; [ Apply pc3_tail_2 | Apply pc3_tail_1 ]; XAuto.
+      Theorem pc3_thin_dx: (c:? ;t1,t2:?) (pc3 c t1 t2) ->
+                           (u:?; f:?) (pc3 c (TTail (Flat f) u t1)
+                                             (TTail (Flat f) u t2)).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
 
-      Theorem pc3_pr3_u : (c:?; t2,t1:?) (pr2 c t1 t2) ->
-                          (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
-      XEAuto.
+      Theorem pc3_tail_1: (c:?; u1,u2:?) (pc3 c u1 u2) ->
+                          (k:?; t:?) (pc3 c (TTail k u1 t) (TTail k u2 t)).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
 
-      Theorem pc3_pr3_u2 : (c:?; t0,t1:?) (pr2 c t0 t1) ->
-                           (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
-      Intros; Apply (pc3_t t0); XAuto.
+      Theorem pc3_tail_2: (c:?; u,t1,t2:?; k:?) (pc3 (CTail c k u) t1 t2) ->
+                          (pc3 c (TTail k u t1) (TTail k u t2)).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
 
-      Theorem pc3_shift : (h:?; c,e:?) (drop h (0) c e) ->
-                          (t1,t2:?) (pc3 c t1 t2) ->
-                          (pc3 e (app c h t1) (app c h t2)).
-      Intros until 2; XElim H0; Clear t1 t2; Intros.
-(* case 1 : pc3_r *)
-      XAuto.
-(* case 2 : pc3_u *)
-      XEAuto.
+      Theorem pc3_shift: (h:?; c,e:?) (drop h (0) c e) ->
+                         (t1,t2:?) (pc3 c t1 t2) ->
+                         (pc3 e (app c h t1) (app c h t2)).
+      Intros; Pc3Unfold; XEAuto.
       Qed.
 
       Theorem pc3_pc1: (t1,t2:?) (pc1 t1 t2) -> (c:?) (pc3 c t1 t2).
-      Intros; XElim H; Intros.
-(* case 1: pc1_r *)
-      XAuto.
-(* case 2 : pc1_u *)
-      XElim H; XEAuto.
+      Intros; Pc1Unfold; XEAuto.
       Qed.
-
+   
    End pc3_props.
 
-      Hints Resolve pc3_pr2_r pc3_pr2_x pc3_pc2 pc3_pr3_r pc3_pr3_x
-                    pc3_t pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
-                    pc3_tail_12 pc3_tail_21 pc3_pr3_u pc3_shift pc3_pc1 : ltlc.
-
-      Tactic Definition Pc3T :=
-         Match Context With
-            | [ _: (pr3 ?1 ?2 (TTail ?3 ?4 ?5)); _: (pc3 ?1 ?6 ?4) |- ? ] ->
-               LApply (pc3_t (TTail ?3 ?4 ?5) ?1 ?2); [ Intros H_x | XAuto ];
-               LApply (H_x (TTail ?3 ?6 ?5)); [ Clear H_x; Intros | Apply pc3_s; XAuto ]
-            | [ _: (pc3 ?1 ?2 ?3); _: (pr3 ?1 ?3 ?4) |- ? ] ->
-               LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
-               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
+      Hints Resolve pc3_refl pc3_pr2_r pc3_pr2_x pc3_pr3_r pc3_pr3_x
+                    pc3_s pc3_pr3_t pc3_thin_dx pc3_tail_1 pc3_tail_2
+                    pc3_pr2_u pc3_shift pc3_pc1 : ltlc.