The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

This is a remark about a one year old thread.
It was about proving the finite Pigeon Hole Principle (PHP)
WITHOUT assuming either the excluded middle or the decidability
of equality over the given type.

A simple trick is to generalize the PHP a bit to
take the case where length l <= length m into account,
i.e. replacing the length l < length m hypothesis with
the lesser assumption length l <= length m.

In that case, it is possible that no duplication occurs,
but then, the two lists must be permutable (and thus have
the same length).

Using that simple generalisation, induction over length l
works like a charm, even in the non-informative Prop case.

Dominique Larchey-Wendling

--------------------------

Require Import List.
Require Import Permutation.

Infix "~p" := (Permutation) (at level 70, no associativity).

Section intuitionistic_pigeon_hole.

  Variable (X : Type).

  Inductive list_has_dup : list X -> Prop :=
    | in_lhd_1 : forall x l, In x l -> list_has_dup (x::l)
    | in_lhd_2 : forall x l, list_has_dup l -> list_has_dup (x::l).

  Notation lhd := list_has_dup.

  (* that one can be proved without Excluded middle
     and without assuming that (@eq X) is decidable
   *)

  Fact length_le_and_incl_implies_dup_or_perm l :
               forall m, length l <= length m
                      -> incl m l
                      -> lhd m \/ m ~p l.
  Proof.
    (* by induction on length l *)
  Admitted.

  (* deducing the pigeon hole principle is then straightforward *)

  Theorem finite_pigeon_hole l m :
            incl m l
         -> length l < length m
         -> lhd m.
  Proof.
    (* use length_le_and_incl_implies_dup_or_perm *)
  Admitted.

End intuitionistic_pigeon_hole.