Variation of the Pigeonhole Principle

In math, the pigeonhole principle states that if `n` items are put in `m` containers and `n` is greater than `m` then at least two items must go in the same container. This principle is formalized in “Software Foundations” as follows

```Theorem pigeonhole_principle : forall {X:Type} (l1 l2:list X),
excluded_middle ->
(forall x, In x l1 -> In x l2) ->
length l2 < length l1 ->
repeats l1.
```

Before unpacking the definition I’ll explain how it maps to the usual pigeonhole principle.

If you think of `l2` as a set of labels for boxes and `l1` as the items labeled by the containers from `l2` then the correspondence becomes somewhat more clear. For example, if `l2 = [x; y]` then the length and element inclusion restriction forces `l1` to be either `[x; x; y]` or `[x; y; y]`. You can imagine other cases as well. We could include elements in `l2` that are not used in `l1` but that just increases the length of `l1` even more because if `l2` had an extra element like `z` that was never used in `l1` then we’d need to repeat `x` and `y` even more times to satisfy the constraints of the theorem.

We could also repeat the elements of `l2` but that’s like taking one big box with a single label and making it two smaller boxes with the same label. It doesn’t change anything about the theorem because if you put one element in a box labeled `x` and another one in another box labeled `x` then we’ve again technically put two elements in a box with the same label.

Hopefully that explains the correspondence so let’s move on to the definitions used.

There are a few inductive definitions in that statement but they’re easy to explain. `In x l` is evidence that the element `x` appears in the list `l`. So the implication `forall x, In x l1 -> In x l2` is really a statement about subset inclusion if we pretend the lists are sets (we’re not worrying about multiplicities for the time being). The other definition is `repeats l` and it provides evidence that `l` contains at least one element that is repeated, i.e. there is an element `x` that has multiplicity greater than 1.

I don’t actually like how the principle is stated because I think it confounds several concepts by overloading the meaning of lists. This is somewhat unavoidable because it is one of the exercises in the first few chapters but there are a few other concepts in that chapter that I think could have been used to state an equivalent form of the principle that would be easier to think about (or at least I think would be easier to prove). So let’s actually do that and reformulate the theorem using some other concepts from that chapter.

The first simplification/strengthening we can perform is to notice that the elements in `l2` that are not in `l1` are not actually relevant for the statement of the theorem. The reasoning goes as follows: split `l2` into two disjoint parts (`l2'`, `l2''`), let the first part consist of all the elements that are in `l1` and the second part consist of the elements that are not in `l1`. Now it is clear that removing all the elements in `l2''` does not affect the statement of the theorem because it doesn’t participate in any part of it and only increases the length of the overall list so we can safely remove it without affecting any of the assumptions. The assumption about lengths is preserved and the assumption about membership is also preserved. So the first simplification we can perform without losing any generality is by turning the subset relation into set equality by converting the implication into a bi-implication

```Theorem pigeonhole_principle : forall {X:Type} (l1 l2:list X),
excluded_middle ->
(forall x, In x l1 <-> In x l2) ->
length l2 < length l1 ->
repeats l1.
```

Already we are working with stronger assumptions and so proving this should be simpler than proving the weaker statement we had before. There are two more simplifications we can make without losing generality. Notice that if `l1` and `l2` contain the same elements as sets then that means there must exist another list `l2'` such that `l1` is the merged list of `l2` and `l2'` and as sets `l2'` is a subset of `l2`.

The reasoning for the equivalence is again pretty simple. If this was not the case then `l1` would contain an element that did not come from `l2` which contradicts one of our assumptions. So the final form of the equivalent but strengthened pigeonhole principle looks like this

```Theorem pigeonhole_principle : forall {X:Type} (l1 l2:list X),
(forall x, In x l1 <-> In x l2) ->
(exists l2', In x l2' -> In x l2 /\ merge l2 l2' l1) ->
length l2 < length l1 ->
repeats l1.
```

It turns out we don’t need the principle of the excluded middle either. Now proving this reformulated theorem is actually not trivial but I thought it was much simpler than how the theorem was initially stated. If you want to prove the theorem then here are some lemmas that you will need along the way

```Lemma merge_equality : forall {X:Type} (l1 l2:list X),
merge l1 [ ] l2 -> l1 = l2.

(* Merging preserves all the elements on the left *)
Lemma merge_includes_left : forall {X:Type} l1 l2 l,
merge l1 l2 l -> forall (x:X), In x l1 -> In x l.

(* Merging preserves all elements on the right *)
Theorem merge_includes_right : forall {X:Type} l1 l2 l,
merge l1 l2 l -> forall (x:X), In x l2 -> In x l.

(* If we have repeats then we can add anything under the head *)
Lemma repeats_under_head : forall {X:Type} (l:list X) y,
repeats (y :: l) -> forall x, repeats (y :: x :: l).

(* Repeats are not changed when we swap elements *)
Theorem repeats_swap : forall {X:Type} (l:list X) x y,
repeats (x :: y :: l) -> repeats (y :: x :: l).

(* Common elements force repeats in the merged list *)
Lemma merge_repeats : forall {X:Type} (l1 l2 l3:list X),
merge l1 l2 l3 ->
forall y, In y l1 -> In y l2 -> repeats l3.
```