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?
Maybe simpl in H
to get 0 > 0, then lia
?
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.
 rewrite (ltn_add2r 1) addn1.
by apply: (leq_trans H); rewrite addnC leq_add2l.
by case=>x Hx; exists x=>/Hx; rewrite inE=>>; rewrite orbT.
Qed.
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?
Indeed, the current statement has a much shorter proof: (by exists O.
), I guess the >
should be a /\
Yeah you see during the proof that implication is sorta useless
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