The Coq mailing list

["John Wiegley" <johnw AT newartisans.com>]

>>>>> Soegtrop, Michael 
>>>>> <michael.soegtrop AT intel.com>
>>>>>  writes:

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

Using Function instead of Fixpoint, you should be able to supply a "measure"
to prove termination, for example:

  Function rev_pal' X (l : list X) (h : l = rev l) {measure length l} : pal X 
l.

Thanks for all the hints, I now have several interesting avenues to pursue!

John