The Coq mailing list

[Xavier Leroy <xavier.leroy AT inria.fr>]

On 20/08/2014 12:07, John Wiegley wrote:
> The second is "pigeonhole_principle".  With or without LEM I run into the 
> same
> problem: a goal of n < m in a context of n < S m, which is clearly 
> unprovable.
> If induction on l1 is the right way to start this proof, what is the next
> creative step?

Hint: you need to use the lemma "appears_in_app_split" that SF asks
you to prove just before.  (How convenient!)

>     Theorem pigeonhole_principle: forall (X:Type) (l1 l2:list X),
>       (forall x, appears_in x l1 -> appears_in x l2)
>         -> length l2 < length l1
>         -> repeats l1.

More detailed hint: in the case l1 = x :: l1', when you need to use
the induction hypothesis, decompose l2 as l2' ++ x :: l2'' and
use the ind. hyp. with l2 = l2' ++ l2''.

Hope this helps,

- Xavier Leroy