The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear John,

instead of an inductive proof, you can make a "recursive proof", that is 
define a fixpoint which takes an argument of type l = rev l and returns pal X 
l.
You can use tactics to create the function body. The syntax looks like this:

Fixpoint rev_pal' X (l : list X) (h : l = rev l) : pal X l.
Proof.
...
Use rev_pal' in the proof
...
Qed.

It is still quite tricky, though. To convince Coq that this terminates, I had 
to add the list length as parameter.

Best regards,

Michael

-----Original Message-----
From: John Wiegley 
[mailto:jwiegley AT gmail.com]
 On Behalf Of John Wiegley
Sent: Wednesday, August 20, 2014 12:07 PM
To: 
coq-club AT inria.fr
Subject: [Coq-Club] Hints needed for two SF exercises

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.

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