Pigeonhole proof without decidable equality or excluded middle

Question

In Software Foundations IndProp.v one is asked to prove the pigeonhole principle, and one may use excluded middle, but it is mentioned that it is not strictly necessary. I've been trying to prove it without EM, but my brain seems to be wired classically.

Q: How would one prove the theorem without using excluded middle? How should one generally approach proofs for types without decidable equality, where one can't easily reason by cases?

I'd be very happy for a complete proof to look at, but please avoid posting it "in the clear", so as to not spoil the exercise in the Software Foundations course.

The definition uses two inductive predicates, In and repeats.

Require Import Lists.List.
Import ListNotations.

Section Pigeon.

  Variable (X:Type).
  Implicit Type (x:X).

  Fixpoint In x l : Prop :=                        (***    In       ***)
    match l with
    | nil => False
    | (x'::l') => x' = x \/ In x l'
    end.

  Hypothesis in_split : forall x l, In x l ->  exists l1 l2, l = l1 ++ x :: l2.
  Hypothesis in_app:    forall x l1 l2, In x (l1++l2) <-> In x l1 \/ In x l2.

  Inductive repeats : list X -> Prop :=            (***    repeats   ***)
    repeats_hd l x : In x l    -> repeats (x::l)
  | repeats_tl l x : repeats l -> repeats (x::l).

  Theorem pigeonhole_principle_NO_EM:              (***   pigeonhole   ***)
    forall l1  l2,
      length l2 < length l1 ->            (* There are more pigeons than nests *)
      (forall x, In x l1 -> In x l2) ->   (* All pigeons are in some nest *)
      repeats l1.                         (* Thus, some pigeons share nest *)
  Proof.

    (* ??? *)

The trick is that equality of membership proofs is still decidable. — András Kovács
Thanks @gallais. On lines 23-24 Agda considers the two cases that could have produced pr, either the constructor here! or there. How would one do that in Coq? (When I do i.e. inversion pr I don't get any information about which constructor was used to construct pr, see x80.org/collacoq/agikoxayom.coq) — larsr

stewbasic stewbasic · Accepted Answer · 2017-12-06T01:32:06

I'll describe the thought process that led me to a solution, in case it helps. We may apply induction and it is straightforward to reduce to the case l1 = a::l1', l2 = a::l2'. Now l1' is a subset of a::l2'. My EM-trained intuition is that one of the following holds:

a is in l1'.
a is not in l1'.

In the latter case, each element of l1' is in a::l2' but differs from a, and therefore must be in l2'. Thus l1' is a subset of l2', and we can apply the inductive hypothesis.

Unfortunately if In is not decidable, the above can't be directly formalized. In particular if equality is not decidable for the given type, it's difficult to prove elements are unequal, and therefore difficult to prove a negative statement like ~(In a l1'). However, we wanted to use that negative statement to prove a positive one, namely

forall x, In x l1' -> In x l2'

By analogy, suppose we wanted to prove

P \/ Q
Q -> R
------
P \/ R

The above intuitive argument is like starting from P \/ ~P, and using ~P -> Q -> R in the second case. We can use a direct proof to avoid EM.

Quantifying over the list l1' makes this a bit more complicated, but still we can construct a direct proof using the following lemma, which can be proven by induction.

Lemma split_or {X} (l : list X) (P Q : X -> Prop) :
  (forall x, In x l -> (P x \/ Q x)) ->
  (exists x, In x l /\ P x) \/ (forall x, In x l -> Q x).

Finally note that the intuitive pigeonhole principle could also be formalized as the following way, which cannot be proven when the type has undecidable equality (note that it has a negative statement in the conclusion):

Definition pigeon2 {X} : Prop := forall (l1 l2 : list X),
  length l2 < length l1 ->
  (exists x, In x l1 /\ ~(In x l2)) \/ repeats l1.

Pigeonhole proof without decidable equality or excluded middle

2 Answers