2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department of the University of Bologna, Italy.
7 ||A|| This file is distributed under the terms of the
8 \ / GNU General Public License Version 2
10 V_______________________________________________________________ *)
12 include "arithmetics/bounded_quantifiers.ma".
13 include "basics/lists/list.ma".
15 (* A bit of combinatorics *)
16 interpretation "list membership" 'mem a l = (mem ? a l).
18 lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
20 [%2 % @False_ind |#a #tl #Htl @decidable_or //]
23 lemma length_unique_le: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| ≤ n.
25 [* // #a #tl #_ #H @False_ind @(absurd (a < 0))
26 [@H %1 % | @le_to_not_lt //]
27 |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
28 lapply (length_filter_eqb … m l Huni) #Hle
29 @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
34 [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
35 cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
36 @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
37 @injective_notb @(mem_filter_true ???? memx)
43 lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l →
44 (∀x. x ∈ l → x ≤ n) → n ∈ l.
45 #n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) //
46 #H4 @False_ind @(absurd (|l| > n))
48 |@le_to_not_lt @length_unique_le //
49 #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
50 #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
54 lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l →
55 (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
57 [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
58 |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
59 [#leim @(mem_filter… (λi.¬(eqb m i)))
60 cases (filter_eqb m … H1)
61 [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
62 #x #memx @le_S_S_to_le @H2 //]
63 * #memm #Hfilter @Hind
64 [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
66 |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
68 |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
69 @injective_notb >(mem_filter_true ???? memx) %
73 |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
78 lemma lt_length_to_not_mem: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| < n →
79 ∃i. i < n ∧ ¬ (i ∈ l).
81 [#l #_ #_ #H @False_ind /2/
82 |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
84 |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
85 [#i * #ltim #memi %{i} % [@le_S // ]
86 @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
87 @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
89 |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
91 |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
92 @injective_notb >(mem_filter_true ???? memx) %
95 |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H