6 Section subst0_gen_lift_lt. (*********************************************)
8 Tactic Definition IH :=
10 [ H1: (x:T; i,h,d:nat) (subst0 i (lift h d ?1) (lift h (S (plus i d)) ?2) x) -> ?;
11 H2: (subst0 ?3 (lift ?4 ?5 ?1) (lift ?4 (S (plus ?3 ?5)) ?2) ?6) |- ? ] ->
12 LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
15 Theorem subst0_gen_lift_lt : (u,t1,x:?; i,h,d:?) (subst0 i (lift h d u) (lift h (S (plus i d)) t1) x) ->
16 (EX t2 | x = (lift h (S (plus i d)) t2) & (subst0 i u t1 t2)).
19 Rewrite lift_sort in H; Subst0GenBase.
21 Apply (lt_le_e n (S (plus i d))); Intros.
22 (* case 2.1: n < 1 + i + d *)
23 Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
24 Subst0GenBase; Rewrite H1; Rewrite H.
25 Rewrite <- lift_d; Simpl; XEAuto.
26 (* case 2.2: n >= 1 + i + d *)
27 Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
28 Subst0GenBase; Rewrite <- H in H0.
29 EApply le_false; [ Idtac | Apply H0 ]; XAuto.
31 Rewrite lift_tail in H1; Subst0GenBase; Rewrite H1; Clear H1 x.
32 (* case 3.1: subst0_fst *)
33 IH; Rewrite H; Rewrite <- lift_tail; XEAuto.
34 (* case 3.2: subst0_snd *)
35 SRwIn H2; IH; Rewrite H0; SRwBack; Rewrite <- lift_tail; XEAuto.
36 (* case 3.2: subst0_snd *)
37 SRwIn H3; Repeat IH; Rewrite H; Rewrite H0; SRwBack;
38 Rewrite <- lift_tail; XEAuto.
41 End subst0_gen_lift_lt.
43 Section subst0_gen_lift_false. (******************************************)
45 Theorem subst0_gen_lift_false : (t,u,x:?; h,d,i:?)
46 (le d i) -> (lt i (plus d h)) ->
47 (subst0 i u (lift h d t) x) ->
51 Rewrite lift_sort in H1; Subst0GenBase.
53 Apply (lt_le_e n d); Intros.
55 Rewrite lift_lref_lt in H1; [ Idtac | XAuto ].
56 Subst0GenBase; Rewrite H1 in H2.
57 EApply le_false; [ Apply H | XAuto ].
58 (* case 2.2: n >= d *)
59 Rewrite lift_lref_ge in H1; [ Idtac | XAuto ].
60 Subst0GenBase; Rewrite <- H1 in H0.
61 EApply le_false; [ Apply H2 | XEAuto ].
63 Rewrite lift_tail in H3; Subst0GenBase.
64 (* case 3.1: subst0_fst *)
66 (* case 3.2: subst0_snd *)
67 EApply H0; [ Idtac | Idtac | XEAuto ]; [ Idtac | SRwBack ]; XAuto.
68 (* case 3.3: subst0_both *)
72 End subst0_gen_lift_false.
74 Section subst0_gen_lift_ge. (*********************************************)
76 Tactic Definition IH :=
78 [ H1: (x:?; i,h,d:?) (subst0 i ?1 (lift h d ?2) x) -> ?;
79 H2: (subst0 ?3 ?1 (lift ?4 ?5 ?2) ?6) |- ? ] ->
80 LApply (H1 ?6 ?3 ?4 ?5); [ Clear H1 H2; Intros H1 | XAuto ];
81 LApply H1; [ Clear H1; Intros H1 | SRwBack; XAuto ];
84 Theorem subst0_gen_lift_ge : (u,t1,x:?; i,h,d:?) (subst0 i u (lift h d t1) x) ->
86 (EX t2 | x = (lift h d t2) & (subst0 (minus i h) u t1 t2)).
89 Rewrite lift_sort in H; Subst0GenBase.
91 Apply (lt_le_e n d); Intros.
93 Rewrite lift_lref_lt in H; [ Idtac | XAuto ].
94 Subst0GenBase; Rewrite H in H1.
95 EApply le_false; [ Apply H0 | XAuto ].
96 (* case 2.2: n >= d *)
97 Rewrite lift_lref_ge in H; [ Idtac | XAuto ].
98 Subst0GenBase; Rewrite <- H; Rewrite H2.
100 EApply ex2_intro; [ Idtac | XAuto ].
101 Rewrite lift_free; [ Idtac | XEAuto (**) | XAuto ].
102 Rewrite plus_sym; Rewrite plus_n_Sm; XAuto.
103 (* case 3: TTail k *)
104 Rewrite lift_tail in H1; Subst0GenBase; Rewrite H1; Clear H1 x;
105 Repeat IH; Try Rewrite H; Try Rewrite H0;
106 Rewrite <- lift_tail; Try Rewrite <- s_minus in H1; XEAuto.
109 End subst0_gen_lift_ge.
111 Tactic Definition Subst0Gen :=
113 | [ H: (subst0 ?0 (lift ?1 ?2 ?3) (lift ?1 (S (plus ?0 ?2)) ?4) ?5) |- ? ] ->
114 LApply (subst0_gen_lift_lt ?3 ?4 ?5 ?0 ?1 ?2); [ Clear H; Intros H | XAuto ];
116 | [ H: (subst0 ?0 ?1 (lift (1) ?0 ?2) ?3) |- ? ] ->
117 LApply (subst0_gen_lift_false ?2 ?1 ?3 (1) ?0 ?0); [ Intros H_x | XAuto ];
118 LApply H_x; [ Clear H_x; Intros H_x | Rewrite plus_sym; XAuto ];
119 LApply H_x; [ Clear H H_x; Intros H | XAuto ];
121 | [ _: (le ?1 ?2); _: (lt ?2 (plus ?1 ?3));
122 _: (subst0 ?2 ?4 (lift ?3 ?1 ?5) ?6) |- ? ] ->
123 Apply (subst0_gen_lift_false ?5 ?4 ?6 ?3 ?1 ?2); XAuto
124 | [ _: (subst0 ?1 ?2 (lift (S ?1) (0) ?3) ?4) |- ? ] ->
125 Apply (subst0_gen_lift_false ?3 ?2 ?4 (S ?1) (0) ?1); XAuto
126 | [ H: (subst0 ?0 ?1 (lift ?2 ?3 ?4) ?5) |- ? ] ->
127 LApply (subst0_gen_lift_ge ?1 ?4 ?5 ?0 ?2 ?3); [ Clear H; Intros H | XAuto ];
128 LApply H; [ Clear H; Intros H | Simpl; XAuto ];
130 | _ -> Subst0GenBase.