6

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.

Community
  • 1
max taldykin
  • 267

1 Answers1

4

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

Carl Mummert
  • 81,604
  • 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
  • I added some thoughts on this. – Carl Mummert Aug 27 '14 at 20:01
  • Sorry for delay. I just completed the proof, you can see it here. It is still hairy and badly structured. I'll try to simplify it and then will post it here as a separate answer. Thanks again for the detailed explanation. – max taldykin Sep 01 '14 at 22:11