Require fsubst0_defs.
Require pr0_subst0.
Require pc3_defs.
+Require pc3_props.
Section pc3_fsubst0. (****************************************************)
(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd *)
- Pr0Subst0; [ XAuto | Apply (pc3_pr3_u c1 x); XEAuto ].
+ Pr0Subst0; [ XAuto | Apply (pc3_pr2_u c1 x); XEAuto ].
(* case 1.2: fsubst0_fst *)
XAuto.
(* case 1.3: fsubst0_both *)
- Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr3_u c0 x); XEAuto ].
+ Pr0Subst0; CSubst0Drop; [ XAuto | Apply (pc3_pr2_u c0 x); XEAuto ].
(* case 2 : pr2_delta *)
Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
(* 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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* 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 *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
(* 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.
+ CSubst0Drop; Apply pc3_pr2_u2 with t0 := t1; 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_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
+ Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; 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_u2 c0 t1); [ Idtac | Apply pc3_pr2_r ]; XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u2 c0 t1); [ 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_u2 c0 t1); [ Idtac | Apply (pc3_pr3_u c0 x) ]; XEAuto.
+ Apply (pc3_pr2_u2 c0 t1); [ Idtac | Apply (pc3_pr2_u c0 x) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
- CSubst0Drop; Apply (pc3_pr3_u2 c0 t1); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u2 c0 t1); XEAuto.
Qed.
Theorem pc3_pr2_fsubst0_back: (c1:?; t,t1:?) (pr2 c1 t t1) ->
(* case 1: pr2_free *)
Intros until 2; XElim H0; Intros.
(* case 1.1: fsubst0_snd. *)
- Apply (pc3_pr3_u c1 t2); XEAuto.
+ Apply (pc3_pr2_u c1 t2); XEAuto.
(* case 1.2: fsubst0_fst. *)
XAuto.
(* case 1.3: fsubst0_both. *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t2); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u c0 t2); XEAuto.
(* case 2: pr2_delta *)
Intros until 4; XElim H2; Intros.
(* case 2.1: fsubst0_snd. *)
(* case 2.2.2: i < i0, csubst0_bind *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* 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 *)
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.
+ Apply (pc3_pr2_u c0 x); XEAuto.
(* case 2.2.5: i >= i0 *)
XEAuto.
(* 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:=t2; Try Apply pc3_pr3_r; XEAuto.
+ CSubst0Drop; Apply pc3_pr2_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 t0) ]; XEAuto.
+ Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_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.
+ CSubst0Drop; Apply (pc3_pr2_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.
+ Apply (pc3_pr2_u c0 x); [ Idtac | Apply (pc3_pr2_u2 c0 t0) ]; XEAuto.
(* case 2.3.5: i >= i0 *)
- CSubst0Drop; Apply (pc3_pr3_u c0 t0); XEAuto.
+ CSubst0Drop; Apply (pc3_pr2_u c0 t0); XEAuto.
Qed.
- Theorem pc3_pc2_fsubst0: (c1:?; t1,t:?) (pc2 c1 t1 t) ->
- (i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
- (e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
- (pc3 c2 t2 t).
- Intros until 1; XElim H; Intros.
-(* case 1: pc2_r *)
- EApply pc3_pr2_fsubst0; XEAuto.
-(* case 2: pc2_x *)
- Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto.
- Qed.
+ Opaque pc3.
Theorem pc3_fsubst0: (c1:?; t1,t:?) (pc3 c1 t1 t) ->
(i:?; u,c2,t2:?) (fsubst0 i u c1 t1 c2 t2) ->
(e:?) (drop i (0) c1 (CTail e (Bind Abbr) u)) ->
(pc3 c2 t2 t).
- Intros until 1; XElim H.
-(* case 1: pc3_r *)
+ Intros until 1; XElimUsing pc3_ind_left H.
+(* case 1: pc3_refl *)
Intros until 1; XElim H; Intros; Try CSubst0Drop; XEAuto.
-(* case 2: pc3_u *)
+(* case 2: pc3_pr2_u *)
+ Intros until 4; XElim H2; Intros;
+ (Apply (pc3_t t2); [ EApply pc3_pr2_fsubst0; XEAuto | XEAuto ]).
+(* case 2: pc3_pr2_u2 *)
Intros until 4; XElim H2; Intros;
- (Apply (pc3_t t2); [ EApply pc3_pc2_fsubst0; XEAuto | XEAuto ]).
+ (Apply (pc3_t t0); [ Apply pc3_s; EApply pc3_pr2_fsubst0_back; XEAuto | XEAuto ]).
Qed.
End pc3_fsubst0.
- Hints Resolve pc3_fsubst0.
+ Hints Resolve pc3_fsubst0 : ltlc.