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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v b/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
index 0dcc0b8c7..22b4fcefb 100644
--- a/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc1_defs.v
@@ -1,79 +1,50 @@
 (*#* #stop file *)
 
 Require Export pr0_defs.
+Require Export pr1_defs.
 
-      Inductive pc0 [t1,t2:T] : Prop :=
-         | pc0_r : (pr0 t1 t2) -> (pc0 t1 t2)
-         | pc0_x : (pr0 t2 t1) -> (pc0 t1 t2).
+      Definition pc1 := [t1,t2:?] (EX t | (pr1 t1 t) & (pr1 t2 t)). 
 
-      Hint pc0 : ltlc := Constructors pc0.
+      Hints Unfold pc1 : ltlc.
 
-      Inductive pc1 : T -> T -> Prop :=
-         | pc1_r : (t:?) (pc1 t t)
-         | pc1_u : (t2,t1:?) (pc0 t1 t2) -> (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-
-      Hint pc1 : ltlc := Constructors pc1.
-
-   Section pc0_props. (******************************************************)
-
-      Theorem pc0_s : (t2,t1:?) (pc0 t1 t2) -> (pc0 t2 t1).
-      Intros.
-      Inversion H; XAuto.
-      Qed.
-
-   End pc0_props.
-
-      Hints Resolve pc0_s : ltlc.
+      Tactic Definition Pc1Unfold :=
+         Match Context With
+            [ H: (pc1 ?2 ?3) |- ? ] -> Unfold pc1 in H; XDecompose H.
 
    Section pc1_props. (******************************************************)
 
-      Theorem pc1_pr0_r : (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
+      Theorem pc1_pr0_r: (t1,t2:?) (pr0 t1 t2) -> (pc1 t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pc1_pr0_x : (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
+      Theorem pc1_pr0_x: (t1,t2:?) (pr0 t2 t1) -> (pc1 t1 t2).
       XEAuto.
       Qed.
 
-      Theorem pc1_pc0 : (t1,t2:?) (pc0 t1 t2) -> (pc1 t1 t2).
-      XEAuto.
+      Theorem pc1_pr0_u: (t2,t1:?) (pr0 t1 t2) ->
+                         (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
+      Intros; Pc1Unfold; XEAuto.
       Qed.
-
-      Theorem pc1_t : (t2,t1:?) (pc1 t1 t2) ->
-                      (t3:?) (pc1 t2 t3) -> (pc1 t1 t3).
-      Intros t2 t1 H; XElim H; XEAuto.
+      
+      Theorem pc1_refl: (t:?) (pc1 t t).
+      XEAuto.
       Qed.
 
-      Hints Resolve pc1_t : ltlc.
-
-      Theorem pc1_s : (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
-      Intros; XElim H; XEAuto.
+      Theorem pc1_s: (t2,t1:?) (pc1 t1 t2) -> (pc1 t2 t1).
+      Intros; Pc1Unfold; XEAuto.
       Qed.
 
       Theorem pc1_tail_1: (u1,u2:?) (pc1 u1 u2) ->
                           (t:?; k:?) (pc1 (TTail k u1 t) (TTail k u2 t)).
-      Intros; XElim H; Intros.
-(* case 1: pc1_r *)
-      XAuto.
-(* case 2: pc1_u *)
-      XElim H; Intros; XEAuto.
+      Intros; Pc1Unfold; XEAuto.
       Qed.
 
       Theorem pc1_tail_2: (t1,t2:?) (pc1 t1 t2) ->
                           (u:?; k:?) (pc1 (TTail k u t1) (TTail k u t2)).
-      Intros; XElim H; Intros.
-(* case 1: pc1_r *)
-      XAuto.
-(* case 2: pc1_u *)
-      XElim H; Intros; XEAuto.
-      Qed.
-
-      Theorem pc1_tail: (u1,u2:?) (pc1 u1 u2) -> (t1,t2:?) (pc1 t1 t2) ->
-                        (k:?) (pc1 (TTail k u1 t1) (TTail k u2 t2)).
-      Intros; EApply pc1_t; [ EApply pc1_tail_1 | EApply pc1_tail_2 ]; XAuto.
+      Intros; Pc1Unfold; XEAuto.
       Qed.
 
    End pc1_props.
 
-      Hints Resolve pc1_pr0_r pc1_pr0_x pc1_pc0 pc1_t pc1_s
-                    pc1_tail_1 pc1_tail_2 pc1_tail : ltlc.
+      Hints Resolve pc1_refl pc1_pr0_u pc1_pr0_r pc1_pr0_x pc1_s
+                    pc1_tail_1 pc1_tail_2 : ltlc.