The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wednesday, October 02, 2013 11:05:44 AM N. Raghavendra wrote:
> Definition pigeonhole_principle (X : Type) : Prop :=
>   forall l1 l2 : list X,
>     (forall x : X, appears_in x l1 -> appears_in x l2) ->
>     length l2 < length l1 ->
>     repeats l1.
[...]
> Theorem exmid_appears_in_pigeonhole_principle :
>   forall X : Type,
>     exmid_appears_in X -> pigeonhole_principle X.

For what it's worth, here's a proof of pigeonhole_principle without any 
excluded middle assumptions.

Require Import List.
Require Import Permutation.

Inductive appears_in {X:Type} (x:X) : list X -> Prop :=
| appears_in_first (l : list X) : appears_in x (x :: l)
| appears_in_later (y:X) (l:list X) :
    appears_in x l -> appears_in x (y :: l).

Inductive repeats {X : Type} : list X -> Prop :=
| repeats_1 : forall (x : X) (l : list X),
                appears_in x l -> repeats (x :: l)
| repeats_2 : forall (x : X) (l : list X),
                repeats l -> repeats (x :: l).

Proposition appears_in_app {X:Type} : forall (x:X) (l1 l2:list X),
  appears_in x (l1 ++ l2) -> appears_in x l1 \/ appears_in x l2.
Proof.
intros x l1; revert x; induction l1.
+ right; trivial.
+ intros.
  simpl in H.
  inversion H.
  - left; constructor.
  - destruct (IHl1 _ _ H1).
    * left; constructor; trivial.
    * right; trivial.
Qed.

Proposition appears_in_tl {X:Type} :
  forall (x:X) (l1 l2:list X), appears_in x l2 -> appears_in x (l1 ++ l2).
Proof.
induction l1.
+ trivial.
+ intros.
  simpl.
  constructor.
  auto.
Qed.

Proposition appears_in_both_impl_repeats_app {X:Type} :
  forall (x:X) (l1 l2:list X), appears_in x l1 -> appears_in x l2 ->
  repeats (l1 ++ l2).
Proof.
intros x l1 l2 ?; revert l2.
induction H; intros.
+ simpl.
  constructor.
  now apply appears_in_tl.
+ simpl.
  constructor 2.
  auto.
Qed.

Proposition appears_in_permutation {X:Type} :
  forall (x:X) (l1 l2:list X),
  Permutation l1 l2 -> appears_in x l1 -> appears_in x l2.
Proof.
induction 1; auto; intros;
repeat match goal with
| H : appears_in ?x (?y :: ?l) |- _ => inversion H; clear H; subst
end; eauto using appears_in_first, appears_in_later.
Qed.

Lemma appears_in_permute_to_front {X:Type} :
  forall (x:X) (l:list X), appears_in x l ->
  exists l':list X, Permutation l (x :: l').
Proof.
induction 1.
+ exists l.
  reflexivity.
+ destruct IHappears_in as [l' ?].
  exists (y :: l').
  transitivity (y :: x :: l').
  - constructor; trivial.
  - constructor.
Qed.

Lemma pigeonhole_principle_helper (X:Type) :
  forall hd l1 l2 : list X,
  (forall x:X, appears_in x l1 -> appears_in x (hd ++ l2)) ->
  length l2 < length l1 -> repeats (hd ++ l1).
Proof.
intros hd l1.
remember (length l1) as n.
revert hd l1 Heqn; induction n.
+ intros.
  inversion H0.
+ intros.
  destruct l1 as [x l1 | ]; try discriminate.
  simpl in Heqn.
  injection Heqn; intros; clear Heqn.
  assert (appears_in x (hd ++ l2)).
  - apply H.
    constructor.
  - destruct (appears_in_app _ _ _ H2).
    * eapply appears_in_both_impl_repeats_app.
      { eexact H3. }
      { constructor. }
    * replace (hd ++ x :: l1) with ((hd ++ x :: nil) ++ l1).
      { destruct (appears_in_permute_to_front _ _ H3) as [l2' ?].
        apply IHn with (l2 := l2'); trivial.
        { intros.
          rewrite <- app_assoc.
          simpl.
          refine (appears_in_permutation _ _ _ _ (H _ _)).
          { now apply Permutation_app_head. }
          { now constructor. }
        }
        { rewrite (Permutation_length H4) in H0.
          simpl in H0.
          auto with arith.
        }
      }
      { rewrite <- app_assoc. reflexivity. }
Qed.

Theorem pigeonhole_principle (X : Type) :
  forall l1 l2 : list X,
    (forall x : X, appears_in x l1 -> appears_in x l2) ->
    length l2 < length l1 ->
    repeats l1.
Proof.
intros.
apply pigeonhole_principle_helper with (hd := nil)
  (1 := H) (2 := H0).
Qed.
-- 
Daniel Schepler