The Coq mailing list

[Théo Winterhalter <theo.winterhalter AT ens-cachan.fr>]

Even a fixpoint with no recursive call, has a recursive argument.
This argument is then used a syntactic guard to block reduction, unless it is 
a constructor.

If you print your term you will see that the recursive argument is probably 
not ders but the first argument that is of an inductive type.
You can fix this as Pierre-Léo suggest by using Definition instead of 
Fixpoint, or by explicitly saying that ders is the recursive argument by 
adding {struct ders} before the :=.

> Le 25 avr. 2020 à 12:58, BEGAY Pierre-leo 
> <pbegay AT ens-cachan.fr>
>  a écrit :
> 
> 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
> 
> 
>