Another attempt at an elegant pigeon-hole principle proof in Coq.

pigeons.v

Require Import Utf8 Nat PeanoNat Lia Compare_dec.
Import Nat.

Section Pigeons.

Variable f : nat -> nat.
Variable Σ N : nat.
Hypothesis bound : ∀i, i < N -> f i < Σ.
Hypothesis overflow : Σ < N.

Definition duplicate y n := ∃i, i < n /\ f i = y.

Inductive distinct : nat -> Prop :=
  | distinct_O : distinct 0
  | distinct_S n : distinct n -> ¬(duplicate (f n) n) -> distinct (S n).

Definition first_duplicate n := distinct n /\ duplicate (f n) n.

Theorem distinct_spec n i j :
  distinct n -> i < n -> j < n -> f i ≠ f j.
Proof.
Abort.

Lemma duplicate_dec y n :
  {duplicate y n} + {¬duplicate y n}.
Proof.
induction n. right; now intros [i Hi].
destruct IHn as [IH|IH]. left; destruct IH as [i Hi]; exists i; lia.
destruct (eq_dec (f n) y). left; exists n; lia. right; intros [i [H1i H2i]].
apply Lt.lt_n_Sm_le, le_lt_eq_dec in H1i as [H1i|H1i].
apply IH; now exists i. now subst.
Qed.

Lemma distinct_dec n :
  {distinct n} + {¬distinct n}.
Proof.
induction n. left; apply distinct_O.
destruct IHn as [IH|IH]. destruct (duplicate_dec (f n) n).
right; intros H; inversion H; now subst. left; now apply distinct_S.
right; intros H; now inversion H.
Qed.

Theorem not_distinct :
  ¬distinct N.
Proof.
induction N. easy.
Admitted.

Theorem strong_PHP :
  ∃n, n < N /\ first_duplicate n.
Proof.
assert(H := not_distinct); clear bound overflow.
induction N. exfalso; apply H, distinct_O.
Admitted.

End Pigeons.