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