Pigeonhole.lean — FrcCore

1import FrcCore.Nat23/-!4# FrcCore.Pigeonhole — a list of `n` distinct numbers in `[1, n]` is all of `[1, n]`56The counting fact behind "the drive generates": its `p − 1` powers are distinct nonzero residues, and there7are only `p − 1` of those. Lists of naturals with their own membership, no-duplicates and erase (Lean's8`List` lemmas carry `propext`); everything by induction. No axioms.9-/1011namespace FRC12namespace Pigeonhole1314/-- Membership, by recursion (decidable). -/15def mem (v : Nat) : List Nat → Prop16  | [] => False17  | a :: l => v = a ∨ mem v l1819def decMem (v : Nat) : (l : List Nat) → Decidable (mem v l)20  | [] => isFalse id21  | a :: l => match Nat.decEq v a, decMem v l with22    | isTrue h, _ => isTrue (Or.inl h)23    | isFalse _, isTrue h' => isTrue (Or.inr h')24    | isFalse h, isFalse h' => isFalse (fun e => match e with | Or.inl e => h e | Or.inr e => h' e)2526instance (v : Nat) (l : List Nat) : Decidable (mem v l) := decMem v l2728/-- No duplicates, by recursion. -/29def NoDup : List Nat → Prop30  | [] => True31  | a :: l => ¬ mem a l ∧ NoDup l3233/-- Remove the first occurrence of `v`. -/34def erase (v : Nat) : List Nat → List Nat35  | [] => []36  | a :: l => if a = v then l else a :: erase v l3738theorem length_erase_of_mem {v : Nat} : ∀ {l : List Nat}, mem v l → (erase v l).length + 1 = l.length39  | [], h => absurd h id40  | a :: l, h => by41    show (if a = v then l else a :: erase v l).length + 1 = l.length + 142    exact match Nat.decEq a v with43      | isTrue e => by rw [ite_eq_left e]44      | isFalse e => by45          rw [ite_eq_right e]46          show (erase v l).length + 1 + 1 = l.length + 147          have hm : mem v l := match h with48            | Or.inl h' => absurd h'.symm e49            | Or.inr h' => h'50          rw [length_erase_of_mem hm]5152theorem mem_of_mem_erase {w v : Nat} : ∀ {l : List Nat}, mem w (erase v l) → mem w l53  | [], h => absurd h id54  | a :: l, h => by55    show w = a ∨ mem w l56    exact match Nat.decEq a v with57      | isTrue e => by58          rw [show erase v (a :: l) = l from ite_eq_left e] at h59          exact Or.inr h60      | isFalse e => by61          rw [show erase v (a :: l) = a :: erase v l from ite_eq_right e] at h62          exact match h with63            | Or.inl h' => Or.inl h'64            | Or.inr h' => Or.inr (mem_of_mem_erase h')6566theorem mem_erase_of_ne {w v : Nat} (hwv : w ≠ v) : ∀ {l : List Nat}, mem w l → mem w (erase v l)67  | [], h => absurd h id68  | a :: l, h => by69    exact match Nat.decEq a v with70      | isTrue e => by71          rw [show erase v (a :: l) = l from ite_eq_left e]72          exact match h with73            | Or.inl h' => absurd (h'.trans e) hwv74            | Or.inr h' => h'75      | isFalse e => by76          rw [show erase v (a :: l) = a :: erase v l from ite_eq_right e]77          exact match h with78            | Or.inl h' => Or.inl h'79            | Or.inr h' => Or.inr (mem_erase_of_ne hwv h')8081theorem nodup_erase (v : Nat) : ∀ {l : List Nat}, NoDup l → NoDup (erase v l)82  | [], _ => trivial83  | a :: l, ⟨ha, hl⟩ => by84    exact match Nat.decEq a v with85      | isTrue e => by rw [show erase v (a :: l) = l from ite_eq_left e]; exact hl86      | isFalse e => by87          rw [show erase v (a :: l) = a :: erase v l from ite_eq_right e]88          exact ⟨fun h => ha (mem_of_mem_erase h), nodup_erase v hl⟩8990theorem not_mem_erase_self (v : Nat) : ∀ {l : List Nat}, NoDup l → ¬ mem v (erase v l)91  | [], _, h => h92  | a :: l, ⟨ha, hl⟩, h => by93    exact match Nat.decEq a v with94      | isTrue e => by95          rw [show erase v (a :: l) = l from ite_eq_left e] at h96          exact ha (e ▸ h)97      | isFalse e => by98          rw [show erase v (a :: l) = a :: erase v l from ite_eq_right e] at h99          exact match h with100            | Or.inl h' => e h'.symm101            | Or.inr h' => not_mem_erase_self v hl h'102103/-- The bound: a list of distinct numbers in `[1, n]` has at most `n` entries. -/104theorem length_le_of_nodup : ∀ (n : Nat) (l : List Nat), NoDup l → (∀ e, mem e l → 1 ≤ e ∧ e ≤ n) →105    l.length ≤ n106  | 0, [], _, _ => Nat.le_refl 0107  | 0, a :: l, _, hb => absurd (hb a (Or.inl rfl)) (fun ⟨h1, h0⟩ => Nat.lt_irrefl 0 (Nat.lt_of_lt_of_le h1 h0))108  | n + 1, l, hnd, hb =>109    match (inferInstance : Decidable (mem (n + 1) l)) with110    | isTrue hm =>111      have h1 : (erase (n + 1) l).length ≤ n :=112        length_le_of_nodup n (erase (n + 1) l) (nodup_erase _ hnd) (fun e he =>113          have hb' := hb e (mem_of_mem_erase he)114          ⟨hb'.1, match Nat.lt_or_ge e (n + 1) with115            | Or.inl hlt => Nat.le_of_lt_succ hlt116            | Or.inr hge =>117              have : e = n + 1 := Nat.le_antisymm hb'.2 hge118              absurd (this ▸ he) (not_mem_erase_self (n + 1) hnd)⟩)119      by rw [← length_erase_of_mem hm]; exact Nat.succ_le_succ h1120    | isFalse hm =>121      Nat.le_succ_of_le (length_le_of_nodup n l hnd (fun e he =>122        have hb' := hb e he123        ⟨hb'.1, match Nat.lt_or_ge e (n + 1) with124          | Or.inl hlt => Nat.le_of_lt_succ hlt125          | Or.inr hge => absurd he ((Nat.le_antisymm hb'.2 hge) ▸ hm)⟩))126127/-- The pigeonhole: `n` distinct numbers in `[1, n]` are all of them. -/128theorem mem_of_nodup_of_length (n : Nat) (l : List Nat) (hnd : NoDup l) (hb : ∀ e, mem e l → 1 ≤ e ∧ e ≤ n)129    (hlen : l.length = n) (v : Nat) (hv1 : 1 ≤ v) (hvn : v ≤ n) : mem v l :=130  match decMem v l with131  | isTrue h => h132  | isFalse h =>133    have hnd' : NoDup (v :: l) := ⟨h, hnd⟩134    have hb' : ∀ e, mem e (v :: l) → 1 ≤ e ∧ e ≤ n := fun e he => match he with135      | Or.inl e' => e' ▸ ⟨hv1, hvn⟩136      | Or.inr e' => hb e e'137    have := length_le_of_nodup n (v :: l) hnd' hb'138    absurd (hlen ▸ this : n + 1 ≤ n) (Nat.not_succ_le_self n)139140/-- The same with the range `[0, n)`: a list of distinct numbers below `n` has at most `n` entries. -/141theorem length_le_of_nodup_lt : ∀ (n : Nat) (l : List Nat), NoDup l → (∀ e, mem e l → e < n) → l.length ≤ n142  | 0, [], _, _ => Nat.le_refl 0143  | 0, a :: l, _, hb => absurd (hb a (Or.inl rfl)) (Nat.not_lt_zero a)144  | n + 1, l, hnd, hb =>145    match decMem n l with146    | isTrue hm =>147      have h1 : (erase n l).length ≤ n :=148        length_le_of_nodup_lt n (erase n l) (nodup_erase _ hnd) (fun e he =>149          match Nat.lt_or_ge e n with150          | Or.inl hlt => hlt151          | Or.inr hge =>152            have : e = n := Nat.le_antisymm (Nat.le_of_lt_succ (hb e (mem_of_mem_erase he))) hge153            absurd (this ▸ he) (not_mem_erase_self n hnd))154      by rw [← length_erase_of_mem hm]; exact Nat.succ_le_succ h1155    | isFalse hm =>156      Nat.le_succ_of_le (length_le_of_nodup_lt n l hnd (fun e he =>157        match Nat.lt_or_ge e n with158        | Or.inl hlt => hlt159        | Or.inr hge => absurd he ((Nat.le_antisymm (Nat.le_of_lt_succ (hb e he)) hge) ▸ hm)))160161/-- `n` distinct numbers below `n` are all of them. -/162theorem mem_of_nodup_of_length_lt (n : Nat) (l : List Nat) (hnd : NoDup l) (hb : ∀ e, mem e l → e < n)163    (hlen : l.length = n) (v : Nat) (hv : v < n) : mem v l :=164  match decMem v l with165  | isTrue h => h166  | isFalse h =>167    have hb' : ∀ e, mem e (v :: l) → e < n := fun e he => match he with168      | Or.inl e' => e' ▸ hv169      | Or.inr e' => hb e e'170    have := length_le_of_nodup_lt n (v :: l) ⟨h, hnd⟩ hb'171    absurd (hlen ▸ this : n + 1 ≤ n) (Nat.not_succ_le_self n)172173end Pigeonhole174end FRC175