matita/matita/lib/arithmetics/pidgeon_hole.ma

   1 (*
   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.
   5     ||I||
   6     ||T||
   7     ||A||  This file is distributed under the terms of the
   8     \   /  GNU General Public License Version 2
   9      \ /
  10       V_______________________________________________________________ *)
  11
  12 include "arithmetics/bounded_quantifiers.ma".
  13 include "basics/lists/list.ma".
  14
  15 (* A bit of combinatorics *)
  16 interpretation "list membership" 'mem a l = (mem ? a l).
  17
  18 lemma decidable_mem_nat: ∀n:nat.∀l. decidable (n ∈ l).
  19 #n #l elim l
  20   [%2 % @False_ind |#a #tl #Htl @decidable_or //]
  21 qed.
  22
  23 lemma length_unique_le: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| ≤ n.
  24 #n elim 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|))
  30     [@le_plus //
  31     |@le_S_S @Hind
  32       [@unique_filter //
  33       |#x #memx cut (x ≤ m)
  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)
  38       ]
  39     ]
  40   ]
  41 qed.
  42
  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))
  47   [>H1 //
  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 //
  51   ]
  52 qed.
  53
  54 lemma eq_length_to_mem_all: ∀n,l. |l| = n → unique ? l  →
  55   (∀x. x ∈ l → x < n) → ∀i. i < n → i ∈ l.
  56 #n elim n
  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 %
  65         |@unique_filter @H1
  66         |#x #memx cases (le_to_or_lt_eq … (H2 x (mem_filter … memx))) #H3
  67           [@le_S_S_to_le @H3
  68           |@False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
  69            @injective_notb >(mem_filter_true ???? memx) %
  70           ]
  71       |@le_S_S_to_le @leim
  72       ]
  73     |#eqi @eq_length_to_mem >eqi [@H |@H1 |#x #Hx @le_S_S_to_le >eqi @H2 //]
  74     ]
  75   ]
  76 qed.
  77
  78 lemma lt_length_to_not_mem: ∀n,l. unique ? l  → (∀x. x ∈ l → x < n) → |l| < n →
  79 ∃i. i < n ∧ ¬ (i ∈ l).
  80 #n elim n
  81   [#l #_ #_ #H @False_ind /2/
  82   |#m #Hind #l #Huni #Hmem #Hlen cases (filter_eqb m … Huni)
  83     [2: * #H #_ %{m} % //
  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 //
  88       |@unique_filter //
  89       |#x #memx cases (le_to_or_lt_eq … (Hmem x ?))
  90         [#H @le_S_S_to_le @H
  91         |#H @False_ind @(absurd (m=x)) [@injective_S //] @eqb_false_to_not_eq
  92          @injective_notb >(mem_filter_true ???? memx) %
  93         |@(mem_filter … memx)
  94         ]
  95       |<(filter_length2 … (eqb m)) in Hlen; >Hfilter #H
  96        @le_S_S_to_le @H
  97       ]
  98     ]
  99   ]
 100 qed.