weblib/arithmetics/pidgeon_hole.ma

   1
   2 include "arithmetics/bounded_quantifiers.ma".
   3 include "basics/list.ma".
   4
   5 (* A bit of combinatorics *)
   6 interpretation "list membership" 'mem a l = (mem ? a l).
   7
   8 lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
   9 #n #l elim l
  10   [%2 % @False_ind |#a #tl #Htl @decidable_or //]
  11 qed.
  12
  13 lemma length_unique_le: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| ≤ n.
  14 #n elim n
  15   [* // #a #tl #_ #H @False_ind @(absurd (a < 0))
  16     [@H %1 % | @le_to_not_lt //]
  17   |#m #Hind #l #Huni #Hmem <(filter_length2 ? (eqb m) l)
  18    lapply (length_filter_eqb … m l Huni) #Hle
  19    @(transitive_le ? (1+|filter ? (λx.¬ eqb m x) l|))
  20     [@le_plus //
  21     |@le_S_S @Hind
  22       [@unique_filter //
  23       |#x #memx cut (x ≤ m)
  24         [@le_S_S_to_le @Hmem @(mem_filter … memx)] #Hcut
  25        cases(le_to_or_lt_eq … Hcut) // #eqxm @False_ind
  26        @(absurd ? eqxm) @sym_not_eq @eqb_false_to_not_eq
  27        @injective_notb @(mem_filter_true ???? memx)
  28       ]
  29     ]
  30   ]
  31 qed.
  32
  33 lemma eq_length_to_mem : ∀n,l. |l| = S n → unique ? l →
  34   (∀x. x ∈ l → x ≤ n) → n ∈ l.
  35 #n #l #H1 #H2 #H3 cases (decidable_mem_nat n l) //
  36 #H4 @False_ind @(absurd (|l| > n))
  37   [>H1 //
  38   |@le_to_not_lt @length_unique_le //
  39    #x #memx cases(le_to_or_lt_eq … (H3 x memx)) //
  40    #Heq @not_le_to_lt @(not_to_not … H4) #_ <Heq //
  41   ]
  42 qed.
  43
  44 lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  →
  45   (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
  46 #n elim n
  47   [#l #_ #_ #_ #i #lti0 @False_ind @(absurd ? lti0 (not_le_Sn_O ?))
  48   |#m #Hind #l #H #H1 #H2 #i #lei cases (le_to_or_lt_eq … lei)
  49     [#leim @(mem_filter… (λi.¬(eqb m i)))
  50      cases (filter_eqb m … H1)
  51       [2: * #H @False_ind @(absurd ?? H) @eq_length_to_mem //
  52        #x #memx @le_S_S_to_le @H2 //]
  53       * #memm #Hfilter @Hind
  54         [@injective_S <H <(filter_length2 ? (eqb m) l) >Hfilter %
  55         |@unique_filter @H1
  56         |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
  57           [@le_S_S_to_le @H3
  58           |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
  59            @injective_notb >(mem_filter_true ???? memx) %
  60           ]
  61       |@le_S_S_to_le @leim
  62       ]
  63     |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
  64     ]
  65   ]
  66 qed.
  67
  68 lemma lt_length_to_not_mem: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| < n →
  69 ∃i. i < n ∧ ¬ (i ∈ l).
  70 #n elim n
  71   [#l #_ #_ #H @False_ind /2/
  72   |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
  73     [2: * #H #_ %{m} % //
  74     |* #memm #Hfilter cases (Hind (filter ? (λx. ¬(eqb m x)) l) ? ? ?)
  75       [#i * #ltim #memi %{i} % [@le_S // ]
  76        @(not_to_not … memi) @mem_filter_l @injective_notb >notb_notb
  77        @not_eq_to_eqb_false @sym_not_eq @lt_to_not_eq //
  78       |@unique_filter //
  79       |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
  80         [#H @le_S_S_to_le @H
  81         |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
  82          @injective_notb >(mem_filter_true ???? memx) %
  83         |@(mem_filter … memx)
  84         ]
  85       |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
  86        @le_S_S_to_le @H
  87       ]
  88     ]
  89   ]
  90 qed.