Constructive proof of pigeonhole principle

Question

I'm trying to prove Pigeonhole principle with Coq proof assistant.

Here is how I defined it:

Theorem pigeonhole
    :  forall m n : nat, m < n
    -> forall f : nat -> nat, (forall i, f i < m)
    -> exists i, i < n
    -> exists j, j < i /\ f i = f j.

After spending some time on attempts to prove it by induction I found this discussion (https://math.stackexchange.com/a/228604/15013) that suggest it is impossible.

Is it possible (and how) to prove Pigeonhole principle without using contradiction? Using principle of explosion is fine, but excluded middle is not accepted.

Answer 1

Here is a proof that would go through in Bishop's system and similar systems where equality of natural numbers is decidable.

We only need to prove the case $n = m+ 1$, because this implies the general case $n > m$. So we will work with functions from $n = \{0, 1, \ldots, n-1\}$ to $m = n - 1 = \{0, \ldots, m-1\}$.

The proof will be by induction on $n$. The case $n = 1$ is impossible (there is no function from $1$ to $0$) so the base case is $n = 2$. In this case $f(0) = f(1) = 0$ so we're done.

For the inductive case, assume $f$ is a function from $n = m+1$ to $m$ where $m > 1$. We don't have full excluded middle constructively, but we do have constructively that either there is some $i < m$ with $f(i) = f(m)$, or there is not. Speaking formally, we can prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$ by induction on $m$, with $f$ and $k$ as parameters.

So, working constructively, we can split into those two cases: either there is some $i < m$ with $f(i) = f(m)$, or there is not. In the first case, we are done already.

In the second case, we make a new function $g$ from $m$ to $m - 1$ so that $g(a) = f(a)$ whenever $f(a) < f(m)$, and $g(a) = f(a) -1$ when $f(a) > f(m)$. This is a sound definition because we have assumed $f(a) \not = f(m)$ for all $a < m$. Now we can apply the inductive hypothesis to $g$ to find $i,j < m$ with $g(i) = g(j)$; then $f(i) = f(j)$ also and we are done.

---

Here is a guide to prove $$(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$$

The first step is to prove $(\forall x)(\forall y)[x = y \lor x \not = y]$. This is proved by induction on $x$ with $y$ as a parameter.

• For the base case, we prove $(\forall y)[y = 0 \lor y \not = 0]$ from the axioms

  1) $0 \not = S(z)$

  2) $ y = 0 \lor ( \exists z)[y = S(z)]$.

• For the inductive case, we use the additional axiom $x = y \leftrightarrow S(x) = S(y)$.

Once we have the first step, then we can prove the desired formula by induction on $m$ with $k$ and $f$ as parameters.

• The base case is $\lnot (\exists i < 0)[f(i) = k]$.

• For the inductive case, we use the additional axiom $x = S(y) \to z < x \to z < y \lor z = y$ (or we derive this separately).