4 (*#* #caption "main properties of drop" #clauses *)
6 Section confluence. (*****************************************************)
10 Tactic Definition IH :=
12 [ H1: (drop ?1 ?2 c ?3); H2: (drop ?1 ?2 c ?4) |- ? ] ->
13 LApply (H ?4 ?2 ?1); [ Clear H H2; Intros H | XAuto ];
14 LApply (H ?3); [ Clear H H1; Intros | XAuto ].
18 (*#* #caption "confluence, first case" *)
19 (*#* #cap #alpha c in C, x1 in C1, x2 in C2, d in i *)
21 Theorem drop_mono : (c,x1:?; d,h:?) (drop h d c x1) ->
22 (x2:?) (drop h d c x2) -> x1 = x2.
28 Intros; Repeat DropGenBase; Rewrite H0; XAuto.
32 XElim h; Intros; Repeat DropGenBase; Try Rewrite <- H0; XEAuto.
34 Intros; Repeat DropGenBase; Rewrite H1; Rewrite H2; Rewrite H5 in H3;
40 (*#* #caption "confluence, second case" *)
41 (*#* #cap #alpha c in C1, c0 in E1, e in C2, e0 in E2, u in V1, v in V2, i in k, d in i *)
43 Theorem drop_conf_lt: (b:?; i:?; u:?; c0,c:?)
44 (drop i (0) c (CTail c0 (Bind b) u)) ->
45 (e:?; h,d:?) (drop h (S (plus i d)) c e) ->
46 (EX v e0 | u = (lift h d v) &
47 (drop i (0) e (CTail e0 (Bind b) v)) &
57 Rewrite H in H0; Clear H.
61 (* case 2.1 : CSort *)
63 (* case 2.2 : CTail k *)
64 XElim k; Intros; Repeat DropGenBase; Rewrite H2; Clear H2 H3 e t.
65 (* case 2.2.1 : Bind *)
66 LApply (H u c0 c); [ Clear H H0 H1; Intros H | XAuto ].
67 LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
69 (* case 2.2.2 : Flat *)
70 LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
71 LApply (H x0 h d); [ Clear H H9; Intros H | XAuto ].
77 (*#* #caption "confluence, third case" *)
78 (*#* #cap #alpha c in C, a in C1, e in C2, i in k, d in i *)
80 Theorem drop_conf_ge: (i:?; a,c:?) (drop i (0) c a) ->
81 (e:?; h,d:?) (drop h d c e) -> (le (plus d h) i) ->
82 (drop (minus i h) (0) e a).
89 DropGenBase; Rewrite H in H0; Clear H c.
90 Inversion H1; Rewrite H2; Simpl; Clear H1.
91 PlusO; Rewrite H in H0; Rewrite H1 in H0; Clear H H1 d h.
92 DropGenBase; Rewrite <- H; XAuto.
95 (* case 2.1 : CSort *)
96 Intros; Repeat DropGenBase; Rewrite H1; Rewrite H0; XAuto.
97 (* case 2.2 : CTail k *)
98 XElim k; Intros; DropGenBase;
100 [ NewInduction h; DropGenBase;
101 [ Rewrite <- H2; Simpl; XAuto | Clear IHh ]
102 | DropGenBase; Rewrite H2; Clear IHd H2 H4 e t ] ).
103 (* case 2.2.1 : Bind, d = 0, h > 0 *)
104 LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
105 LApply (H e h (0)); XAuto.
106 (* case 2.2.2 : Bind, d > 0 *)
107 LApply (H a c); [ Clear H H0 H1; Intros H | XAuto ].
108 LApply (H x0 h d); [ Clear H H4; Intros H | XAuto ].
109 LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
110 Rewrite <- minus_Sn_m; XEAuto.
111 (* case 2.2.3 : Flat, d = 0, h > 0 *)
112 LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
113 LApply (H e (S h) (0)); XAuto.
114 (* case 2.2.4 : Flat, d > 0 *)
115 LApply H0; [ Clear H H0 H1; Intros H | XAuto ].
116 LApply (H x0 h (S d)); [ Clear H H4; Intros H | XAuto ].
117 LApply H; [ Clear H; Simpl in H3; Intros H | XAuto ].
118 Rewrite <- minus_Sn_m in H; [ Idtac | XEAuto ].
119 Rewrite <- minus_Sn_m; XEAuto.
126 Section transitivity. (***************************************************)
128 (*#* #caption "transitivity, first case" *)
129 (*#* #cap #alpha c1 in C1, c2 in C2, e1 in D1, e2 in D2, d in i, i in k *)
131 Theorem drop_trans_le : (i,d:?) (le i d) ->
132 (c1,c2:?; h:?) (drop h d c1 c2) ->
133 (e2:?) (drop i (0) c2 e2) ->
134 (EX e1 | (drop i (0) c1 e1) & (drop h (minus d i) e1 e2)).
141 DropGenBase; Rewrite H1 in H0.
142 Rewrite <- minus_n_O; XEAuto.
144 Intros i IHi; XElim d.
145 (* case 2.1 : d = 0 *)
147 (* case 2.2 : d > 0 *)
148 Intros d IHd; XElim c1.
149 (* case 2.2.1 : CSort *)
151 DropGenBase; Rewrite H0 in H1.
152 DropGenBase; Rewrite H1; XEAuto.
153 (* case 2.2.2 : CTail k *)
154 Intros c1 IHc; XElim k; Intros;
155 DropGenBase; Rewrite H0 in H1; Rewrite H2; Clear IHd H0 H2 c2 t;
157 (* case 2.2.2.1 : Bind *)
158 LApply (IHi d); [ Clear IHi; Intros IHi | XAuto ].
159 LApply (IHi c1 x0 h); [ Clear IHi H8; Intros IHi | XAuto ].
160 LApply (IHi e2); [ Clear IHi H0; Intros IHi | XAuto ].
162 (* case 2.2.2.2 : Flat *)
163 LApply (IHc x0 h); [ Clear IHc H8; Intros IHc | XAuto ].
164 LApply (IHc e2); [ Clear IHc H0; Intros IHc | XAuto ].
170 (*#* #caption "transitivity, second case" *)
171 (*#* #cap #alpha c1 in C1, c2 in C, e2 in C2, d in i, i in k *)
173 Theorem drop_trans_ge : (i:?; c1,c2:?; d,h:?) (drop h d c1 c2) ->
174 (e2:?) (drop i (0) c2 e2) -> (le d i) ->
175 (drop (plus i h) (0) c1 e2).
182 DropGenBase; Rewrite <- H0.
183 Inversion H1; Rewrite H2 in H; XAuto.
185 Intros i IHi; XElim c1; Simpl.
186 (* case 2.1: CSort *)
188 DropGenBase; Rewrite H in H0.
189 DropGenBase; Rewrite H0; XAuto.
190 (* case 2.2: CTail *)
191 Intros c1 IHc; XElim d.
192 (* case 2.2.1: d = 0 *)
194 (* case 2.2.1.1: h = 0 *)
195 DropGenBase; Rewrite <- H in H0;
196 DropGenBase; Rewrite <- plus_n_O; XAuto.
197 (* case 2.2.1.2: h > 0 *)
198 DropGenBase; Rewrite <- plus_n_Sm.
199 Apply drop_drop; RRw; XEAuto. (**) (* explicit constructor *)
200 (* case 2.2.2: d > 0 *)
201 Intros d IHd; Intros.
202 DropGenBase; Rewrite H in IHd; Rewrite H in H0; Rewrite H2 in IHd; Rewrite H2; Clear IHd H H2 c2 t;
203 DropGenBase; Apply drop_drop; NewInduction k; Simpl; XEAuto. (**) (* explicit constructor *)
212 Tactic Definition DropDis :=
214 [ H1: (drop ?1 ?2 ?3 ?4); H2: (drop ?1 ?2 ?3 ?5) |- ? ] ->
215 LApply (drop_mono ?3 ?5 ?2 ?1); [ Intros H_x | XAuto ];
216 LApply (H_x ?4); [ Clear H_x H1; Intros H1; Rewrite H1 in H2 | XAuto ]
217 | [ H1: (drop ?0 (0) ?1 (CTail ?2 (Bind ?3) ?4));
218 H2: (drop ?5 (S (plus ?0 ?6)) ?1 ?7) |- ? ] ->
219 LApply (drop_conf_lt ?3 ?0 ?4 ?2 ?1); [ Clear H1; Intros H1 | XAuto ];
220 LApply (H1 ?7 ?5 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
222 | [ _: (drop ?0 (0) ?1 ?2); _: (drop ?5 (0) ?1 ?7);
223 _: (lt ?5 ?0) |- ? ] ->
224 LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
225 LApply (H_x ?7 ?5 (0)); [ Clear H_x; Intros H_x | XAuto ];
226 Simpl in H_x; LApply H_x; [ Clear H_x; Intros | XAuto ]
227 | [ _: (drop ?1 (0) ?2 (CTail ?3 (Bind ?) ?));
228 _: (drop (1) ?1 ?2 ?4) |- ? ] ->
229 LApply (drop_conf_ge (S ?1) ?3 ?2); [ Intros H_x | XEAuto ];
230 LApply (H_x ?4 (1) ?1); [ Clear H_x; Intros H_x | XAuto ];
231 LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]; (
233 [ H: (drop (minus (S ?1) (1)) (0) ?4 ?3) |- ? ] ->
234 Simpl in H; Rewrite <- minus_n_O in H )
235 | [ H0: (drop ?0 (0) ?1 ?2); H2: (lt ?6 ?0);
236 H1: (drop (1) ?6 ?1 ?7) |- ? ] ->
237 LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
238 LApply (H_x ?7 (1) ?6); [ Clear H_x; Intros H_x | XAuto ];
239 LApply H_x; [ Clear H_x; Intros | Rewrite plus_sym; XAuto ]
240 | [ H0: (drop ?0 (0) ?1 ?2);
241 H1: (drop ?5 ?6 ?1 ?7) |- ? ] ->
242 LApply (drop_conf_ge ?0 ?2 ?1); [ Intros H_x | XAuto ];
243 LApply (H_x ?7 ?5 ?6); [ Clear H_x; Intros H_x | XAuto ];
244 LApply H_x; [ Clear H_x; Intros | XAuto ]
246 H1: (drop ?3 ?2 ?4 ?5); H2: (drop ?1 (0) ?5 ?6) |- ? ] ->
247 LApply (drop_trans_le ?1 ?2); [ Intros H_x | XAuto ];
248 LApply (H_x ?4 ?5 ?3); [ Clear H_x H1; Intros H_x | XAuto ];
249 LApply (H_x ?6); [ Clear H_x H2; Intros H_x | XAuto ];
252 H1: (drop ?3 ?1 ?4 ?5); H2: (drop ?2 (0) ?5 ?6) |- ? ] ->
253 LApply (drop_trans_ge ?2 ?4 ?5 ?1 ?3); [ Clear H1; Intros H1 | XAuto ];
254 LApply (H1 ?6); [ Clear H1 H2; Intros H1 | XAuto ];
255 LApply H1; [ Clear H1; Intros | XAuto ].