## Stream: Coq users

### Topic: Pigeonhole principle

#### Julin S (Jun 13 2022 at 07:42):

I once found a statement of a version of pigeonhole principle online (couldn't recall where it was, but probably somewhere in stackexchange) that goes like this:

``````forall l:list nat,
list_sum l > length l -> exists x:nat, x > 1 -> In x l.
``````

I gave it a try and (as usual in my case) couldn't go much beyond the statment.

``````Require Import List.
Import ListNotations.

Theorem ph : forall l:list nat,
list_sum l > length l -> exists x:nat, x > 1 -> In x l.
Proof.
intros.
induction l.
-
``````

The goal at this point was:

``````1 subgoal
(1 unfocused at this level)

H : list_sum [] > length []

========================= (1 / 1)

exists x : nat, x > 1 -> In x []
``````

The `list_sum [] > length []` would be `False`, right?

How can I discharge the base case of the induction in this case?

#### Paolo Giarrusso (Jun 13 2022 at 07:56):

Maybe `simpl in H` to get 0 > 0, then `lia`?

#### Alexander Gryzlov (Jun 13 2022 at 22:42):

here's the proof in ssreflect:

``````Lemma pigeonhole (l : seq nat) :
size l < sumn l -> exists x: nat, 1 < x -> x \in l.
Proof.
elim: l=>//=h t IH; case: (ltnP 1 h)=>Hh H.
- by exists h=>_; rewrite inE eq_refl.
have/IH : size t < sumn t.
by case=>x Hx; exists x=>/Hx; rewrite inE=>->; rewrite orbT.
Qed.
``````

#### Paolo Giarrusso (Jun 14 2022 at 09:07):

I'm missing something, why's this the right statement? Don't you want that there's an x that is in the list and is greater than 1?

#### Pierre Roux (Jun 14 2022 at 09:15):

Indeed, the current statement has a much shorter proof: (`by exists O.`), I guess the `->` should be a `/\`

#### Alexander Gryzlov (Jun 14 2022 at 11:32):

Yeah you see during the proof that implication is sorta useless

#### Alexander Gryzlov (Jun 14 2022 at 11:34):

It's not hard to switch to conjunction though, the idea and the structure stays the same :)

Last updated: Oct 03 2023 at 20:01 UTC