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.
- 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.

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: Apr 18 2024 at 02:01 UTC