Reverse pigeonhole principle?

Stream: new members

[aron]

How can I prove this theorem:

theorem List.rev_pigeonhole_principle {l : List Nat}
  (nodup : l.Nodup)
  (heach : ∀ item ∈ l, item < n)
  (hitemlen : item < n)
  (hitemin : item ∉ l)
  : l.length < n := by sorry

it's sort of like a reverse pigeonhole principle? that if I have a list of unduplicated Nats and I know they're all less than some n, and I have another value item that is also less than n, that I know the list must not contain all possible values it could contain – and it's only if the list is "full" that its length would equal n.

sorry I am not a mathematician I have probably expressed this in a very awkward way :grimacing: but hopefully it's clear what I'm trying to do

[aron]

I can't quite work out how to do this because this problem doesn't lend itself to a nice simple induction. I think I'm going to have to induct over n and then remove n' from the list and then prove the same lemmas about the smaller list recursively?

[Kenny Lau]

the Nodup assumption allows you to transfer to Finset Nat, where the rest of the assumptions show that your finset is in fact a proper subset of Finset.range n, so its size must be strictly less than (Finset.range n).card, which is n.

[Kenny Lau]

in summary: don't use induction, use existing theorems

[aron]

could you give me an example how I'd transfer into Finset Nat? and how I'd show that the size is less than n?

sorry mathlib is still v intimidating to me :sweat_smile:

[Robin Arnez]

import Mathlib.Data.Finset.Card

theorem List.rev_pigeonhole_principle {l : List Nat}
    (nodup : l.Nodup)
    (heach : ∀ item ∈ l, item < n)
    (hitemlen : item < n)
    (hitemin : item ∉ l)
    : l.length < n := by
  let s : Finset Nat := Finset.mk l nodup
  have hs1 (x) : x ∈ l ↔ x ∈ s := Iff.rfl
  have hs2 : l.length = s.card := rfl
  simp only [hs1, implies_true, hs2] at *
  have : s ⊂ Finset.range n := by
    constructor
    · intro a ha
      simp_all
    · intro hs
      exact hitemin (hs (by simpa using hitemlen))
  simpa using Finset.card_lt_card this

[aron]

ahh thank you @Robin Arnez! I attempted to do what @Kenny Lau suggested on my own but I was getting nowhere. Your solution is really nice and elegant :ok: