This section presents some elementary facts from the theory of cardinality and discusses a proof of the familiar pigeonhole principle.

Figure lists the definitions and lemmas used to prove the pigeonhole principle.

**Figure:** Proving the Pigeonhole Principle

` lemma_wf_1` is used to prove
well-formedness conditions that arise in the other lemmas. We use the lemma
` lemma_arith`
when we want to do a case analysis on an integer equality. ` lemma_hole`
finds for some ` f` and some ` y` in the codomain of ` f` an ` x`
in the domain of ` f`
for which ` f(x)=y` (or indicates if no such ` x` can be found).
This lemma
can be considered as a computational procedure that will be useful
in the proof of the main lemma, ` lemma_1`. This lemma is a simplified
version of the theorem, with the domain of ` f`
only one element larger than the
range. The theorem ` pigeonhole_principle` follows in short order from
` lemma_1`.

Using the pigeonhole principle one can prove a more general form of the principle. Figure lists the definitions needed to state the theorem and the statement of the theorem.

**Figure:** The General Pigeonhole Principle

The proof of ` lemma_hole` is a straightforward induction on ` m`,
the size of the domain of ` f`. It is left as an exercise.

We consider in depth the proof of ` lemma_1`.
In the proof given below we elide hypotheses which appear
previously in order to condense the presentation. The system
performs no such action.
After introducing the quantifiers
we perform induction on the eliminated set type ` n`
(we need to get an integer,
` n1` below, to do induction on).
This induction is over the size of the domain and range together.

+----------------------------------------------------------+ |EDIT THM lemma_1 | |----------------------------------------------------------| |# top 1 2 | |1. n:P | |2. n1:int | |[3]. 0<n1 | |>> all f:({1..n1+1}->{1..n1}).some i:{1..n1+1}. | | some j:{1..n1+1}. (i<>j#f(i).=z.f(j)) | | | |BY elim 2 new ih,k | | | |1# {down case} | | | |2* 1...3. | | >> all f:({1..0+1}->{1..0}).some i:{1..0+1}. | | some j:{1..0+1}. (i<>j#f(i).=z.f(j)) | | | |3# 1...3. | | 4. k:int | | 5. 0<k | | 6. ih:all f:({1..k-1+1}->{1..k-1}).some i:{1..k-1+1}. | | some j:{1..k-1+1}.(i<>j#f(i).=z.f(j)) | | >> all f:({1..k+1}->{1..k}).some i:{1..k+1}. | | some j:{1..k+1}. (i<>j#f(i).=z.f(j)) | | | +----------------------------------------------------------+

The ``up'' case is the only interesting case. First we intro ` f`,
and then since we want to use the lemma ` lemma_hole`
a proper form of it is sequenced in and appears as hypothesis 9
below.
We use this lemma on ` f:{1..k}->{1..k}`.
We then do a case analysis on the lemma.

The left case is trivial. We have some ` x` such that ` f(x)=f(k+1)`,
and ` x` is in ` {1..k}`, so ` x<>k`; thus
we can intro ` x` for ` i` and ` k+1` for ` j`. Let us concentrate
on the more interesting right case.
Using our induction hypothesis requires a function
` f:{1..k}->{1..k-1}`; our function will possibly map a value of
the domain to ` k`. We thus
make a new function by taking the value of ` f` that would have mapped to
` k` to whatever ` k+1` maps to. Since by the hole lemma (hypothesis 10)
no ` f(x)` has the same value as ` f(k+1)`, our new function will just be
a permutation of the old function.

+------------------------------------------------------------+ |EDIT THM lemma_1 | -------------------------------------------------------------| |# top 1 2 3 1 2 2 2 | |1...6. | |7. f:({1..k+1}->{1..k}) | |8. all y:{1..k}. (some x:{1..k}.f(x).=z.y) | | |(all x:{1..k}.f(x)<>y) | |9. (some x:{1..k}.f(x).=z.f(k+1)) | | |(all x:{1..k}.f(x)<>f(k+1)) | |10. (all x:{1..k}.f(x)<>f(k+1)) | |>> some i:{1..k+1}.some j:{1..k+1}.(i<>j#f(i).=z.f(j)) | | | |BY elim 6 on \x.int_eq(f(x);k;f(k+1);f(x)) | | | |1# 1...10. | | >> \x.int_eq(f(x);k;f(k+1);f(x)) | | in ({1..k-1+1}->{1..k-1}) | | | |2# 1..10. | | 11. i:({1..k-1+1})#(j:({1..k-1+1})#((i<>j)# | | ((\x.int_eq(f(x);k;f(k+1);f(x)))(i) | | =(\x.int_eq(f(x);k;f(k+1);f(x)))(j) in int))) | | >> some i:{1..k+1}.some j:{1..k+1}.(i<>j#f(i).=z.f(j)) | | | +------------------------------------------------------------+

We can now unravel our induction hypothesis into hypotheses 12, 14, 16 and 17
below. We want to do a case analysis
on ` f(i)=k | f(i)=k` (hypothesis 18); we sequence this
fact (proven by ` lemma_arith`) in.
Consider the case where ` f(i)=k`.
Then we can prove ` f(k+1)=f(j)`
by reducing hypothesis 17 (note how we have to sequence in 20 and 21, and then
` f(k+1)=f(j)`, in order to reduce the hypothesis).

+----------------------------------------------------------+ |EDIT THM lemma_1 | |----------------------------------------------------------| |# top 1 2 3 1 2 2 2 2 1 1 1 2 1 2 2 | |1. n:P | |12. i:{1..k-1+1} | |14. j:{1..k-1+1} | |16. i<>j | |17. (\x.int_eq(f(x);k;f(k+1);f(x)))(i)= | (\x.int_eq(f(x);k;f(k+1);f(x)))(j) in int | |18. f(i).=z.k|~f(i).=z.k | |19. f(i).=z.k | |20. (\x.int_eq(f(x);k;f(k+1);f(x)))(i)=f(k+1) in int | |21. (\x.int_eq(f(x);k;f(k+1);f(x)))(j)=f(j) in int | |>> some i:{1..k+1}.some j:{1..k+1}.(i<>j#f(i).=z.f(j)) | | | |BY (*combine 17,20,21*) | | seq f(k+1)=f(j) in int | | | |1* 1...19. | | 20. (\x.int_eq(f(x);k;f(k+1);f(x)))(i)=f(k+1) in int | | 21. (\x.int_eq(f(x);k;f(k+1);f(x)))(j)=f(j) in int | | >> f(k+1)=f(j) in int | | | |2# 1...21. | | 22. f(k+1)=f(j) in int | | >> some i:{1..k+1}.some j:{1..k+1}.(i<>j#f(i).=z.f(j)) | | | +----------------------------------------------------------+

We can now prove our goal by letting ` i` be ` k+1`
and ` j` be ` j`. ` k+1<>j` follows
from hypothesis 14.

+-------------------------------------------------------+ |EDIT THM lemma_1 | |-------------------------------------------------------| |# top 1 2 3 1 2 2 2 2 1 1 1 2 1 2 2 2 2 2 | |1...13. | |14. j:{1..k-1+1} | |15..22. | |>> (k+1 <>j#f(k+1 ).=z.f(j)) | | | |BY intro | | .... | | | +-------------------------------------------------------+

This concludes this part of the proof.
We now consider the other case, i.e., ` f(i)=k`.
If ` f(j)=k` then
the conclusion follows by symmetry from above (note that
in the current system we still have to prove this; eventually
a smart symmetry tactic could do the job). Otherwise,
` f(j)=k`,
and we can reduce hypothesis 17 to ` f(i)=f(j)` as done previously
(see hypotheses 22 and 23 below). The conclusion then
follows from hypotheses 16 and 24.

+---------------------------------------------------+ |EDIT THM lemma_1 | |---------------------------------------------------| |* top 1 2 3 1 2 2 2 2 1 1 1 2 2 2 2 2 2 2 2 | |1...15. | |16. i<>j | |17. (\x.int_eq(f(x);k;f(k+1);f(x)))(i)= | | (\x.int_eq(f(x);k;f(k+1);f(x)))(j) in int | |18. f(i).=z.k|~f(i).=z.k | |19. ~f(i).=z.k | |20. f(j).=z.k|~f(j).=z.k | |21. ~f(j).=z.k | |22. (\x.int_eq(f(x);k;f(k+1);f(x)))(i)=f(i) in int | |23. (\x.int_eq(f(x);k;f(k+1);f(x)))(j)=f(j) in int | |24. f(i)=f(j) in int | |>> (i<>j#f(i).=z.f(j)) | | | |BY intro | | ... | | | +---------------------------------------------------+

This completes the proof of ` lemma_1`.
The proof of ` pigeonhole_principle` is straightforward and
is left as an exercise for the reader.

The evaluator, when applied to ` term_of (pigeonhole_principle)` on a
given
function ` f`, returns the ` i` and ` j`
such that ` f(i)=f(j)` and ` i<>j`.
Figure gives some examples of such evaluations performed by the evaluator.
The redex on the left of the ` -->` evaluates
to the contractum on the right of the ` -->`.

**Figure:** Using the Evaluator on the Pigeonhole Principle

Thu Sep 14 08:45:18 EDT 1995