The Coq mailing list

[BEGAY Pierre-leo <pbegay AT ens-cachan.fr>]

Hello,

I've had the same issue recently, the problem was that I used a  
Fixpoint where a Definition was sufficient. I guess simpl does not  
perform "terminal computations" on Fixpoints, but only tries to  
simplify the recursive call, maybe someone else can elaborate on that.

As far as I can tell, you do not need to use a Fixpoint either, so  
that may be the source of your problem.

Cheers,
Pierre-Léo Bégay


Jeremy Dawson 
<Jeremy.Dawson AT anu.edu.au>
 a écrit :

> Hi,
>
> I have a definition
>
> Fixpoint dersrec_hd X rules prems c cs
>   (ders : @dersrec X rules prems (c :: cs)) :=
>   match ders with
>     | dlCons d ds => d
>   end.
>
> but when I try do prove the following, I would expect the simpl step  
> to simplify it to d = d
>
> Lemma dersrec_hd_eq X rs ps c cs
>   (d : @derrec X rs ps c) (ds : @dersrec X rs ps cs) :
>   dersrec_hd (dlCons d ds) = d.
> Proof. simpl. (* does nothing *)
>
> What could be the reason for failure here?
>
> Thanks
>
> Jeremy Dawson