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 (* Ultima modifica: 05/08/2009 *)
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; 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 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 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; napply (bool_destruct … H1)
111 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
112 ##[ ##1: #H1; nnormalize; #H2; napply (bool_destruct … H2)
113 ##| ##2: #hh2; #ll2; #H1; #H2;
114 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = true);
115 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
116 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
122 nlemma eq_to_bfoldrightlist2
123 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
124 (∀x,y.(x = y → f x y = true)) →
125 (l1 = l2 → bfold_right_list2 T1 f l1 l2 = true).
128 ##[ ##1: #l2; ncases l2;
129 ##[ ##1: #H; #H1; nnormalize; napply refl_eq
130 ##| ##2: #hh2; #ll2; #H; #H1; nelim (list_destruct_nil_cons ??? H1)
132 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
133 ##[ ##1: #H1; #H2; nelim (list_destruct_cons_nil ??? H2)
134 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
135 nrewrite > (list_destruct_1 … H2);
136 nrewrite > (H1 hh2 hh2 (refl_eq …));
138 nrewrite > (H ll2 H1 (list_destruct_2 … H2));
144 nlemma bfoldrightlist2_to_lenlist
145 : ∀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.
148 ##[ ##1: #l2; ncases l2;
149 ##[ ##1: nnormalize; #H; napply refl_eq
150 ##| ##2: nnormalize; #hh; #tt; #H; napply (bool_destruct … H)
152 ##| ##2: #hh; #tt; #H; #l2; ncases l2;
153 ##[ ##1: nnormalize; #H1; napply (bool_destruct … H1)
154 ##| ##2: #hh1; #tt1; #H1; nnormalize;
155 nrewrite > (H tt1 ?);
156 ##[ ##1: napply refl_eq
157 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_list2 T f tt tt1)) = true);
158 napply (andb_true_true_r … H1)
164 nlemma decidable_list : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:list T.decidable (x = y).
166 ##[ ##1: #y; ncases y;
167 ##[ ##1: nnormalize; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
168 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
169 nnormalize; #H1; napply (list_destruct_nil_cons T … H1)
171 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
172 ##[ ##1: nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
173 nnormalize; #H2; napply (list_destruct_cons_nil T … H2)
174 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
175 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
176 nnormalize; #H3; napply (H2 (list_destruct_1 T … H3))
177 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
178 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
179 nnormalize; #H4; napply (H3 (list_destruct_2 T … H4))
180 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
181 nrewrite > H2; nrewrite > H3; napply refl_eq
188 nlemma nbfoldrightlist2_to_neq
189 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:list T1.
190 (∀x,y.(f x y = false → x ≠ y)) →
191 (bfold_right_list2 T1 f l1 l2 = false → l1 ≠ l2).
194 ##[ ##1: #l2; ncases l2;
195 ##[ ##1: #H; nnormalize; #H1; napply (bool_destruct … H1)
196 ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
198 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
199 ##[ ##1: #H1; #H2; nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
200 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
201 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
202 napply (H ll2 H1 ? (list_destruct_2 T … H3));
203 napply (or2_elim ??? (andb_false2 … H2) );
204 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
205 ##[ ##1: nrewrite > (list_destruct_1 T … H3); napply refl_eq
206 ##| ##2: napply (H1 … H4)
208 ##| ##2: #H4; napply H4
215 : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:list T.(h1::l1) ≠ (h2::l2) → h1 ≠ h2 ∨ l1 ≠ l2.
216 #T; #H; #h1; #h2; #l1; nelim l1;
217 ##[ ##1: #l2; ncases l2;
218 ##[ ##1: #H1; napply (or2_intro1 (h1 ≠ h2) ([] ≠ []) …);
219 nnormalize; #H2; nrewrite > H2 in H1:(%);
220 nnormalize; #H1; napply (H1 (refl_eq …))
221 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) ([] ≠ (hh2::ll2)) …);
222 nnormalize; #H2; napply (list_destruct_nil_cons T … H2)
224 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
225 ##[ ##1: #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ []) …);
226 nnormalize; #H3; napply (list_destruct_cons_nil T … H3)
227 ##| ##2: #hh2; #ll2; #H2;
228 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
229 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2)) H3)
230 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1::ll1) ≠ (hh2::ll2) …));
231 nrewrite > H3 in H2:(%); #H2;
232 nnormalize; #H4; nrewrite > (list_destruct_1 T … H4) in H2:(%); #H2;
233 nrewrite > (list_destruct_2 T … H4) in H2:(%); #H2;
234 napply (H2 (refl_eq …))
240 nlemma neq_to_nbfoldrightlist2
241 : ∀T:Type.∀f:T → T → bool.∀l1,l2:list T.
242 (∀x,y:T.decidable (x = y)) →
243 (∀x,y.(x ≠ y → f x y = false)) →
244 (l1 ≠ l2 → bfold_right_list2 T f l1 l2 = false).
247 ##[ ##1: #l2; ncases l2;
248 ##[ ##1: #H; #H1; nnormalize; #H2; nelim (H2 (refl_eq …))
249 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
251 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
252 ##[ ##1: #H1; #H2; nnormalize; #H3; napply refl_eq
253 ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
254 nchange with (((f hh1 hh2)⊗(bfold_right_list2 T f ll1 ll2)) = false);
255 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (list_destruct T H1 … H3) …);
256 ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
257 ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
258 nrewrite > (symmetric_andbool (f hh1 hh2) false);
259 nnormalize; napply refl_eq
265 nlemma isbemptylist_to_isemptylist : ∀T,l.isb_empty_list T l = true → is_empty_list T l.
269 ##[ ##1: #H; napply I
270 ##| ##2: #x; #l; #H; napply (bool_destruct … H)
274 nlemma isnotbemptylist_to_isnotemptylist : ∀T,l.isnotb_empty_list T l = true → isnot_empty_list T l.
278 ##[ ##1: #H; napply (bool_destruct … H)
279 ##| ##2: #x; #l; #H; napply I
287 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.
290 ##[ ##1: #h; #l2; ncases l2; nnormalize;
291 ##[ ##1: #H; #H1; napply refl_eq
292 ##| ##2: #h; #t; #H; nrewrite > H; napply refl_eq
294 ##| ##2: #h; #l2; ncases l2; nnormalize;
295 ##[ ##1: #h1; #H; #l; #H1; nrewrite < H1; napply refl_eq
296 ##| ##2: #h; #l; #H; #l3; #H1; nrewrite < H1; napply refl_eq
301 nlemma symmetric_foldrightnelist2_aux
302 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.
303 ∀H1:len_neList T1 l1 = len_neList T1 l2.∀H2:len_neList T1 l2 = len_neList T1 l1.
304 (∀x,y,z.f x y z = f y x z) →
305 fold_right_neList2 T1 T2 f acc l1 l2 H1 = fold_right_neList2 T1 T2 f acc l2 l1 H2.
306 #T1; #T2; #f; #acc; #l1;
308 ##[ ##1: #h; #l2; ncases l2;
309 ##[ ##1: #h1; nnormalize; #H1; #H2; #H3; nrewrite > (H3 h h1 acc); napply refl_eq
310 ##| ##2: #h1; #l; ncases l;
311 ##[ ##1: #h3; #H1; #H2; #H3;
312 nchange in H1:(%) with ((S O) = (S (S O)));
313 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
314 ##| ##2: #h3; #l3; #H1; #H2; #H3;
315 nchange in H1:(%) with ((S O) = (S (S (len_neList ? l3))));
316 nelim (nat_destruct_0_S ? (nat_destruct_S_S … H1))
319 ##| ##2: #h3; #l3; #H; #l2; ncases l2;
320 ##[ ##1: #h4; ncases l3;
321 ##[ ##1: #h5; #H1; #H2; #H3;
322 nchange in H1:(%) with ((S (S O)) = (S O));
323 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
324 ##| ##2: #h5; #l5; #H1; #H2; #H3;
325 nchange in H1:(%) with ((S (S (len_neList ? l5))) = (S O));
326 nelim (nat_destruct_S_0 ? (nat_destruct_S_S … H1))
328 ##| ##2: #h4; #l4; #H1; #H2; #H3;
329 nchange in H1:(%) with ((S (len_neList ? l3)) = (S (len_neList ? l4)));
330 nchange in H2:(%) with ((S (len_neList ? l4)) = (S (len_neList ? l3)));
331 nchange with ((f h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 ?))) =
332 (f h4 h3 (fold_right_neList2 T1 T2 f acc l4 l3 (fold_right_neList2_aux3 T1 h4 h3 l4 l3 ?))));
333 nrewrite < (H l4 (fold_right_neList2_aux3 T1 h3 h4 l3 l4 H1) (fold_right_neList2_aux3 T1 h4 h3 l4 l3 H2) H3);
334 nrewrite > (H3 h3 h4 (fold_right_neList2 T1 T2 f acc l3 l4 ?));
340 nlemma symmetric_foldrightnelist2
341 : ∀T1,T2:Type.∀f:T1 → T1 → T2 → T2.∀acc:T2.∀l1,l2:ne_list T1.∀H:len_neList T1 l1 = len_neList T1 l2.
342 (∀x,y,z.f x y z = f y x z) →
343 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).
344 #T1; #T2; #f; #acc; #l1; #l2; #H; #H1;
345 nrewrite > (symmetric_foldrightnelist2_aux T1 T2 f acc l1 l2 H (symmetric_lennelist T1 l1 l2 H) H1);
349 nlemma symmetric_bfoldrightnelist2
350 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
351 (∀x,y.f x y = f y x) →
352 bfold_right_neList2 T1 f l1 l2 = bfold_right_neList2 T1 f l2 l1.
355 ##[ ##1: #hh1; #l2; ncases l2;
356 ##[ ##1: #hh2; #H; nnormalize; nrewrite > (H hh1 hh2); napply refl_eq
357 ##| ##2: #hh2; #ll2; #H; nnormalize; napply refl_eq
359 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
360 ##[ ##1: #hh2; #H1; nnormalize; napply refl_eq
361 ##| ##2: #hh2; #ll2; #H1; nnormalize;
362 nrewrite > (H ll2 H1);
363 nrewrite > (H1 hh1 hh2);
369 nlemma bfoldrightnelist2_to_eq
370 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
371 (∀x,y.(f x y = true → x = y)) →
372 (bfold_right_neList2 T1 f l1 l2 = true → l1 = l2).
375 ##[ ##1: #hh1; #l2; ncases l2;
376 ##[ ##1: #hh2; #H; #H1; nnormalize in H1:(%); nrewrite > (H hh1 hh2 H1); napply refl_eq
377 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; napply (bool_destruct … H1)
379 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
380 ##[ ##1: #hh2; #H1; nnormalize; #H2; napply (bool_destruct … H2)
381 ##| ##2: #hh2; #ll2; #H1; #H2;
382 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = true);
383 nrewrite > (H1 hh1 hh2 (andb_true_true_l … H2));
384 nrewrite > (H ll2 H1 (andb_true_true_r … H2));
390 nlemma eq_to_bfoldrightnelist2
391 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
392 (∀x,y.(x = y → f x y = true)) →
393 (l1 = l2 → bfold_right_neList2 T1 f l1 l2 = true).
396 ##[ ##1: #hh1; #l2; ncases l2;
397 ##[ ##1: #hh2; #H; #H1; nnormalize;
398 nrewrite > (H hh1 hh2 (nelist_destruct_nil_nil … H1));
400 ##| ##2: #hh2; #ll2; #H; #H1; nelim (nelist_destruct_nil_cons ???? H1)
402 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
403 ##[ ##1: #hh2; #H1; #H2; nelim (nelist_destruct_cons_nil ???? H2)
404 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize;
405 nrewrite > (nelist_destruct_cons_cons_1 … H2);
406 nrewrite > (H1 hh2 hh2 (refl_eq …));
408 nrewrite > (H ll2 H1 (nelist_destruct_cons_cons_2 … H2));
414 nlemma bfoldrightnelist2_to_lennelist
415 : ∀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.
418 ##[ ##1: #hh1; #l2; ncases l2;
419 ##[ ##1: nnormalize; #hh2; #H; napply refl_eq
420 ##| ##2: nnormalize; #hh2; #tt2; #H; napply (bool_destruct … H)
422 ##| ##2: #hh1; #tt1; #H; #l2; ncases l2;
423 ##[ ##1: nnormalize; #hh2; #H1; napply (bool_destruct … H1)
424 ##| ##2: #hh2; #tt2; #H1; nnormalize;
425 nrewrite > (H tt2 ?);
426 ##[ ##1: napply refl_eq
427 ##| ##2: nchange in H1:(%) with ((? ⊗ (bfold_right_neList2 T f tt1 tt2)) = true);
428 napply (andb_true_true_r … H1)
434 nlemma decidable_nelist : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀x,y:ne_list T.decidable (x = y).
436 ##[ ##1: #hh1; #y; ncases y;
437 ##[ ##1: #hh2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H hh1 hh2));
438 ##[ ##1: #H1; nrewrite > H1; napply (or2_intro1 (? = ?) (? ≠ ?) (refl_eq …))
439 ##| ##2: #H1; napply (or2_intro2 (? = ?) (? ≠ ?) ?); nnormalize;
440 #H2; napply (H1 (nelist_destruct_nil_nil T … H2))
442 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
443 nnormalize; #H1; napply (nelist_destruct_nil_cons T … H1)
445 ##| ##2: #hh1; #tt1; #H1; #y; ncases y;
446 ##[ ##1: #hh1; nnormalize; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
447 nnormalize; #H2; napply (nelist_destruct_cons_nil T … H2)
448 ##| ##2: #hh2; #tt2; nnormalize; napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …));
449 ##[ ##2: #H2; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
450 nnormalize; #H3; napply (H2 (nelist_destruct_cons_cons_1 T … H3))
451 ##| ##1: #H2; napply (or2_elim (tt1 = tt2) (tt1 ≠ tt2) ? (H1 tt2));
452 ##[ ##2: #H3; napply (or2_intro2 (? = ?) (? ≠ ?) ?);
453 nnormalize; #H4; napply (H3 (nelist_destruct_cons_cons_2 T … H4))
454 ##| ##1: #H3; napply (or2_intro1 (? = ?) (? ≠ ?) ?);
455 nrewrite > H2; nrewrite > H3; napply refl_eq
462 nlemma nbfoldrightnelist2_to_neq
463 : ∀T1:Type.∀f:T1 → T1 → bool.∀l1,l2:ne_list T1.
464 (∀x,y.(f x y = false → x ≠ y)) →
465 (bfold_right_neList2 T1 f l1 l2 = false → l1 ≠ l2).
468 ##[ ##1: #hh1; #l2; ncases l2;
469 ##[ ##1: #hh2; #H; nnormalize; #H1; #H2; napply (H hh1 hh2 H1 (nelist_destruct_nil_nil T … H2))
470 ##| ##2: #hh2; #ll2; #H; #H1; nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
472 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
473 ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
474 ##| ##2: #hh2; #ll2; #H1; #H2; nnormalize; #H3;
475 nchange in H2:(%) with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
476 napply (H ll2 H1 ? (nelist_destruct_cons_cons_2 T … H3));
477 napply (or2_elim ??? (andb_false2 … H2) );
478 ##[ ##1: #H4; napply (absurd (hh1 = hh2) …);
479 ##[ ##1: nrewrite > (nelist_destruct_cons_cons_1 T … H3); napply refl_eq
480 ##| ##2: napply (H1 … H4)
482 ##| ##2: #H4; napply H4
488 nlemma nelist_destruct
489 : ∀T.∀H:(Πx,y:T.decidable (x = y)).∀h1,h2:T.∀l1,l2:ne_list T.(h1§§l1) ≠ (h2§§l2) → h1 ≠ h2 ∨ l1 ≠ l2.
490 #T; #H; #h1; #h2; #l1; nelim l1;
491 ##[ ##1: #hh1; #l2; ncases l2;
492 ##[ ##1: #hh2; #H1; napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H …) …);
493 ##[ ##2: #H2; napply (or2_intro1 (h1 ≠ h2) («£hh1» ≠ «£hh2») H2)
494 ##| ##1: #H2; nrewrite > H2 in H1:(%); #H1;
495 napply (or2_elim (hh1 = hh2) (hh1 ≠ hh2) ? (H …) …);
496 ##[ ##2: #H3; napply (or2_intro2 (h2 ≠ h2) («£hh1» ≠ «£hh2») ?);
497 nnormalize; #H4; napply (H3 (nelist_destruct_nil_nil T … H4))
498 ##| ##1: #H3; nrewrite > H3 in H1:(%); #H1; nelim (H1 (refl_eq …))
501 ##| ##2: #hh2; #ll2; #H1; napply (or2_intro2 (h1 ≠ h2) («£hh1» ≠ (hh2§§ll2)) …);
502 nnormalize; #H2; napply (nelist_destruct_nil_cons T … H2)
504 ##| ##2: #hh1; #ll1; #H1; #l2; ncases l2;
505 ##[ ##1: #hh2; #H2; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ «£hh2») …);
506 nnormalize; #H3; napply (nelist_destruct_cons_nil T … H3)
507 ##| ##2: #hh2; #ll2; #H2;
508 napply (or2_elim (h1 = h2) (h1 ≠ h2) ? (H h1 h2) …);
509 ##[ ##2: #H3; napply (or2_intro1 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2)) H3)
510 ##| ##1: #H3; napply (or2_intro2 (h1 ≠ h2) ((hh1§§ll1) ≠ (hh2§§ll2) …));
511 nrewrite > H3 in H2:(%); #H2;
512 nnormalize; #H4; nrewrite > (nelist_destruct_cons_cons_1 T … H4) in H2:(%); #H2;
513 nrewrite > (nelist_destruct_cons_cons_2 T … H4) in H2:(%); #H2;
514 napply (H2 (refl_eq …))
520 nlemma neq_to_nbfoldrightnelist2
521 : ∀T:Type.∀f:T → T → bool.∀l1,l2:ne_list T.
522 (∀x,y:T.decidable (x = y)) →
523 (∀x,y.(x ≠ y → f x y = false)) →
524 (l1 ≠ l2 → bfold_right_neList2 T f l1 l2 = false).
527 ##[ ##1: #hh1; #l2; ncases l2;
528 ##[ ##1: #hh2; #H; #H1; nnormalize; #H2; napply (H1 hh1 hh2 ?);
529 nnormalize; #H3; nrewrite > H3 in H2:(%); #H2; napply (H2 (refl_eq …))
530 ##| ##2: #hh2; #ll2; #H; nnormalize; #H1; #H2; napply refl_eq
532 ##| ##2: #hh1; #ll1; #H; #l2; ncases l2;
533 ##[ ##1: #hh2; #H1; #H2; nnormalize; #H3; napply refl_eq
534 ##| ##2: #hh2; #ll2; #H1; #H2; #H3;
535 nchange with (((f hh1 hh2)⊗(bfold_right_neList2 T f ll1 ll2)) = false);
536 napply (or2_elim (hh1 ≠ hh2) (ll1 ≠ ll2) ? (nelist_destruct T H1 … H3) …);
537 ##[ ##1: #H4; nrewrite > (H2 hh1 hh2 H4); nnormalize; napply refl_eq
538 ##| ##2: #H4; nrewrite > (H ll2 H1 H2 H4);
539 nrewrite > (symmetric_andbool (f hh1 hh2) false);
540 nnormalize; napply refl_eq