# Constructive proof of pigeonhole principle

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.

• Could you state exactly which pigeonhole principle you mean? There are several principles that could go by that name. – Carl Mummert Aug 27 '14 at 10:34
• Yep, sorry. I added my definition (failed to TeXify it, but hope it is clear as it is). – max taldykin Aug 27 '14 at 10:50
• Another version, actually a generalization, of the pigeonhole principle is "the average of a finite bag (multiset) of numbers $\leq$ its maximum". That may or may not help... – Marnix Klooster Aug 27 '14 at 20:24

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).

• Thank you very much. The proof is really easy and straightforward, I even thought about applying inductive hypothesis to some new function but then got distracted and switched to googling for hints. – max taldykin Aug 27 '14 at 11:30
• The facts about decidability follow from induction and the axioms (1) $x \not = S(x)$; (2) $x = 0 \lor (\exists y)[x = S(y)]$; (3) $x = y \leftrightarrow S(x) = S(y)$. – Carl Mummert Aug 27 '14 at 12:01
• (1) should be $0 \not = S(x)$ – Carl Mummert Aug 27 '14 at 12:30
• Thanks for accepting - I assume that means you were able to formalize the proof? I have been thinking for a while about trying to learn Coq. Would you be willing to share the formalized proof with me? If so, could you email me at the address listed in my profile? I would deeply appreciate it. @max taldykin – Carl Mummert Aug 27 '14 at 19:41
• I succeeded formalizing everything except $(\forall f)(\forall k)(\forall m)[(\exists i < m)[f(i) = k] \lor \lnot (\exists i < m)[f(i) = k]]$. It is easy to prove it by classic axiom but I still trying to understand how to prove it by induction. – max taldykin Aug 27 '14 at 19:54