3 Require Export contexts_defs.
4 Require Export subst0_defs.
5 Require Export drop_defs.
7 Inductive csubst0 : nat -> T -> C -> C -> Prop :=
8 | csubst0_fst : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) -> (c:?)
9 (csubst0 (S i) v (CTail c k u) (CTail c k w))
10 | csubst0_snd : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
11 (u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
12 | csubst0_both : (k:?; i:?; u,v,w:?) (subst0 (r k i) v u w) ->
13 (c1,c2:?) (csubst0 (r k i) v c1 c2) ->
14 (csubst0 (S i) v (CTail c1 k u) (CTail c2 k w)).
16 Hint csubst0 : ltlc := Constructors csubst0.
18 Inductive fsubst0 [i:nat; v:T; c1:C; t1:T] : C -> T -> Prop :=
19 | fsubst0_t : (t2:?) (subst0 i v t1 t2) -> (fsubst0 i v c1 t1 c1 t2)
20 | fsubst0_c : (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t1)
21 | fsubst0_b : (t2:?) (subst0 i v t1 t2) ->
22 (c2:?) (csubst0 i v c1 c2) -> (fsubst0 i v c1 t1 c2 t2).
24 Hint fsubst0 : ltlc := Constructors fsubst0.
26 Section csubst0_gen_base. (***********************************************)
28 Theorem csubst0_gen_tail: (k:?; c1,x:?; u1,v:?; i:?)
29 (csubst0 (S i) v (CTail c1 k u1) x) -> (OR
30 (EX u2 | x = (CTail c1 k u2) &
31 (subst0 (r k i) v u1 u2)
33 (EX c2 | x = (CTail c2 k u1) &
34 (csubst0 (r k i) v c1 c2)
36 (EX u2 c2 | x = (CTail c2 k u2) &
37 (subst0 (r k i) v u1 u2) &
38 (csubst0 (r k i) v c1 c2)
40 Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
41 XCase H; Clear x v y y0; Intros; Inversion H1.
42 (* case 1: csubst0_fst *)
43 Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
44 (* case 2: csubst0_snd *)
45 Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
46 (* case 2: csubst0_both *)
47 Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
48 Rewrite H4 in H0; Rewrite H5 in H0; Rewrite H7 in H0; XEAuto.
53 Tactic Definition CSubst0GenBase :=
55 | [ H: (csubst0 (S ?1) ?2 (CTail ?3 ?4 ?5) ?6) |- ? ] ->
56 LApply (csubst0_gen_tail ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
57 XElim H; Intros H; XElim H; Intros.
59 Section csubst0_drop. (***************************************************)
61 Theorem csubst0_drop_ge : (i,n:?) (le i n) ->
62 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
63 (e:?) (drop n (0) c1 e) ->
73 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
75 (* case 2.2.1: csubst0_fst *)
77 (* case 2.2.2: csubst0_snd *)
78 XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
79 (* case 2.2.3: csubst0_both *)
80 XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
81 DropGenBase; NewInduction k; XEAuto.
84 Tactic Definition IH :=
86 | [ H0: (n:?) (lt n ?1) -> (c1,c2:?; v:?) (csubst0 ?1 v c1 c2) -> (e:C) (drop n (0) c1 e) -> ?;
87 H1: (csubst0 ?1 ?2 ?3 ?4); H2: (drop ?5 (0) ?3 ?6) |- ? ] ->
88 LApply (H0 ?5); [ Clear H0; Intros H0 | XAuto ];
89 LApply (H0 ?3 ?4 ?2); [ Clear H0 H1; Intros H0 | XAuto ];
90 LApply (H0 ?6); [ Clear H0 H2; Intros H0 | XAuto ];
91 XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros
92 | [ H0: (r ? ?1) = (S ?1) -> (e:?) (drop (S ?2) (0) ?3 e) -> ?;
93 H1: (drop (S ?2) (0) ?3 ?4) |- ? ] ->
94 LApply H0; [ Clear H0; Intros H0 | XAuto ];
95 LApply (H0 ?4); [ Clear H0 H1; Intros H0 | XAuto ];
96 XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros.
98 Theorem csubst0_drop_lt : (i,n:?) (lt n i) ->
99 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
100 (e:?) (drop n (0) c1 e) -> (OR
102 (EX k e0 u w | e = (CTail e0 k u) &
103 (drop n (0) c2 (CTail e0 k w)) &
104 (subst0 (minus (r k i) (S n)) v u w)
106 (EX k e1 e2 u | e = (CTail e1 k u) &
107 (drop n (0) c2 (CTail e2 k u)) &
108 (csubst0 (minus (r k i) (S n)) v e1 e2)
110 (EX k e1 e2 u w | e = (CTail e1 k u) &
111 (drop n (0) c2 (CTail e2 k w)) &
112 (subst0 (minus (r k i) (S n)) v u w) &
113 (csubst0 (minus (r k i) (S n)) v e1 e2)
120 (* case 2.1: n = 0 *)
121 Intros H0; Clear H0; Intros until 1; InsertEq H0 '(S i); XElim H0;
122 Clear H c1 c2 v y; Intros; DropGenBase; XRewrite e;
123 Rewrite <- r_arith0 in H; Try Rewrite <- r_arith0 in H0; Replace i with i0; XEAuto.
124 (* case 2.2: n > 0 *)
125 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
127 (* case 2.2.1: csubst0_fst *)
129 (* case 2.2.2: csubst0_snd *)
130 Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
131 Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
132 (* case 2.2.2.1: bind *)
133 IH; XRewrite e; Try Rewrite <- (H3 n) in H; Try Rewrite <- (H3 n) in H0;
134 Try Rewrite <- r_arith1 in H4; Try Rewrite <- r_arith1 in H5; XEAuto.
135 (* case 2.2.2.2: flat *)
136 IH; XRewrite e; Try Rewrite <- (H3 n) in H2; Try Rewrite <- (H3 n) in H4; XEAuto.
137 (* case 2.2.3: csubst0_both *)
138 Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; XReplaceIn H3 i0 i; Clear H4 i0.
139 Apply (r_dis k); Intros; Rewrite (H4 i) in H2; Rewrite (H4 n) in H5.
140 (* case 2.2.2.1: bind *)
141 IH; XRewrite e; Try Rewrite <- (H4 n) in H; Try Rewrite <- (H4 n) in H2;
142 Try Rewrite <- r_arith1 in H5; Try Rewrite <- r_arith1 in H6; XEAuto.
143 (* case 2.2.3.2: flat *)
144 IH; XRewrite e; Try Rewrite <- (H4 n) in H3; Try Rewrite <- (H4 n) in H5; XEAuto.
147 Theorem csubst0_drop_ge_back : (i,n:?) (le i n) ->
148 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
149 (e:?) (drop n (0) c2 e) ->
153 Intros; Inversion H0.
156 (* case 2.1 : n = 0 *)
157 Intros; Inversion H0.
158 (* case 2.2 : n > 0 *)
159 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
161 (* case 2.2.1 : csubst0_fst *)
163 (* case 2.2.2 : csubst0_snd *)
164 XReplaceIn H0 i0 i; NewInduction k; XEAuto.
165 (* case 2.2.3 : csubst0_both *)
166 XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.
171 Tactic Definition CSubst0Drop :=
174 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
175 LApply (csubst0_drop_lt ?1 ?2); [ Intros H_x | XAuto ];
176 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
177 LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
179 [ Intros | Intros H3; XElim H3; Intros
180 | Intros H3; XElim H3; Intros | Intros H3; XElim H3; Intros ]
182 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
183 LApply (csubst0_drop_ge ?1 ?2); [ Intros H_x | XAuto ];
184 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
185 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
186 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
187 LApply (csubst0_drop_ge ?1 ?1); [ Intros H_x | XAuto ];
188 LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
189 LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
190 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?5 ?6) |- ? ] ->
191 LApply (csubst0_drop_ge_back ?1 ?1); [ Intros H_x | XAuto ];
192 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
193 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
194 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?5 ?6) |- ? ] ->
195 LApply (csubst0_drop_ge_back ?1 ?2); [ Intros H_x | XAuto ];
196 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
197 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ].