1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* ********************************************************************** *)
16 (* Progetto FreeScale *)
18 (* Sviluppato da: Ing. Cosimo Oliboni, oliboni@cs.unibo.it *)
19 (* Sviluppo: 2008-2010 *)
21 (* ********************************************************************** *)
23 include "common/list_utility.ma".
24 include "common/list_lemmas.ma".
30 nlemma symmetric_lenlist : ∀T.∀l1,l2:list T.len_list T l1 = len_list T l2 → len_list T l2 = len_list T l1.
33 ##[ ##1: #l2; ncases l2; nnormalize;
34 ##[ ##1: #H; napply refl_eq
35 ##| ##2: #h; #t; #H; ndestruct (*nelim (nat_destruct_0_S ? H)*)
37 ##| ##2: #h; #l2; ncases l2; nnormalize;
38 ##[ ##1: #H; #l; #H1; nrewrite < H1; napply refl_eq
39 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
44 nlemma symmetric_foldrightlist2_aux :
45 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
46 (∀x,y,z.f x y z = f y x z) →
47 (∀acc:T2.∀l1,l2:list T1.
48 ∀H1:(len_list T1 l1 = len_list T1 l2).
49 ∀H2:(len_list T1 l2 = len_list T1 l1).
50 (fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2)).
51 #T1; #T2; #f; #H; #acc; #l1;
53 ##[ ##1: #l2; ncases l2;
54 ##[ ##1: nnormalize; #H1; #H2; napply refl_eq
55 ##| ##2: #h; #l; #H1; #H2;
56 nchange in H1:(%) with (O = (S (len_list ? l)));
57 ndestruct (*nelim (nat_destruct_0_S ? H1)*)
59 ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
60 ##[ ##1: #H2; #H3; nchange in H2:(%) with ((S (len_list ? l3)) = O);
61 ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
62 ##| ##2: #h4; #l4; #H2; #H3;
63 nchange in H2:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
64 nchange in H3:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
65 nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
66 (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
67 nrewrite < (H1 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H3));
68 nrewrite > (H h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
74 nlemma symmetric_foldrightlist2 :
75 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
76 (∀x,y,z.f x y z = f y x z) →
77 (∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
78 fold_right_list2 T1 T2 f acc l1 l2 H = fold_right_list2 T1 T2 f acc l2 l1 (symmetric_lenlist T1 l1 l2 H)).
79 #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
80 nrewrite > (symmetric_foldrightlist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lenlist T1 l1 l2 H1));
84 nlemma symmetric_bfoldrightlist2 :
85 ∀T1:Type.∀f:T1 → T1 → bool.
86 (∀x,y.f x y = f y x) →
88 bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1).
91 ##[ ##1: #l2; ncases l2;
92 ##[ ##1: nnormalize; napply refl_eq
93 ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
95 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
96 ##[ ##1: nnormalize; napply refl_eq
97 ##| ##2: #hh2; #ll2; nnormalize;
99 nrewrite > (H hh1 hh2);
105 nlemma bfoldrightlist2_to_eq :
106 ∀T1:Type.∀f:T1 → T1 → bool.
107 (∀x,y.(f x y = true → x = y)) →
109 (bfold_right_list2 T1 f l1 l2 = true → l1 = l2)).
112 ##[ ##1: #l2; ncases l2;
113 ##[ ##1: #H1; napply refl_eq
114 ##| ##2: #hh2; #ll2; nnormalize; #H1;
115 ndestruct (*napply (bool_destruct … H1)*)
117 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
118 ##[ ##1: nnormalize; #H2;
119 ndestruct (*napply (bool_destruct … H2)*)
120 ##| ##2: #hh2; #ll2; #H2;
121 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
122 nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
123 nrewrite > (H1 ll2 (andb_true_true_r … H2));
129 nlemma eq_to_bfoldrightlist2 :
130 ∀T1:Type.∀f:T1 → T1 → bool.
131 (∀x,y.(x = y → f x y = true)) →
133 (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true)).
136 ##[ ##1: #l2; ncases l2;
137 ##[ ##1: #H1; nnormalize; napply refl_eq
138 ##| ##2: #hh2; #ll2; #H1;
139 (* !!! ndestruct: assert false *)
140 nelim (list_destruct_nil_cons ??? H1)
142 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
144 (* !!! ndestruct: assert false *)
145 nelim (list_destruct_cons_nil ??? H2)
146 ##| ##2: #hh2; #ll2; #H2; nnormalize;
147 nrewrite > (list_destruct_1 … H2);
148 nrewrite > (H hh2 hh2 (refl_eq …));
150 nrewrite > (H1 ll2 (list_destruct_2 … H2));
156 nlemma bfoldrightlist2_to_lenlist :
158 (∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2).
161 ##[ ##1: #l2; ncases l2;
162 ##[ ##1: nnormalize; #H; napply refl_eq
163 ##| ##2: nnormalize; #hh; #tt; #H;
164 ndestruct (*napply (bool_destruct … H)*)
166 ##| ##2: #hh; #tt; #H; #l2; ncases l2;
167 ##[ ##1: nnormalize; #H1;
168 ndestruct (*napply (bool_destruct … H1)*)
169 ##| ##2: #hh1; #tt1; #H1; nnormalize;
170 nrewrite > (H tt1 ?);
171 ##[ ##1: napply refl_eq
172 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
173 napply (andb_true_true_r … H1)
179 nlemma decidable_list :
180 ∀T.(∀x,y:T.decidable (x = y)) →
181 (∀x,y:list T.decidable (x = y)).
183 ##[ ##1: #y; ncases y;
184 ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
185 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
187 (* !!! ndestruct: assert false *)
188 napply (list_destruct_nil_cons T … H1)
190 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
191 ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
193 (* !!! ndestruct: assert false *)
194 napply (list_destruct_cons_nil T … H2)
195 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
196 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
197 nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
198 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
199 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
200 nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
201 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
202 nrewrite > H2; nrewrite > H3; napply refl_eq
209 nlemma nbfoldrightlist2_to_neq :
210 ∀T1:Type.∀f:T1 → T1 → bool.
211 (∀x,y.(f x y = false → x ≠ y)) →
213 (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2)).
216 ##[ ##1: #l2; ncases l2;
217 ##[ ##1: nnormalize; #H1;
218 ndestruct (*napply (bool_destruct … H1)*)
219 ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
220 (* !!! ndestruct: assert false *)
221 napply (list_destruct_nil_cons T … H2)
223 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
224 ##[ ##1: #H2; nnormalize; #H3;
225 (* !!! ndestruct: assert false *)
226 napply (list_destruct_cons_nil T … H3)
227 ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
228 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
229 napply (H1 ll2 ? (list_destruct_2 T … H3));
230 napply (or2_elim ??? (andb_false2 … H2) );
231 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
232 ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
233 ##| ##2: napply (H … H4)
235 ##| ##2: #H4; napply H4
241 nlemma list_destruct :
242 ∀T.(∀x,y:T.decidable (x = y)) →
243 (∀h1,h2:T.∀l1,l2:list T.
244 (h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2).
245 #T; #H; #h1; #h2; #l1; nelim l1;
246 ##[ ##1: #l2; ncases l2;
247 ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
248 nnormalize; #H2; nrewrite > H2 in H1:(%);
249 nnormalize; #H1; napply (H1 (refl_eq …))
250 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
252 (* !!! ndestruct: assert false *)
253 napply (list_destruct_nil_cons T … H2)
255 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
256 ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
258 (* !!! ndestruct: assert false *)
259 napply (list_destruct_cons_nil T … H3)
260 ##| ##2: #hh2; #ll2; #H2;
261 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
262 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
263 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
264 nrewrite > H3 in H2:(%); #H2;
265 nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
266 nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
267 napply (H2 (refl_eq …))
273 nlemma neq_to_nbfoldrightlist2 :
274 ∀T:Type.∀f:T → T → bool.
275 (∀x,y:T.decidable (x = y)) →
276 (∀x,y.(x ≠ y → f x y = false)) →
278 (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false)).
279 #T; #f; #H; #H1; #l1;
281 ##[ ##1: #l2; ncases l2;
282 ##[ ##1: nnormalize; #H2; nelim (H2 (refl_eq …))
283 ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
285 ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
286 ##[ ##1: nnormalize; #H3; napply refl_eq
287 ##| ##2: #hh2; #ll2; #H3;
288 nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
289 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H … H3) …);
290 ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
291 ##| ##2: #H4; nrewrite > (H2 ll2 H4);
292 nrewrite > (symmetric_andbool (f hh1 hh2) false);
293 nnormalize; napply refl_eq
299 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
303 ##[ ##1: #H; napply I
304 ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
308 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
312 ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
313 ##| ##2: #x; #l; #H; napply I
321 nlemma symmetric_lennelist : ∀T.∀l1,l2:ne_list T.len_neList T l1 = len_neList T l2 → len_neList T l2 = len_neList T l1.
324 ##[ ##1: #h; #l2; ncases l2; nnormalize;
325 ##[ ##1: #H; #H1; napply refl_eq
326 ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
328 ##| ##2: #h; #l2; ncases l2; nnormalize;
329 ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
330 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
335 nlemma symmetric_foldrightnelist2_aux :
336 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
337 (∀x,y,z.f x y z = f y x z) →
338 (∀acc:T2.∀l1,l2:ne_list T1.
339 ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
340 fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2).
341 #T1; #T2; #f; #H; #acc; #l1;
343 ##[ ##1: #h; #l2; ncases l2;
344 ##[ ##1: #h1; nnormalize; #H1; #H2; nrewrite > (H h h1 acc); napply refl_eq
345 ##| ##2: #h1; #l; ncases l;
346 ##[ ##1: #h3; #H1; #H2;
347 nchange in H1:(%) with ((S O) = (S (S O)));
348 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
349 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
350 ##| ##2: #h3; #l3; #H1; #H2;
351 nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
352 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
353 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
356 ##| ##2: #h3; #l3; #H1; #l2; ncases l2;
357 ##[ ##1: #h4; ncases l3;
358 ##[ ##1: #h5; #H2; #H3;
359 nchange in H2:(%) with ((S (S O)) = (S O));
360 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
361 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
362 ##| ##2: #h5; #l5; #H2; #H3;
363 nchange in H2:(%) with ((S (S (len_neList ? l5))) = (S O));
364 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
365 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H2))
367 ##| ##2: #h4; #l4; #H2; #H3;
368 nchange in H2:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
369 nchange in H3:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
370 nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
371 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
372 nrewrite < (H1 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H2) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H3));
373 nrewrite > (H h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
379 nlemma symmetric_foldrightnelist2 :
380 ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.
381 (∀x,y,z.f x y z = f y x z) →
382 (∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
383 fold_right_neList2 T1 T2 f acc l1 l2 H = fold_right_neList2 T1 T2 f acc l2 l1 (symmetric_lennelist T1 l1 l2 H)).
384 #T1; #T2; #f; #H; #acc; #l1; #l2; #H1;
385 nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f H acc l1 l2 H1 (symmetric_lennelist T1 l1 l2 H1));
389 nlemma symmetric_bfoldrightnelist2 :
390 ∀T1:Type.∀f:T1 → T1 → bool.
391 (∀x,y.f x y = f y x) →
393 bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1).
396 ##[ ##1: #hh1; #l2; ncases l2;
397 ##[ ##1: #hh2; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
398 ##| ##2: #hh2; #ll2; nnormalize; napply refl_eq
400 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
401 ##[ ##1: #hh2; nnormalize; napply refl_eq
402 ##| ##2: #hh2; #ll2; nnormalize;
404 nrewrite > (H hh1 hh2);
410 nlemma bfoldrightnelist2_to_eq :
411 ∀T1:Type.∀f:T1 → T1 → bool.
412 (∀x,y.(f x y = true → x = y)) →
414 (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2)).
417 ##[ ##1: #hh1; #l2; ncases l2;
418 ##[ ##1: #hh2; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
419 ##| ##2: #hh2; #ll2; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
421 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
422 ##[ ##1: #hh2; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
423 ##| ##2: #hh2; #ll2; #H2;
424 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
425 nrewrite > (H hh1 hh2 (andb_true_true_l … H2));
426 nrewrite > (H1 ll2 (andb_true_true_r … H2));
432 nlemma eq_to_bfoldrightnelist2 :
433 ∀T1:Type.∀f:T1 → T1 → bool.
434 (∀x,y.(x = y → f x y = true)) →
436 (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true)).
439 ##[ ##1: #hh1; #l2; ncases l2;
440 ##[ ##1: #hh2; #H1; nnormalize;
441 nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
443 ##| ##2: #hh2; #ll2; #H1;
444 (* !!! ndestruct: assert false *)
445 nelim (nelist_destruct_nil_cons ???? H1)
447 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
449 (* !!! ndestruct: assert false *)
450 nelim (nelist_destruct_cons_nil ???? H2)
451 ##| ##2: #hh2; #ll2; #H2; nnormalize;
452 nrewrite > (nelist_destruct_cons_cons_1 … H2);
453 nrewrite > (H hh2 hh2 (refl_eq …));
455 nrewrite > (H1 ll2 (nelist_destruct_cons_cons_2 … H2));
461 nlemma bfoldrightnelist2_to_lennelist :
463 (∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2).
466 ##[ ##1: #hh1; #l2; ncases l2;
467 ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
468 ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
470 ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
471 ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
472 ##| ##2: #hh2; #tt2; #H1; nnormalize;
473 nrewrite > (H tt2 ?);
474 ##[ ##1: napply refl_eq
475 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
476 napply (andb_true_true_r … H1)
482 nlemma decidable_nelist :
483 ∀T.(∀x,y:T.decidable (x = y)) →
484 (∀x,y:ne_list T.decidable (x = y)).
486 ##[ ##1: #hh1; #y; ncases y;
487 ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
488 ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
489 ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
490 #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
492 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
494 (* !!! ndestruct: assert false *)
495 napply (nelist_destruct_nil_cons T … H1)
497 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
498 ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
500 (* !!! ndestruct: assert false *)
501 napply (nelist_destruct_cons_nil T … H2)
502 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
503 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
504 nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
505 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
506 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
507 nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
508 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
509 nrewrite > H2; nrewrite > H3; napply refl_eq
516 nlemma nbfoldrightnelist2_to_neq :
517 ∀T1:Type.∀f:T1 → T1 → bool.
518 (∀x,y.(f x y = false → x ≠ y)) →
520 (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2)).
523 ##[ ##1: #hh1; #l2; ncases l2;
524 ##[ ##1: #hh2; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
525 ##| ##2: #hh2; #ll2; #H1; nnormalize; #H2;
526 (* !!! ndestruct: assert false *)
527 napply (nelist_destruct_nil_cons T … H2)
529 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
530 ##[ ##1: #hh2; #H2; nnormalize; #H3;
531 (* !!! ndestruct: assert false *)
532 napply (nelist_destruct_cons_nil T … H3)
533 ##| ##2: #hh2; #ll2; #H2; nnormalize; #H3;
534 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
535 napply (H1 ll2 ? (nelist_destruct_cons_cons_2 T … H3));
536 napply (or2_elim ??? (andb_false2 … H2) );
537 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
538 ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
539 ##| ##2: napply (H … H4)
541 ##| ##2: #H4; napply H4
547 nlemma nelist_destruct :
548 ∀T.(∀x,y:T.decidable (x = y)) →
549 (∀h1,h2:T.∀l1,l2:ne_list T.
550 (h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2).
551 #T; #H; #h1; #h2; #l1; nelim l1;
552 ##[ ##1: #hh1; #l2; ncases l2;
553 ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
554 ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
555 ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
556 napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
557 ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
558 nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
559 ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
562 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
564 (* !!! ndestruct: assert false *)
565 napply (nelist_destruct_nil_cons T … H2)
567 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
568 ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
570 (* !!! ndestruct: assert false *)
571 napply (nelist_destruct_cons_nil T … H3)
572 ##| ##2: #hh2; #ll2; #H2;
573 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
574 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
575 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
576 nrewrite > H3 in H2:(%); #H2;
577 nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
578 nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
579 napply (H2 (refl_eq …))
585 nlemma neq_to_nbfoldrightnelist2 :
586 ∀T:Type.∀f:T → T → bool.
587 (∀x,y:T.decidable (x = y)) →
588 (∀x,y.(x ≠ y → f x y = false)) →
590 (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false)).
591 #T; #f; #H; #H1; #l1;
593 ##[ ##1: #hh1; #l2; ncases l2;
594 ##[ ##1: #hh2; nnormalize; #H2; napply (H1 hh1 hh2 ?);
595 nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
596 ##| ##2: #hh2; #ll2; nnormalize; #H2; napply refl_eq
598 ##| ##2: #hh1; #ll1; #H2; #l2; ncases l2;
599 ##[ ##1: #hh2; nnormalize; #H3; napply refl_eq
600 ##| ##2: #hh2; #ll2; #H3;
601 nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
602 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H … H3) …);
603 ##[ ##1: #H4; nrewrite > (H1 hh1 hh2 H4); nnormalize; napply refl_eq
604 ##| ##2: #H4; nrewrite > (H2 ll2 H4);
605 nrewrite > (symmetric_andbool (f hh1 hh2) false);
606 nnormalize; napply refl_eq