The Coq mailing list

[Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>]

Thanks very much!  Each of these solutions would work.

Cheers,

Jeremy

On 25/4/20 9:03 pm, Théo Winterhalter wrote:
> 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