some reorganization and some corrections

[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 49d9bc4ecff08729ce4d5bddade8eab2cff853ab..6f48a27fee4470734972e50424f33fe97a13528e 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_props.v
@@ -2,21 +2,20 @@
 
 Require subst0_subst0.
 Require pr0_subst0.
+Require cpr0_defs.
 Require pr3_defs.
 Require pr3_props.
 Require pr3_confluence.
-Require cpr0_defs.
-Require cpr0_props.
 Require pc3_defs.
 
    Section pc3_confluence. (*************************************************)
 
-      Theorem pc3_confluence : (c:?; t1,t2:?) (pc3 c t1 t2) ->
-                               (EX t0 | (pr3 c t1 t0) & (pr3 c t2 t0)).
+      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 *)
+(* case 1: pc3_r *)
       XEAuto.
-(* case 2 : pc3_u *)
+(* case 2: pc3_u *)
       Clear H0; XElim H1; Intros.
       Inversion_clear H; [ XEAuto | Pr3Confluence; XEAuto ].
       Qed.
@@ -31,58 +30,58 @@ Require pc3_defs.
 
    Section pc3_context. (****************************************************)
 
-      Theorem pc3_pr0_pr2_t : (u1,u2:?) (pr0 u2 u1) ->
-                              (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
-                              (pc3 (CTail c k u1) t1 t2).
+      Theorem pc3_pr0_pr2_t: (u1,u2:?) (pr0 u2 u1) ->
+                             (c:?; t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+                             (pc3 (CTail c k u1) t1 t2).
       Intros.
       Inversion H0; Clear H0; [ XAuto | NewInduction i ].
-(* case 1 : pr2_delta i = 0 *)
-      DropGenBase; Inversion H0; Clear H0 H3 H4 c k.
-      Rewrite H5 in H; Clear H5 u2.
-      Pr0Subst0; XEAuto.
-(* case 2 : pr2_delta i > 0 *)
+(* case 1: pr2_delta i = 0 *)
+      DropGenBase; Inversion H0; Clear H0 H4 H5 H6 c k t.
+      Rewrite H7 in H; Clear H7 u2.
+      Pr0Subst0; Apply pc3_pr3_t with t0:=x; XEAuto.
+(* case 2: pr2_delta i > 0 *)
       NewInduction k; DropGenBase; XEAuto.
       Qed.
 
-      Theorem pc3_pr2_pr2_t : (c:?; u1,u2:?) (pr2 c u2 u1) ->
-                              (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
-                              (pc3 (CTail c k u1) t1 t2).
+      Theorem pc3_pr2_pr2_t: (c:?; u1,u2:?) (pr2 c u2 u1) ->
+                             (t1,t2:?; k:?) (pr2 (CTail c k u2) t1 t2) ->
+                             (pc3 (CTail c k u1) t1 t2).
       Intros until 1; Inversion H; Clear H; Intros.
-(* case 1 : pr2_pr0 *)
+(* case 1: pr2_free *)
       EApply pc3_pr0_pr2_t; [ Apply H0 | XAuto ].
-(* case 2 : pr2_delta *)
+(* case 2: pr2_delta *)
       Inversion H; [ XAuto | NewInduction i0 ].
-(* case 2.1 : i0 = 0 *)
-      DropGenBase; Inversion H2; Clear H2.
-      Rewrite <- H5; Rewrite H6 in H; Rewrite <- H7 in H3; Clear H5 H6 H7 d0 k u0.
-      Subst0Subst0; Arith9'In H4 i.
+(* case 2.1: i0 = 0 *)
+      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 pr2_delta; XEAuto.
-      Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto ]; XEAuto.
-(* case 2.2 : i0 > 0 *)
+      Apply pc3_pr2_x; EApply pr2_delta; [ Idtac | XEAuto | XEAuto ]; XEAuto.
+(* case 2.2: i0 > 0 *)
       Clear IHi0; NewInduction k; DropGenBase; XEAuto.
       Qed.
 
-      Theorem pc3_pr2_pr3_t : (c:?; u2,t1,t2:?; k:?)
-                              (pr3 (CTail c k u2) t1 t2) ->
-                              (u1:?) (pr2 c u2 u1) ->
-                              (pc3 (CTail c k u1) t1 t2).
+      Theorem pc3_pr2_pr3_t: (c:?; u2,t1,t2:?; k:?)
+                             (pr3 (CTail c k u2) t1 t2) ->
+                             (u1:?) (pr2 c u2 u1) ->
+                             (pc3 (CTail c k u1) t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
       EApply pc3_t.
       EApply pc3_pr2_pr2_t; [ Apply H2 | Apply H ].
       XAuto.
       Qed.
 
-      Theorem pc3_pr3_pc3_t : (c:?; u1,u2:?) (pr3 c u2 u1) ->
-                              (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
-                              (pc3 (CTail c k u1) t1 t2).
+      Theorem pc3_pr3_pc3_t: (c:?; u1,u2:?) (pr3 c u2 u1) ->
+                             (t1,t2:?; k:?) (pc3 (CTail c k u2) t1 t2) ->
+                             (pc3 (CTail c k u1) t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : pr3_r *)
+(* case 1: pr3_refl *)
       XAuto.
-(* case 2 : pr3_u *)
+(* case 2: pr3_sing *)
       Apply H1; Pc3Confluence.
       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_pr2_pr3_t; XEAuto.
       Qed.
@@ -110,9 +109,9 @@ Require pc3_defs.
 
    Section pc3_lift. (*******************************************************)
 
-      Theorem pc3_lift : (c,e:?; h,d:?) (drop h d c e) ->
-                         (t1,t2:?) (pc3 e t1 t2) ->
-                         (pc3 c (lift h d t1) (lift h d t2)).
+      Theorem pc3_lift: (c,e:?; h,d:?) (drop h d c e) ->
+                        (t1,t2:?) (pc3 e t1 t2) ->
+                        (pc3 c (lift h d t1) (lift h d t2)).
 
       Intros.
       Pc3Confluence.
@@ -125,35 +124,35 @@ Require pc3_defs.
 
    Section pc3_cpr0. (*******************************************************)
 
-      Remark pc3_cpr0_t_aux : (c1,c2:?) (cpr0 c1 c2) ->
-                              (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
-                              (pc3 (CTail c2 k u) t1 t2).
+      Remark pc3_cpr0_t_aux: (c1,c2:?) (cpr0 c1 c2) ->
+                             (k:?; u,t1,t2:?) (pr3 (CTail c1 k u) t1 t2) ->
+                             (pc3 (CTail c2 k u) t1 t2).
       Intros; XElim H0; Intros.
-(* case 1.1 : pr3_r *)
+(* case 1.1: pr3_refl *)
       XAuto.
-(* case 1.2 : pr3_u *)
+(* case 1.2: pr3_sing *)
       EApply pc3_t; [ Idtac | XEAuto ]. Clear H2 t1 t2.
       Inversion_clear H0.
-(* case 1.2.1 : pr2_pr0 *)
+(* case 1.2.1: pr2_free *)
       XAuto.
-(* case 1.2.2 : pr2_delta *)
+(* case 1.2.2: pr2_delta *)
       Cpr0Drop; Pr0Subst0.
       EApply pc3_pr3_u; [ EApply pr2_delta; XEAuto | XAuto ].
       Qed.
 
-      Theorem pc3_cpr0_t : (c1,c2:?) (cpr0 c1 c2) ->
-                           (t1,t2:?) (pr3 c1 t1 t2) ->
-                           (pc3 c2 t1 t2).
+      Theorem pc3_cpr0_t: (c1,c2:?) (cpr0 c1 c2) ->
+                          (t1,t2:?) (pr3 c1 t1 t2) ->
+                          (pc3 c2 t1 t2).
       Intros until 1; XElim H; Intros.
-(* case 1 : cpr0_refl *)
+(* case 1: cpr0_refl *)
       XAuto.
-(* case 2 : cpr0_cont *)
+(* case 2: cpr0_comp *)
       Pc3Context; Pc3Confluence.
       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).
+      Theorem pc3_cpr0: (c1,c2:?) (cpr0 c1 c2) -> (t1,t2:?) (pc3 c1 t1 t2) ->
+                        (pc3 c2 t1 t2).
       Intros; Pc3Confluence.
       EApply pc3_t; [ Idtac | Apply pc3_s ]; EApply pc3_cpr0_t; XEAuto.
       Qed.