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.∀acc:T2.∀l1,l2:list T1.
46 ∀H1:len_list T1 l1 = len_list T1 l2.∀H2:len_list T1 l2 = len_list T1 l1.
47 (∀x,y,z.f x y z = f y x z) →
48 fold_right_list2 T1 T2 f acc l1 l2 H1 = fold_right_list2 T1 T2 f acc l2 l1 H2.
49 #T1; #T2; #f; #acc; #l1;
51 ##[ ##1: #l2; ncases l2;
52 ##[ ##1: nnormalize; #H1; #H2; #H3; napply refl_eq
53 ##| ##2: #h; #l; #H1; #H2; #H3;
54 nchange in H1:(%) with (O = (S (len_list ? l)));
55 ndestruct (*nelim (nat_destruct_0_S ? H1)*)
57 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
58 ##[ ##1: #H1; #H2; #H3; nchange in H1:(%) with ((S (len_list ? l3)) = O);
59 ndestruct (*nelim (nat_destruct_S_0 ? H1)*)
60 ##| ##2: #h4; #l4; #H1; #H2; #H3;
61 nchange in H1:(%) with ((S (len_list ? l3)) = (S (len_list ? l4)));
62 nchange in H2:(%) with ((S (len_list ? l4)) = (S (len_list ? l3)));
63 nchange with ((f h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 ?))) =
64 (f h4 h3 (fold_right_list2 T1 T2 f acc l4 l3 (fold_right_list2_aux3 T1 h4 h3 l4 l3 ?))));
65 nrewrite < (H l4 (fold_right_list2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_list2_aux3 T1 h4 h3 l4 l3 H2) H3);
66 nrewrite > (H3 h3 h4 (fold_right_list2 T1 T2 f acc l3 l4 ?));
72 nlemma symmetric_foldrightlist2
73 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:list T1.∀H:len_list T1 l1 = len_list T1 l2.
74 (∀x,y,z.f x y z = f y x z) →
75 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).
76 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
77 nrewrite > (symmetric_foldrightlist2_aux T1 T2 f acc l1 l2 H (symmetric_lenlist T1 l1 l2 H) H1);
81 nlemma symmetric_bfoldrightlist2
82 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
83 (∀x,y.f x y = f y x) →
84 bfold_right_list2 T1 f l1 l2 = bfold_right_list2 T1 f l2 l1.
87 ##[ ##1: #l2; ncases l2;
88 ##[ ##1: #H; nnormalize; napply refl_eq
89 ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
91 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
92 ##[ ##1: #H1; nnormalize; napply refl_eq
93 ##| ##2: #hh2; #ll2; #H1; nnormalize;
94 nrewrite > (H ll2 H1);
95 nrewrite > (H1 hh1 hh2);
101 nlemma bfoldrightlist2_to_eq
102 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
103 (∀x,y.(f x y = true → x = y)) →
104 (bfold_right_list2 T1 f l1 l2 = true → l1 = l2).
107 ##[ ##1: #l2; ncases l2;
108 ##[ ##1: #H; #H1; napply refl_eq
109 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1;
110 ndestruct (*napply (bool_destruct … H1)*)
112 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
113 ##[ ##1: #H1; nnormalize; #H2;
114 ndestruct (*napply (bool_destruct … H2)*)
115 ##| ##2: #hh2; #ll2; #H1; #H2;
116 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
117 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
118 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
124 nlemma eq_to_bfoldrightlist2
125 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
126 (∀x,y.(x = y → f x y = true)) →
127 (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
130 ##[ ##1: #l2; ncases l2;
131 ##[ ##1: #H; #H1; nnormalize; napply refl_eq
132 ##| ##2: #hh2; #ll2; #H; #H1;
133 (* !!! ndestruct: assert false *)
134 nelim (list_destruct_nil_cons ??? H1)
136 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
138 (* !!! ndestruct: assert false *)
139 nelim (list_destruct_cons_nil ??? H2)
140 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
141 nrewrite > (list_destruct_1 … H2);
142 nrewrite > (H1 hh2 hh2 (refl_eq …));
144 nrewrite > (H ll2 H1 (list_destruct_2 … H2));
150 nlemma bfoldrightlist2_to_lenlist
151 : ∀T.∀f:T → T → bool.∀l1,l2:list T.bfold_right_list2 T f l1 l2 = true → len_list T l1 = len_list T l2.
154 ##[ ##1: #l2; ncases l2;
155 ##[ ##1: nnormalize; #H; napply refl_eq
156 ##| ##2: nnormalize; #hh; #tt; #H;
157 ndestruct (*napply (bool_destruct … H)*)
159 ##| ##2: #hh; #tt; #H; #l2; ncases l2;
160 ##[ ##1: nnormalize; #H1;
161 ndestruct (*napply (bool_destruct … H1)*)
162 ##| ##2: #hh1; #tt1; #H1; nnormalize;
163 nrewrite > (H tt1 ?);
164 ##[ ##1: napply refl_eq
165 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
166 napply (andb_true_true_r … H1)
172 nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y).
174 ##[ ##1: #y; ncases y;
175 ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
176 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
178 (* !!! ndestruct: assert false *)
179 napply (list_destruct_nil_cons T … H1)
181 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
182 ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
184 (* !!! ndestruct: assert false *)
185 napply (list_destruct_cons_nil T … H2)
186 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
187 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
188 nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
189 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
190 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
191 nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
192 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
193 nrewrite > H2; nrewrite > H3; napply refl_eq
200 nlemma nbfoldrightlist2_to_neq
201 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
202 (∀x,y.(f x y = false → x ≠ y)) →
203 (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2).
206 ##[ ##1: #l2; ncases l2;
207 ##[ ##1: #H; nnormalize; #H1;
208 ndestruct (*napply (bool_destruct … H1)*)
209 ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
210 (* !!! ndestruct: assert false *)
211 napply (list_destruct_nil_cons T … H2)
213 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
214 ##[ ##1: #H1; #H2; nnormalize; #H3;
215 (* !!! ndestruct: assert false *)
216 napply (list_destruct_cons_nil T … H3)
217 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
218 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
219 napply (H ll2 H1 ? (list_destruct_2 T … H3));
220 napply (or2_elim ??? (andb_false2 … H2) );
221 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
222 ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
223 ##| ##2: napply (H1 … H4)
225 ##| ##2: #H4; napply H4
232 : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2.
233 #T; #H; #h1; #h2; #l1; nelim l1;
234 ##[ ##1: #l2; ncases l2;
235 ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
236 nnormalize; #H2; nrewrite > H2 in H1:(%);
237 nnormalize; #H1; napply (H1 (refl_eq …))
238 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
240 (* !!! ndestruct: assert false *)
241 napply (list_destruct_nil_cons T … H2)
243 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
244 ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
246 (* !!! ndestruct: assert false *)
247 napply (list_destruct_cons_nil T … H3)
248 ##| ##2: #hh2; #ll2; #H2;
249 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
250 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
251 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
252 nrewrite > H3 in H2:(%); #H2;
253 nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
254 nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
255 napply (H2 (refl_eq …))
261 nlemma neq_to_nbfoldrightlist2
262 : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T.
263 (∀x,y:T.decidable (x = y)) →
264 (∀x,y.(x ≠ y → f x y = false)) →
265 (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false).
268 ##[ ##1: #l2; ncases l2;
269 ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …))
270 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
272 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
273 ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq
274 ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
275 nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
276 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …);
277 ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
278 ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
279 nrewrite > (symmetric_andbool (f hh1 hh2) false);
280 nnormalize; napply refl_eq
286 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
290 ##[ ##1: #H; napply I
291 ##| ##2: #x; #l; #H; ndestruct (*napply (bool_destruct … H)*)
295 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
299 ##[ ##1: #H; ndestruct (*napply (bool_destruct … H)*)
300 ##| ##2: #x; #l; #H; napply I
308 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.
311 ##[ ##1: #h; #l2; ncases l2; nnormalize;
312 ##[ ##1: #H; #H1; napply refl_eq
313 ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
315 ##| ##2: #h; #l2; ncases l2; nnormalize;
316 ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
317 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
322 nlemma symmetric_foldrightnelist2_aux
323 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
324 ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
325 (∀x,y,z.f x y z = f y x z) →
326 fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
327 #T1; #T2; #f; #acc; #l1;
329 ##[ ##1: #h; #l2; ncases l2;
330 ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
331 ##| ##2: #h1; #l; ncases l;
332 ##[ ##1: #h3; #H1; #H2; #H3;
333 nchange in H1:(%) with ((S O) = (S (S O)));
334 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
335 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
336 ##| ##2: #h3; #l3; #H1; #H2; #H3;
337 nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
338 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
339 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
342 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
343 ##[ ##1: #h4; ncases l3;
344 ##[ ##1: #h5; #H1; #H2; #H3;
345 nchange in H1:(%) with ((S (S O)) = (S O));
346 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
347 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
348 ##| ##2: #h5; #l5; #H1; #H2; #H3;
349 nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
350 (* !!! ndestruct: si inceppa su un'ipotesi che non e' H1 *)
351 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
353 ##| ##2: #h4; #l4; #H1; #H2; #H3;
354 nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
355 nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
356 nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
357 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
358 nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
359 nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
365 nlemma symmetric_foldrightnelist2
366 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
367 (∀x,y,z.f x y z = f y x z) →
368 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).
369 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
370 nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
374 nlemma symmetric_bfoldrightnelist2
375 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
376 (∀x,y.f x y = f y x) →
377 bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
380 ##[ ##1: #hh1; #l2; ncases l2;
381 ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
382 ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
384 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
385 ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
386 ##| ##2: #hh2; #ll2; #H1; nnormalize;
387 nrewrite > (H ll2 H1);
388 nrewrite > (H1 hh1 hh2);
394 nlemma bfoldrightnelist2_to_eq
395 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
396 (∀x,y.(f x y = true → x = y)) →
397 (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
400 ##[ ##1: #hh1; #l2; ncases l2;
401 ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
402 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; ndestruct (*napply (bool_destruct … H1)*)
404 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
405 ##[ ##1: #hh2; #H1; nnormalize; #H2; ndestruct (*napply (bool_destruct … H2)*)
406 ##| ##2: #hh2; #ll2; #H1; #H2;
407 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
408 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
409 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
415 nlemma eq_to_bfoldrightnelist2
416 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
417 (∀x,y.(x = y → f x y = true)) →
418 (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
421 ##[ ##1: #hh1; #l2; ncases l2;
422 ##[ ##1: #hh2; #H; #H1; nnormalize;
423 nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
425 ##| ##2: #hh2; #ll2; #H; #H1;
426 (* !!! ndestruct: assert false *)
427 nelim (nelist_destruct_nil_cons ???? H1)
429 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
430 ##[ ##1: #hh2; #H1; #H2;
431 (* !!! ndestruct: assert false *)
432 nelim (nelist_destruct_cons_nil ???? H2)
433 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
434 nrewrite > (nelist_destruct_cons_cons_1 … H2);
435 nrewrite > (H1 hh2 hh2 (refl_eq …));
437 nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
443 nlemma bfoldrightnelist2_to_lennelist
444 : ∀T.∀f:T → T → bool.∀l1,l2:ne_list T.bfold_right_neList2 T f l1 l2 = true → len_neList T l1 = len_neList T l2.
447 ##[ ##1: #hh1; #l2; ncases l2;
448 ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
449 ##| ##2: nnormalize; #hh2; #tt2; #H; ndestruct (*napply (bool_destruct … H)*)
451 ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
452 ##[ ##1: nnormalize; #hh2; #H1; ndestruct (*napply (bool_destruct … H1)*)
453 ##| ##2: #hh2; #tt2; #H1; nnormalize;
454 nrewrite > (H tt2 ?);
455 ##[ ##1: napply refl_eq
456 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
457 napply (andb_true_true_r … H1)
463 nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y).
465 ##[ ##1: #hh1; #y; ncases y;
466 ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
467 ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
468 ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
469 #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
471 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
473 (* !!! ndestruct: assert false *)
474 napply (nelist_destruct_nil_cons T … H1)
476 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
477 ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
479 (* !!! ndestruct: assert false *)
480 napply (nelist_destruct_cons_nil T … H2)
481 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
482 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
483 nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
484 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
485 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
486 nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
487 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
488 nrewrite > H2; nrewrite > H3; napply refl_eq
495 nlemma nbfoldrightnelist2_to_neq
496 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
497 (∀x,y.(f x y = false → x ≠ y)) →
498 (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2).
501 ##[ ##1: #hh1; #l2; ncases l2;
502 ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
503 ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2;
504 (* !!! ndestruct: assert false *)
505 napply (nelist_destruct_nil_cons T … H2)
507 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
508 ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3;
509 (* !!! ndestruct: assert false *)
510 napply (nelist_destruct_cons_nil T … H3)
511 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
512 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
513 napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
514 napply (or2_elim ??? (andb_false2 … H2) );
515 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
516 ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
517 ##| ##2: napply (H1 … H4)
519 ##| ##2: #H4; napply H4
525 nlemma nelist_destruct
526 : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2.
527 #T; #H; #h1; #h2; #l1; nelim l1;
528 ##[ ##1: #hh1; #l2; ncases l2;
529 ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
530 ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
531 ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
532 napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
533 ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
534 nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
535 ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
538 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
540 (* !!! ndestruct: assert false *)
541 napply (nelist_destruct_nil_cons T … H2)
543 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
544 ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
546 (* !!! ndestruct: assert false *)
547 napply (nelist_destruct_cons_nil T … H3)
548 ##| ##2: #hh2; #ll2; #H2;
549 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
550 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
551 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
552 nrewrite > H3 in H2:(%); #H2;
553 nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
554 nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
555 napply (H2 (refl_eq …))
561 nlemma neq_to_nbfoldrightnelist2
562 : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T.
563 (∀x,y:T.decidable (x = y)) →
564 (∀x,y.(x ≠ y → f x y = false)) →
565 (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false).
568 ##[ ##1: #hh1; #l2; ncases l2;
569 ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?);
570 nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
571 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
573 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
574 ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq
575 ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
576 nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
577 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …);
578 ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
579 ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
580 nrewrite > (symmetric_andbool (f hh1 hh2) false);
581 nnormalize; napply refl_eq