X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=weblib%2Farithmetics%2Fpidgeon_hole.ma;h=c7c1f701600600350c21c159d7cb0e3bf6a65fbf;hb=adfe97c3044e996cc691d760578ba6c91ce386bd;hp=e4aed1629c8de86ad6e27df017fa69b63e569f49;hpb=8c057e95fd8d88bcc74a2335482b16eedd0ee60c;p=helm.git diff --git a/weblib/arithmetics/pidgeon_hole.ma b/weblib/arithmetics/pidgeon_hole.ma index e4aed1629..c7c1f7016 100644 --- a/weblib/arithmetics/pidgeon_hole.ma +++ b/weblib/arithmetics/pidgeon_hole.ma @@ -1,89 +1,89 @@ 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). +img class="anchor" src="icons/tick.png" id="decidable_mem_nat"lemma decidable_mem_nat: ∀n:a href="cic:/matita/arithmetics/nat/nat.ind(1,0,0)"nat/a.∀l. a href="cic:/matita/basics/logic/decidable.def(1)"decidable/a (n a title="list membership" href="cic:/fakeuri.def(1)"∈/a l). #n #l elim l - [%2 % @False_ind |#a #tl #Htl @decidable_or //] + [%2 % @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a |#a #tl #Htl @a href="cic:/matita/arithmetics/bounded_quantifiers/decidable_or.def(3)"decidable_or/a //] qed. -lemma length_unique_le: ∀n,l. unique ? l → (∀x. x ∈ l → x < n) → |l| ≤ n. +img class="anchor" src="icons/tick.png" id="length_unique_le"lemma length_unique_le: ∀n,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n) → |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a 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 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a (a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a a title="natural number" href="cic:/fakeuri.def(1)"0/a)) + [@H %1 % | @a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"le_to_not_lt/a //] + |#m #Hind #l #Huni #Hmem <(a href="cic:/matita/basics/lists/search/filter_length2.def(5)"filter_length2/a ? (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m) l) + lapply (a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"length_filter_eqb/a … m l Huni) #Hle + @(a href="cic:/matita/arithmetics/nat/transitive_le.def(3)"transitive_le/a ? (a title="natural number" href="cic:/fakeuri.def(1)"1/aa title="natural plus" href="cic:/fakeuri.def(1)"+/a|a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (λx.a title="boolean not" href="cic:/fakeuri.def(1)"¬/a a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m x) la title="list length" href="cic:/fakeuri.def(1)"|/a)) + [@a href="cic:/matita/arithmetics/nat/le_plus.def(7)"le_plus/a // + |@a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"le_S_S/a @Hind + [@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a // + |#x #memx cut (x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a m) + [@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @Hmem @(a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx)] #Hcut + cases(a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … Hcut) // #eqxm @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a + @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a ? eqxm) @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a + @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a @(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? 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)) +img class="anchor" src="icons/tick.png" id="eq_length_to_mem"lemma eq_length_to_mem : ∀n,l. |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/a a href="cic:/matita/arithmetics/nat/nat.con(0,2,0)"S/a n → a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → + (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"≤/a n) → n a title="list membership" href="cic:/fakeuri.def(1)"∈/a l. +#n #l #H1 #H2 #H3 cases (a href="cic:/matita/arithmetics/pidgeon_hole/decidable_mem_nat.def(6)"decidable_mem_nat/a n l) // +#H4 @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a (|la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'greater than'" href="cic:/fakeuri.def(1)">/a 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) #_ 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) % + [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a Hfilter % + |@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a @H1 + |#x #memx cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (H2 x (a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx))) #H3 + [@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H3 + |@a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a (ma title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a //] @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a + @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? memx) % ] - |@le_S_S_to_le @leim + |@a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @leim ] - |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //] + |#eqi @a href="cic:/matita/arithmetics/pidgeon_hole/eq_length_to_mem.def(10)"eq_length_to_mem/a >eqi [@H |@H1 |#x #Hx @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a >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). +img class="anchor" src="icons/tick.png" id="lt_length_to_not_mem"lemma lt_length_to_not_mem: ∀n,l. a href="cic:/matita/basics/lists/search/unique.fix(0,1,2)"unique/a ? l → (∀x. x a title="list membership" href="cic:/fakeuri.def(1)"∈/a l → x a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n) → |la title="list length" href="cic:/fakeuri.def(1)"|/a a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n → +a title="exists" href="cic:/fakeuri.def(1)"∃/ai. i a title="natural 'less than'" href="cic:/fakeuri.def(1)"</a n a title="logical and" href="cic:/fakeuri.def(1)"∧/a a title="logical not" href="cic:/fakeuri.def(1)"¬/a (i a title="list membership" href="cic:/fakeuri.def(1)"∈/a l). #n elim n - [#l #_ #_ #H @False_ind /2/ - |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni) + [#l #_ #_ #H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a /span class="autotactic"2span class="autotrace" trace a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a/span/span/ + |#m #Hind #l #Huni #Hmem #Hlen cases (a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"filter_eqb/a 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 (a href="cic:/matita/basics/lists/search/filter.def(2)"filter/a ? (λx. a title="boolean not" href="cic:/fakeuri.def(1)"¬/a(a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m x)) l) ? ? ?) + [#i * #ltim #memi %{i} % [@a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"le_S/a // ] + @(a href="cic:/matita/basics/logic/not_to_not.def(3)"not_to_not/a … memi) @a href="cic:/matita/basics/lists/search/mem_filter_l.def(4)"mem_filter_l/a @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >a href="cic:/matita/basics/bool/notb_notb.def(2)"notb_notb/a + @a href="cic:/matita/arithmetics/nat/not_eq_to_eqb_false.def(6)"not_eq_to_eqb_false/a @a href="cic:/matita/basics/logic/sym_not_eq.def(4)"sym_not_eq/a @a href="cic:/matita/arithmetics/nat/lt_to_not_eq.def(7)"lt_to_not_eq/a // + |@a href="cic:/matita/basics/lists/search/unique_filter.def(4)"unique_filter/a // + |#x #memx cases (a href="cic:/matita/arithmetics/nat/le_to_or_lt_eq.def(5)"le_to_or_lt_eq/a … (Hmem x ?)) + [#H @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H + |#H @a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"False_ind/a @(a href="cic:/matita/basics/logic/absurd.def(2)"absurd/a (ma title="leibnitz's equality" href="cic:/fakeuri.def(1)"=/ax)) [@a href="cic:/matita/arithmetics/nat/injective_S.def(4)"injective_S/a //] @a href="cic:/matita/arithmetics/nat/eqb_false_to_not_eq.def(6)"eqb_false_to_not_eq/a + @a href="cic:/matita/basics/bool/injective_notb.def(4)"injective_notb/a >(a href="cic:/matita/basics/lists/search/mem_filter_true.def(4)"mem_filter_true/a ???? memx) % + |@(a href="cic:/matita/basics/lists/search/mem_filter.def(3)"mem_filter/a … memx) ] - |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H - @le_S_S_to_le @H + |<(a href="cic:/matita/basics/lists/search/filter_length2.def(5)"filter_length2/a … (a href="cic:/matita/arithmetics/nat/eqb.fix(0,0,1)"eqb/a m)) in Hlen; >Hfilter #H + @a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"le_S_S_to_le/a @H ] ] ]