ocaml 3.09 transition

[helm.git] / helm / coq-contribs / LAMBDA-TYPES / pc3_props.v

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v
index 6f48a27fee4470734972e50424f33fe97a13528e..28aa031507847ed705a456f7f2549eb78c52fc78 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v
@@ -8,25 +8,47 @@ Require pr3_props.
 Require pr3_confluence.
 Require pc3_defs.
 
-   Section pc3_confluence. (*************************************************)
+   Section pc3_trans. (******************************************************)
 
-      Theorem pc3_confluence: (c:?; t1,t2:?) (pc3 c t1 t2) ->
-                              (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
-      Intros; XElim H; Intros.
-(* case 1: pc3_r *)
-      XEAuto.
-(* case 2: pc3_u *)
-      Clear H0; XElim H1; Intros.
-      Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
+      Theorem pc3_t: (t2,c,t1:?) (pc3 c t1 t2) ->
+                     (t3:?) (pc3 c t2 t3) -> (pc3 c t1 t3).
+      Intros; Repeat Pc3Unfold; Pr3Confluence; XEAuto.
       Qed.
 
-   End pc3_confluence.
+      Theorem pc3_pr2_u2: (c:?; t0,t1:?) (pr2 c t0 t1) ->
+                          (t2:?) (pc3 c t0 t2) -> (pc3 c t1 t2).
+      Intros; Apply (pc3_t t0); XAuto.
+      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.
+      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.
+      Qed.
+
+   End pc3_trans.
+
+      Hints Resolve pc3_t pc3_tail_12 pc3_tail_21 : ltlc.
 
-      Tactic Definition Pc3Confluence :=
+      Tactic Definition Pc3T :=
          Match Context With
-            [ H: (pc3 ?1 ?2 ?3) |- ? ] ->
-               LApply (pc3_confluence ?1 ?2 ?3); [ Clear H; Intros H | XAuto ];
-               XElim H; Intros.
+            | [ _: (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 ]
+            | [ _: (pc3 ?1 ?2 ?3); _: (pc3 ?1 ?4 ?3) |- ? ] ->
+               LApply (pc3_t ?3 ?1 ?2); [ Intros H_x | XAuto ];
+               LApply (H_x ?4); [ Clear H_x; Intros | XAuto ].
 
    Section pc3_context. (****************************************************)
 
@@ -55,7 +77,7 @@ Require pc3_defs.
       DropGenBase; Inversion H4; Clear H3 H4 H7 t t4.
       Rewrite <- H9; Rewrite H10 in H; Rewrite <- H11 in H6; Clear H9 H10 H11 d0 k u0.
       Pr0Subst0; Subst0Subst0; Arith9'In H6 i.
-      EApply pc3_pr3_u.
+      EApply pc3_pr2_u.
       EApply pr2_delta; XEAuto.
       Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
 (* case 2.2: i0 > 0 *)
@@ -82,7 +104,7 @@ Require pc3_defs.
 (* case 1: pr3_refl *)
       XAuto.
 (* case 2: pr3_sing *)
-      Apply H1; Pc3Confluence.
+      Apply H1; Pc3Unfold.
       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
       Qed.
 
@@ -114,8 +136,8 @@ Require pc3_defs.
                         (pc3 c (lift h d t1) (lift h d t2)).
 
       Intros.
-      Pc3Confluence.
-      EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H0 Orelse Apply H1 ]).
+      Pc3Unfold.
+      EApply pc3_pr3_t; (EApply pr3_lift; [ XEAuto | Apply H1 Orelse Apply H2 ]).
       Qed.
 
    End pc3_lift.
@@ -137,7 +159,7 @@ Require pc3_defs.
       XAuto.
 (* case 1.2.2: pr2_delta *)
       Cpr0Drop; Pr0Subst0.
-      EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
+      EApply pc3_pr2_u; [ EApply pr2_delta; XEAuto | XAuto ].
       Qed.
 
       Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
@@ -147,16 +169,65 @@ Require pc3_defs.
 (* case 1: cpr0_refl *)
       XAuto.
 (* case 2: cpr0_comp *)
-      Pc3Context; Pc3Confluence.
+      Pc3Context; Pc3Unfold.
       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t_aux; XEAuto.
       Qed.
 
       Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
                         (pc3 c2 t1 t2).
-      Intros; Pc3Confluence.
+      Intros; Pc3Unfold.
       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
       Qed.
 
    End pc3_cpr0.
 
       Hints Resolve pc3_cpr0 : ltlc.
+
+   Section pc3_ind_left. (***************************************************)
+   
+      Inductive pc3_left [c:C] : T -> T -> Prop :=
+         | pc3_left_r : (t:?) (pc3_left c t t)
+        | pc3_left_ur: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t2 t3) ->
+                       (pc3_left c t1 t3)
+        | pc3_left_ux: (t1,t2:?) (pr2 c t1 t2) -> (t3:?) (pc3_left c t1 t3) ->
+                       (pc3_left c t2 t3).
+                       
+      Hint pc3_left: ltlc := Constructors pc3_left.
+
+      Remark pc3_left_pr3: (c:?; t1,t2:?) (pr3 c t1 t2) -> (pc3_left c t1 t2).
+      Intros; XElim H; XEAuto.
+      Qed.
+
+      Remark pc3_left_trans: (c:?; t1,t2:?) (pc3_left c t1 t2) -> 
+                             (t3:?) (pc3_left c t2 t3) -> (pc3_left c t1 t3).
+      Intros until 1; XElim H; XEAuto.
+      Qed.
+
+      Hints Resolve pc3_left_trans : ltlc.
+
+      Remark pc3_left_sym: (c:?; t1,t2:?) (pc3_left c t1 t2) -> 
+                           (pc3_left c t2 t1).
+      Intros; XElim H; XEAuto.
+      Qed.
+
+      Hints Resolve pc3_left_sym pc3_left_pr3 : ltlc.
+
+      Remark pc3_left_pc3: (c:?; t1,t2:?) (pc3 c t1 t2) -> (pc3_left c t1 t2).
+      Intros; Pc3Unfold; XEAuto.
+      Qed.
+
+      Remark pc3_pc3_left: (c:?; t1,t2:?) (pc3_left c t1 t2) -> (pc3 c t1 t2).
+      Intros; XElim H; XEAuto.
+      Qed.
+      
+      Hints Resolve pc3_left_pc3 pc3_pc3_left : ltlc.
+
+      Theorem pc3_ind_left: (c:C; P:(T->T->Prop))
+                            ((t:T) (P t t)) ->
+                           ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t2 t3) -> (P t2 t3) -> (P t1 t3)) ->
+                           ((t1,t2:T) (pr2 c t1 t2) -> (t3:T) (pc3 c t1 t3) -> (P t1 t3) -> (P t2 t3)) ->
+                           (t,t0:T) (pc3 c t t0) -> (P t t0).
+      Intros; ElimType (pc3_left c t t0); XEAuto.
+      Qed.
+
+   End pc3_ind_left.