The Coq mailing list

[Basile Clement <basile AT clement.pm>]

On 08/20/2014 12:07 PM, John Wiegley wrote:
> Hello,
>
> There are two exercises in Software Foundations that have me stumped at the
> moment.  The first is "rev_pal" from Prop.v.  Is there a way to solve this
> more simply than defining a new induction principle for lists that looks at
> both ends?  If so, a hint would be lovely.  If not, knowing that I must go
> that route is also appreciated.

Instead of writing your own induction principle, you can use the list's 
length and first prove

    forall (X:Type) (n:nat) (l:list X), length l <= n -> l = rev l -> pal l

This can be proven quite easily by induction on [n], although it is only 
simpler in the sense that the natural numbers and a couple of theorems 
on the [length] function have already been proven.

> 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?  So far I have:
>
>      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.
>      Proof.
>        move=> X.
>        elim=> [|x xs IHxs] l2 Happ Hlen.
>          inversion Hlen.
>        apply repeats_tail.
>        apply: IHxs => // [z ?|].
>        apply: Happ. by constructor.
>      Admitted.
>
> I'm missing information about the 'x' it seems.  I can imagine two scenarios:
>
>    l1: [1,2,3,1]  l2: [1,2,3]
>    l1: [2,1,3,1]  l2: [2,1,3]
>
> My attempt lacks knowledge about whether 'x' is a repeating element, which
> would determine the constructor to use, and thus give me the knowledge that
> should make the remainder provable.  But how?  Even with LEM I get stuck in
> the same spot, so a clue on solving it that way would also be helpful.
>
> Thanks,
>    John
--
Basile