include "arithmetics/bounded_quantifiers.ma".
-include "basics/list.ma".
+include "basics/lists/search.ma".
(* A bit of combinatorics *)
interpretation "list membership" 'mem a l = (mem ? a l).
-lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
+\ 5img class="anchor" src="icons/tick.png" id="decidable_mem_nat"\ 6lemma decidable_mem_nat: ∀n:\ 5a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"\ 6nat\ 5/a\ 6.∀l. \ 5a href="cic:/matita/basics/logic/decidable.def(1)"\ 6decidable\ 5/a\ 6 (n \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l).
#n #l elim l
- [%2 % @False_ind |#a #tl #Htl @decidable_or //]
+ [%2 % @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 |#a #tl #Htl @\ 5a href="cic:/matita/arithmetics/bounded_quantifiers/decidable_or.def(3)"\ 6decidable_or\ 5/a\ 6 //]
qed.
-lemma length_unique_le: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| ≤ n.
+\ 5img class="anchor" src="icons/tick.png" id="length_unique_le"\ 6lemma length_unique_le: ∀n,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n.
#n elim n
- [* // #a #tl #_ #H @False_ind @(absurd (a < 0))
- [@H %1 % | @le_to_not_lt //]
- |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
- lapply (length_filter_eqb … m l Huni) #Hle
- @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
- [@le_plus //
- |@le_S_S @Hind
- [@unique_filter //
- |#x #memx cut (x ≤ m)
- [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
- cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
- @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
- @injective_notb @(mem_filter_true ???? memx)
+ [* // #a #tl #_ #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 (a \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 \ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 60\ 5/a\ 6))
+ [@H %1 % | @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //]
+ |#m #Hind #l #Huni #Hmem <(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l)
+ lapply (\ 5a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"\ 6length_filter_eqb\ 5/a\ 6 … m l Huni) #Hle
+ @(\ 5a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"\ 6transitive_le\ 5/a\ 6 ? (\ 5a title="natural number" href="cic:/fakeuri.def(1)"\ 61\ 5/a\ 6\ 5a title="natural plus" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6|\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m x) l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6))
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 @Hind
+ [@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
+ |#x #memx cut (x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m)
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @Hmem @(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)] #Hcut
+ cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … Hcut) // #eqxm @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6
+ @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ? eqxm) @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx)
]
]
]
qed.
-lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l →
- (∀x. x ∈ l → x ≤ n) → n ∈ l.
-#n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) //
-#H4 @False_ind @(absurd (|l| > n))
+\ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem"\ 6lemma eq_length_to_mem : ∀n,l. |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"\ 6S\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l →
+ (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 n) → n \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l.
+#n #l #H1 #H2 #H3 cases (\ 5a href="cic:/matita/arithmetics/pidgeon_hole/decidable_mem_nat.def(6)"\ 6decidable_mem_nat\ 5/a\ 6 n l) //
+#H4 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 (|l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'greater than'" href="cic:/fakeuri.def(1)"\ 6>\ 5/a\ 6 n))
[>H1 //
- |@le_to_not_lt @length_unique_le //
- #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
- #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/length_unique_le.def(9)"\ 6length_unique_le\ 5/a\ 6 //
+ #x #memx cases(\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (H3 x memx)) //
+ #Heq @\ 5a href="cic:/matita/arithmetics/nat/not_le_to_lt.def(5)"\ 6not_le_to_lt\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H4) #_ <Heq //
]
qed.
-lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l →
- (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
+\ 5img class="anchor" src="icons/tick.png" id="eq_length_to_mem_all"\ 6lemma eq_length_to_mem_all: ∀n,l. |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 n → \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l →
+ (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → ∀i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n → i \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l.
#n elim n
- [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
- |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
- [#leim @(mem_filter… (λi.¬(eqb m i)))
- cases (filter_eqb m … H1)
- [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
- #x #memx @le_S_S_to_le @H2 //]
+ [#l #_ #_ #_ #i #lti0 @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ? lti0 (\ 5a href="cic:/matita/arithmetics/nat/not_le_Sn_O.def(3)"\ 6not_le_Sn_O\ 5/a\ 6 ?))
+ |#m #Hind #l #H #H1 #H2 #i #lei cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … lei)
+ [#leim @(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6… (λi.\ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m i)))
+ cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m … H1)
+ [2: * #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 ?? H) @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"\ 6eq_length_to_mem\ 5/a\ 6 //
+ #x #memx @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H2 //]
* #memm #Hfilter @Hind
- [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
- |@unique_filter @H1
- |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
- [@le_S_S_to_le @H3
- |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
- @injective_notb >(mem_filter_true ???? memx) %
+ [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 <H <(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 ? (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m) l) >Hfilter %
+ |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 @H1
+ |#x #memx cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (H2 x (\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx))) #H3
+ [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H3
+ |@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 (m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 //] @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx) %
]
- |@le_S_S_to_le @leim
+ |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @leim
]
- |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
+ |#eqi @\ 5a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"\ 6eq_length_to_mem\ 5/a\ 6 >eqi [@H |@H1 |#x #Hx @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 >eqi @H2 //]
]
]
qed.
-lemma lt_length_to_not_mem: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| < n →
-∃i. i < n ∧ ¬ (i ∈ l).
+\ 5img class="anchor" src="icons/tick.png" id="lt_length_to_not_mem"\ 6lemma lt_length_to_not_mem: ∀n,l. \ 5a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"\ 6unique\ 5/a\ 6 ? l → (∀x. x \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l → x \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n) → |l\ 5a title="list length" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6 \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n →
+\ 5a title="exists" href="cic:/fakeuri.def(1)"\ 6∃\ 5/a\ 6i. i \ 5a title="natural 'less than'" href="cic:/fakeuri.def(1)"\ 6<\ 5/a\ 6 n \ 5a title="logical and" href="cic:/fakeuri.def(1)"\ 6∧\ 5/a\ 6 \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 (i \ 5a title="list membership" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 l).
#n elim n
- [#l #_ #_ #H @False_ind /2/
- |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
+ [#l #_ #_ #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#m #Hind #l #Huni #Hmem #Hlen cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m … Huni)
[2: * #H #_ %{m} % //
- |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
- [#i * #ltim #memi %{i} % [@le_S // ]
- @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
- @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
- |@unique_filter //
- |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
- [#H @le_S_S_to_le @H
- |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
- @injective_notb >(mem_filter_true ???? memx) %
- |@(mem_filter … memx)
+ |* #memm #Hfilter cases (Hind (\ 5a href="cic:/matita/basics/lists/search/filter.def(2)"\ 6filter\ 5/a\ 6 ? (λx. \ 5a title="boolean not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6(\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m x)) l) ? ? ?)
+ [#i * #ltim #memi %{i} % [@\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 // ]
+ @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … memi) @\ 5a href="cic:/matita/basics/lists/search/mem_filter_l.def(4)"\ 6mem_filter_l\ 5/a\ 6 @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >\ 5a href="cic:/matita/basics/bool/notb_notb.def(2)"\ 6notb_notb\ 5/a\ 6
+ @\ 5a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"\ 6not_eq_to_eqb_false\ 5/a\ 6 @\ 5a href="cic:/matita/basics/logic/sym_not_eq.def(4)"\ 6sym_not_eq\ 5/a\ 6 @\ 5a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"\ 6lt_to_not_eq\ 5/a\ 6 //
+ |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
+ |#x #memx cases (\ 5a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"\ 6le_to_or_lt_eq\ 5/a\ 6 … (Hmem x ?))
+ [#H @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
+ |#H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6 (m\ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6x)) [@\ 5a href="cic:/matita/arithmetics/nat/injective_S.def(4)"\ 6injective_S\ 5/a\ 6 //] @\ 5a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"\ 6eqb_false_to_not_eq\ 5/a\ 6
+ @\ 5a href="cic:/matita/basics/bool/injective_notb.def(4)"\ 6injective_notb\ 5/a\ 6 >(\ 5a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"\ 6mem_filter_true\ 5/a\ 6 ???? memx) %
+ |@(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)
]
- |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
- @le_S_S_to_le @H
+ |<(\ 5a href="cic:/matita/basics/lists/search/filter_length2.def(5)"\ 6filter_length2\ 5/a\ 6 … (\ 5a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"\ 6eqb\ 5/a\ 6 m)) in Hlen; >Hfilter #H
+ @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
]
]
]
projects / helm.git / blobdiff