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.