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.

  • $\begingroup$ Could you state exactly which pigeonhole principle you mean? There are several principles that could go by that name. $\endgroup$ – Carl Mummert Aug 27 '14 at 10:34
  • $\begingroup$ Yep, sorry. I added my definition (failed to TeXify it, but hope it is clear as it is). $\endgroup$ – max taldykin Aug 27 '14 at 10:50
  • $\begingroup$ 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... $\endgroup$ – 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).

  • $\begingroup$ 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. $\endgroup$ – max taldykin Aug 27 '14 at 11:30
  • $\begingroup$ 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)$. $\endgroup$ – Carl Mummert Aug 27 '14 at 12:01
  • $\begingroup$ (1) should be $0 \not = S(x)$ $\endgroup$ – Carl Mummert Aug 27 '14 at 12:30
  • $\begingroup$ 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 $\endgroup$ – Carl Mummert Aug 27 '14 at 19:41
  • $\begingroup$ 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. $\endgroup$ – max taldykin Aug 27 '14 at 19:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.