some reorganization and some corrections

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

diff --git a/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v b/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v
index 52505544becde9839452725471c2436c6187a58d..4fd7e138a624026fe2ca6bf8a3de157e2e53a281 100644 (file)
--- a/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v
+++ b/helm/coq-contribs/LAMBDA-TYPES/pc3_subst0.v
@@ -1,7 +1,7 @@
 (*#* #stop file *)
 
 Require subst0_subst0.
-Require csubst0_defs.
+Require fsubst0_defs.
 Require pr0_subst0.
 Require pc3_defs.
 
@@ -12,49 +12,49 @@ Require pc3_defs.
                                (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
                                (pc3 c2 t2 t).
       Intros until 1; XElim H.
-(* case 1: pr2_pr0 *)
+(* case 1: pr2_free *)
       Intros until 2; XElim H0; Intros.
-(* case 1.1: fsubst0_t *)
+(* case 1.1: fsubst0_snd *)
       Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
-(* case 1.2: fsubst0_c *)
+(* case 1.2: fsubst0_fst *)
       XAuto.
-(* case 1.3: fsubst0_b *)
+(* case 1.3: fsubst0_both *)
       Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
 (* case 2 : pr2_delta *)
-      Intros until 3; XElim H1; Intros.
-(* case 2.1: fsubst0_t. *)
+      Intros until 4; XElim H2; Intros.
+(* case 2.1: fsubst0_snd. *)
       Apply (pc3_t t1); [ Apply pc3_s; XEAuto | XEAuto ].
-(* case 2.2: fsubst0_c. *)
+(* case 2.2: fsubst0_fst. *)
       Apply (lt_le_e i i0); Intros; CSubst0Drop.
 (* case 2.2.1: i < i0, none *)
       XEAuto.
-(* case 2.2.2: i < i0, csubst0_fst *)
-      Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ].
+(* case 2.2.2: i < i0, csubst0_snd *)
+      CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u c0 x); XEAuto.
-(* case 2.2.3: i < i0, csubst0_snd *)
-      Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3.
+(* case 2.2.3: i < i0, csubst0_fst *)
+      CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
       Apply pc3_pr2_r; XEAuto.
 (* case 2.2.4: i < i0, csubst0_both *)
-      Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+      CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u c0 x); XEAuto.
 (* case 2.2.5: i >= i0 *)
       XEAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
       Apply (lt_le_e i i0); Intros; CSubst0Drop.
 (* case 2.3.1 : i < i0, none *)
       CSubst0Drop; Apply pc3_pr3_u2 with t0 := t1; XEAuto.
-(* case 2.3.2 : i < i0, csubst0_fst *)
-      Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+(* case 2.3.2 : i < i0, csubst0_snd *)
+      CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
-(* case 2.3.3: i < i0, csubst0_snd *)
-      Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
+(* case 2.3.3: i < i0, csubst0_fst *)
+      CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
       CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
 (* case 2.3.4: i < i0, csubst0_both *)
-      Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
+      CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
 (* case 2.3.5: i >= i0 *)
       CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
@@ -65,52 +65,52 @@ Require pc3_defs.
                                     (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
                                     (pc3 c2 t t2).
       Intros until 1; XElim H.
-(* case 1: pr2_pr0 *)
+(* case 1: pr2_free *)
       Intros until 2; XElim H0; Intros.
-(* case 1.1: fsubst0_t. *)
-      Apply (pc3_pr3_u c1 t1); XEAuto.
-(* case 1.2: fsubst0_c. *)
+(* case 1.1: fsubst0_snd. *)
+      Apply (pc3_pr3_u c1 t2); XEAuto.
+(* case 1.2: fsubst0_fst. *)
       XAuto.
-(* case 1.3: fsubst0_c. *)
-      CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto.
+(* case 1.3: fsubst0_both. *)
+      CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
 (* case 2: pr2_delta *)
-      Intros until 3; XElim H1; Intros.
-(* case 2.1: fsubst0_t. *)
-      Apply (pc3_t t1); XEAuto.
-(* case 2.2: fsubst0_c. *)
+      Intros until 4; XElim H2; Intros.
+(* case 2.1: fsubst0_snd. *)
+      Apply (pc3_t t2); Apply pc3_pr3_r; XEAuto.
+(* case 2.2: fsubst0_fst. *)
       Apply (lt_le_e i i0); Intros; CSubst0Drop.
 (* case 2.2.1: i < i0, none *)
       XEAuto.
 (* case 2.2.2: i < i0, csubst0_bind *)
-      Inversion H; Rewrite <- H7 in H4; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Clear H H7 H8 H9 c2 t2 x0 x1 x2.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H6; [ CSubst0Drop | XAuto ].
+      CGenBase; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H8 H9 H10 c2 t3 x0 x1 x2.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u c0 x); XEAuto.
-(* case 2.2.3: i < i0, csubst0_snd *)
-      Inversion H; Rewrite <- H7 in H5; Rewrite <- H8 in H4; Rewrite <- H8 in H5; Rewrite <- H9 in H4; Clear H H7 H8 H9 c2 t2 x0 x1 x3.
+(* case 2.2.3: i < i0, csubst0_fst *)
+      CGenBase; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H8 H9 H10 c2 t3 x0 x1 x3.
       Apply pc3_pr2_r; XEAuto.
 (* case 2.2.4: i < i0, csubst0_both *)
-      Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H4; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
+      CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
       Apply (pc3_pr3_u c0 x); XEAuto.
 (* case 2.2.5: i >= i0 *)
       XEAuto.
-(* case 2.3: fsubst0_b *)
+(* case 2.3: fsubst0_both *)
       Apply (lt_le_e i i0); Intros; CSubst0Drop.
 (* case 2.3.1 : i < i0, none *)
-      CSubst0Drop; Apply pc3_pr3_u with t2 := t1; XEAuto.
-(* case 2.3.2 : i < i0, csubst0_fst *)
-      Inversion H; Rewrite <- H8 in H5; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Clear H H8 H9 H10 c2 t2 x0 x1 x2.
-      Subst0Subst0; Rewrite <- lt_plus_minus_r in H7; [ CSubst0Drop | XAuto ].
-      Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto.
-(* case 2.3.3: i < i0, csubst0_snd *)
-      Inversion H; Rewrite <- H8 in H6; Rewrite <- H9 in H5; Rewrite <- H9 in H6; Rewrite <- H10 in H5; Clear H H8 H9 H10 c2 t2 x0 x1 x3.
-      CSubst0Drop; Apply (pc3_pr3_u c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
-(* case 2.3.4: i < i0, csubst0_both *)
-      Inversion H; Rewrite <- H9 in H7; Rewrite <- H10 in H5; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H H9 H10 H11 c2 t2 x0 x1 x3.
+      CSubst0Drop; Apply pc3_pr3_u with t2:=t2; Try Apply pc3_pr3_r; XEAuto.
+(* case 2.3.2 : i < i0, csubst0_snd *)
+      CGenBase; Rewrite <- H9 in H6; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H7; Clear H9 H10 H11 c2 t3 x0 x1 x2.
       Subst0Subst0; Rewrite <- lt_plus_minus_r in H8; [ CSubst0Drop | XAuto ].
-      Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t1) ]; XEAuto.
+      Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
+(* case 2.3.3: i < i0, csubst0_fst *)
+      CGenBase; Rewrite <- H9 in H7; Rewrite <- H10 in H6; Rewrite <- H10 in H7; Rewrite <- H11 in H6; Clear H9 H10 H11 c2 t3 x0 x1 x3.
+      CSubst0Drop; Apply (pc3_pr3_u c0 t0); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
+(* case 2.3.4: i < i0, csubst0_both *)
+      CGenBase; Rewrite <- H10 in H8; Rewrite <- H11 in H6; Rewrite <- H11 in H7; Rewrite <- H11 in H8; Rewrite <- H12 in H7; Clear H10 H11 H12 c2 t3 x0 x1 x3.
+      Subst0Subst0; Rewrite <- lt_plus_minus_r in H9; [ CSubst0Drop | XAuto ].
+      Apply (pc3_pr3_u c0 x); [ Idtac | Apply (pc3_pr3_u2 c0 t0) ]; XEAuto.
 (* case 2.3.5: i >= i0 *)
-      CSubst0Drop; Apply (pc3_pr3_u c0 t1); XEAuto.
+      CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
       Qed.
 
       Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->