weblib/arithmetics/pidgeon_hole.ma

   1
   2 include "arithmetics/bounded_quantifiers.ma".
   3 include "basics/lists/search.ma".
   4
   5 (* A bit of combinatorics *)
   6 interpretation "list membership" 'mem a l = (mem ? a l).
   7
   8 \ 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).
   9 #n #l elim l
  10   [%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 //]
  11 qed.
  12
  13 \ 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.
  14 #n elim n
  15   [* // #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))
  16     [@H %1 % | @\ 5a href="cic:/matita/arithmetics/nat/le_to_not_lt.def(8)"\ 6le_to_not_lt\ 5/a\ 6 //]
  17   |#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)
  18    lapply (\ 5a href="cic:/matita/basics/lists/search/length_filter_eqb.def(8)"\ 6length_filter_eqb\ 5/a\ 6 … m l Huni) #Hle
  19    @(\ 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))
  20     [@\ 5a href="cic:/matita/arithmetics/nat/le_plus.def(7)"\ 6le_plus\ 5/a\ 6 //
  21     |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S.def(2)"\ 6le_S_S\ 5/a\ 6 @Hind
  22       [@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
  23       |#x #memx cut (x \ 5a title="natural 'less or equal to'" href="cic:/fakeuri.def(1)"\ 6≤\ 5/a\ 6 m)
  24         [@\ 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
  25        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
  26        @(\ 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
  27        @\ 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)
  28       ]
  29     ]
  30   ]
  31 qed.
  32
  33 \ 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 →
  34   (∀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.
  35 #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) //
  36 #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))
  37   [>H1 //
  38   |@\ 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 //
  39    #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)) //
  40    #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 //
  41   ]
  42 qed.
  43
  44 \ 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  →
  45   (∀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.
  46 #n elim n
  47   [#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 ?))
  48   |#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)
  49     [#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)))
  50      cases (\ 5a href="cic:/matita/basics/lists/search/filter_eqb.def(7)"\ 6filter_eqb\ 5/a\ 6 m … H1)
  51       [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 //
  52        #x #memx @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H2 //]
  53       * #memm #Hfilter @Hind
  54         [@\ 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 %
  55         |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 @H1
  56         |#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
  57           [@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H3
  58           |@\ 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
  59            @\ 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) %
  60           ]
  61       |@\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @leim
  62       ]
  63     |#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 //]
  64     ]
  65   ]
  66 qed.
  67
  68 \ 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 →
  69 \ 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).
  70 #n elim n
  71   [#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/
  72   |#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)
  73     [2: * #H #_ %{m} % //
  74     |* #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) ? ? ?)
  75       [#i * #ltim #memi %{i} % [@\ 5a href="cic:/matita/arithmetics/nat/le.con(0,2,1)"\ 6le_S\ 5/a\ 6 // ]
  76        @(\ 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
  77        @\ 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 //
  78       |@\ 5a href="cic:/matita/basics/lists/search/unique_filter.def(4)"\ 6unique_filter\ 5/a\ 6 //
  79       |#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 ?))
  80         [#H @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
  81         |#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
  82          @\ 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) %
  83         |@(\ 5a href="cic:/matita/basics/lists/search/mem_filter.def(3)"\ 6mem_filter\ 5/a\ 6 … memx)
  84         ]
  85       |<(\ 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
  86        @\ 5a href="cic:/matita/arithmetics/nat/le_S_S_to_le.def(5)"\ 6le_S_S_to_le\ 5/a\ 6 @H
  87       ]
  88     ]
  89   ]
  90 qed.