1 Require Export contexts_defs.
2 Require Export subst0_defs.
3 Require Export drop_defs.
5 (*#* #caption "axioms for strict substitution in contexts",
6 "substituted tail item: second operand",
7 "substituted tail item: first operand",
8 "substituted tail item: both operands"
10 (*#* #cap #cap c, c1, c2 #alpha v in W, u in V, u1 in V1, u2 in V2, k in z, r in q *)
12 Inductive csubst0 : nat -> T -> C -> C -> Prop :=
13 | csubst0_snd : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) -> (c:?)
14 (csubst0 (S i) v (CTail c k u1) (CTail c k u2))
15 | csubst0_fst : (k:?; i:?; c1,c2:?; v:?) (csubst0 (r k i) v c1 c2) ->
16 (u:?) (csubst0 (S i) v (CTail c1 k u) (CTail c2 k u))
17 | csubst0_both : (k:?; i:?; v,u1,u2:?) (subst0 (r k i) v u1 u2) ->
18 (c1,c2:?) (csubst0 (r k i) v c1 c2) ->
19 (csubst0 (S i) v (CTail c1 k u1) (CTail c2 k u2)).
23 Hint csubst0 : ltlc := Constructors csubst0.
25 Section csubst0_gen_base. (***********************************************)
27 Theorem csubst0_gen_tail: (k:?; c1,x:?; u1,v:?; i:?)
28 (csubst0 (S i) v (CTail c1 k u1) x) -> (OR
29 (EX u2 | x = (CTail c1 k u2) &
30 (subst0 (r k i) v u1 u2)
32 (EX c2 | x = (CTail c2 k u1) &
33 (csubst0 (r k i) v c1 c2)
35 (EX u2 c2 | x = (CTail c2 k u2) &
36 (subst0 (r k i) v u1 u2) &
37 (csubst0 (r k i) v c1 c2)
39 Intros until 1; InsertEq H '(S i); InsertEq H '(CTail c1 k u1).
40 XCase H; Clear x v y y0; Intros; Inversion H1.
41 (* case 1: csubst0_snd *)
42 Inversion H0; Rewrite H3 in H; Rewrite H5 in H; Rewrite H6 in H; XEAuto.
43 (* case 2: csubst0_fst *)
44 Inversion H0; Rewrite H3 in H; Rewrite H4 in H; Rewrite H5 in H; XEAuto.
45 (* case 2: csubst0_both *)
46 Inversion H2; Rewrite H5 in H; Rewrite H6 in H; Rewrite H7 in H;
47 Rewrite H4 in H0; Rewrite H5 in H0; Rewrite H7 in H0; XEAuto.
52 Tactic Definition CSubst0GenBase :=
54 | [ H: (csubst0 (S ?1) ?2 (CTail ?3 ?4 ?5) ?6) |- ? ] ->
55 LApply (csubst0_gen_tail ?4 ?3 ?6 ?5 ?2 ?1); [ Clear H; Intros H | XAuto ];
56 XElim H; Intros H; XElim H; Intros.
58 Section csubst0_drop. (***************************************************)
60 Theorem csubst0_drop_ge : (i,n:?) (le i n) ->
61 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
62 (e:?) (drop n (0) c1 e) ->
72 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros.
74 (* case 2.2.1: csubst0_snd *)
76 (* case 2.2.2: csubst0_fst *)
77 XReplaceIn H0 i0 i; DropGenBase; NewInduction k; XEAuto.
78 (* case 2.2.3: csubst0_both *)
79 XReplaceIn H0 i0 i; XReplaceIn H2 i0 i.
80 DropGenBase; NewInduction k; XEAuto.
83 Tactic Definition IH :=
85 | [ H0: (n:?) (lt n ?1) -> (c1,c2:?; v:?) (csubst0 ?1 v c1 c2) -> (e:C) (drop n (0) c1 e) -> ?;
86 H1: (csubst0 ?1 ?2 ?3 ?4); H2: (drop ?5 (0) ?3 ?6) |- ? ] ->
87 LApply (H0 ?5); [ Clear H0; Intros H0 | XAuto ];
88 LApply (H0 ?3 ?4 ?2); [ Clear H0 H1; Intros H0 | XAuto ];
89 LApply (H0 ?6); [ Clear H0 H2; Intros H0 | XAuto ];
90 XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros
91 | [ H0: (r ? ?1) = (S ?1) -> (e:?) (drop (S ?2) (0) ?3 e) -> ?;
92 H1: (drop (S ?2) (0) ?3 ?4) |- ? ] ->
93 LApply H0; [ Clear H0; Intros H0 | XAuto ];
94 LApply (H0 ?4); [ Clear H0 H1; Intros H0 | XAuto ];
95 XElim H0; Intros H0; [ Idtac | XElim H0 | XElim H0 | XElim H0 ]; Intros.
97 Theorem csubst0_drop_lt : (i,n:?) (lt n i) ->
98 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
99 (e:?) (drop n (0) c1 e) -> (OR
101 (EX k e0 u w | e = (CTail e0 k u) &
102 (drop n (0) c2 (CTail e0 k w)) &
103 (subst0 (minus (r k i) (S n)) v u w)
105 (EX k e1 e2 u | e = (CTail e1 k u) &
106 (drop n (0) c2 (CTail e2 k u)) &
107 (csubst0 (minus (r k i) (S n)) v e1 e2)
109 (EX k e1 e2 u w | e = (CTail e1 k u) &
110 (drop n (0) c2 (CTail e2 k w)) &
111 (subst0 (minus (r k i) (S n)) v u w) &
112 (csubst0 (minus (r k i) (S n)) v e1 e2)
119 (* case 2.1: n = 0 *)
120 Intros H0; Clear H0; Intros until 1; InsertEq H0 '(S i); XElim H0;
121 Clear H c1 c2 v y; Intros; DropGenBase; XRewrite e;
122 Rewrite <- r_arith0 in H; Try Rewrite <- r_arith0 in H0; Replace i with i0; XEAuto.
123 (* case 2.2: n > 0 *)
124 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Clear c1 c2 v y;
126 (* case 2.2.1: csubst0_snd *)
128 (* case 2.2.2: csubst0_fst *)
129 Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; Clear H3 i0.
130 Apply (r_dis k); Intros; Rewrite (H3 i) in H0; Rewrite (H3 n) in H4.
131 (* case 2.2.2.1: bind *)
132 IH; XRewrite e; Try Rewrite <- (H3 n) in H; Try Rewrite <- (H3 n) in H0;
133 Try Rewrite <- r_arith1 in H4; Try Rewrite <- r_arith1 in H5; XEAuto.
134 (* case 2.2.2.2: flat *)
135 IH; XRewrite e; Try Rewrite <- (H3 n) in H2; Try Rewrite <- (H3 n) in H4; XEAuto.
136 (* case 2.2.3: csubst0_both *)
137 Replace i0 with i; XAuto; XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; XReplaceIn H3 i0 i; Clear H4 i0.
138 Apply (r_dis k); Intros; Rewrite (H4 i) in H2; Rewrite (H4 n) in H5.
139 (* case 2.2.2.1: bind *)
140 IH; XRewrite e; Try Rewrite <- (H4 n) in H; Try Rewrite <- (H4 n) in H2;
141 Try Rewrite <- r_arith1 in H5; Try Rewrite <- r_arith1 in H6; XEAuto.
142 (* case 2.2.3.2: flat *)
143 IH; XRewrite e; Try Rewrite <- (H4 n) in H3; Try Rewrite <- (H4 n) in H5; XEAuto.
146 Theorem csubst0_drop_ge_back : (i,n:?) (le i n) ->
147 (c1,c2:?; v:?) (csubst0 i v c1 c2) ->
148 (e:?) (drop n (0) c2 e) ->
152 Intros; Inversion H0.
155 (* case 2.1 : n = 0 *)
156 Intros; Inversion H0.
157 (* case 2.2 : n > 0 *)
158 Intros until 3; Clear H0; InsertEq H2 '(S i); XElim H0; Intros;
160 (* case 2.2.1 : csubst0_snd *)
162 (* case 2.2.2 : csubst0_fst *)
163 XReplaceIn H0 i0 i; NewInduction k; XEAuto.
164 (* case 2.2.3 : csubst0_both *)
165 XReplaceIn H0 i0 i; XReplaceIn H2 i0 i; NewInduction k; XEAuto.
170 Tactic Definition CSubst0Drop :=
173 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
174 LApply (csubst0_drop_lt ?1 ?2); [ Intros H_x | XAuto ];
175 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
176 LApply (H_x ?6); [ Clear H_x H3; Intros H3 | XAuto ];
178 [ Intros | Intros H3; XElim H3; Intros
179 | Intros H3; XElim H3; Intros | Intros H3; XElim H3; Intros ]
181 H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?4 ?6) |- ? ] ->
182 LApply (csubst0_drop_ge ?1 ?2); [ Intros H_x | XAuto ];
183 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
184 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
185 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?4 ?6) |- ? ] ->
186 LApply (csubst0_drop_ge ?1 ?1); [ Intros H_x | XAuto ];
187 LApply (H_x ?4 ?5 ?3); [ Clear H_x H2; Intros H2 | XAuto ];
188 LApply (H2 ?6); [ Clear H2 H3; Intros | XAuto ]
189 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?1 (0) ?5 ?6) |- ? ] ->
190 LApply (csubst0_drop_ge_back ?1 ?1); [ Intros H_x | XAuto ];
191 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
192 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ]
193 | [H2: (csubst0 ?1 ?3 ?4 ?5); H3: (drop ?2 (0) ?5 ?6) |- ? ] ->
194 LApply (csubst0_drop_ge_back ?1 ?2); [ Intros H_x | XAuto ];
195 LApply (H_x ?4 ?5 ?3); [ Clear H_x; Intros H_x | XAuto ];
196 LApply (H_x ?6); [ Clear H_x H3; Intros | XAuto ].