The Coq mailing list

[julien.forest AT ensiie.fr]

On Wed, 15 Oct 2014 22:09:49 -0400
Jason Gross 
<jasongross9 AT gmail.com>
 wrote:

> Hi,
> Is there a variant of Coq.Init.Fix_eq that allows you to prove
> properties about [Fix]es by well-founded induction?  That is, say
> that I have [Q : forall x, P x -> Type], and my goal is [Q x (@Fix A
> R Rwf P F x)].  If I do [rewrite Coq.Init.Fix_eq], I can then
> progress on my goal to the point where I am again faced with
> something like [Q y (@Fix A R Rwf P F y)].  Is there an induction
> principle for [Fix] that I can use to prove my goal? Intuitively, as
> long as the function has [Acc] fuel for recursing, I can use the same
> fuel to keep rewriting with [Fix_eq].
>
> Thanks,
> Jason

Hi Jason,

the short answer is no.

Maybe, depending on the fixpoint equation of your function, you can use
Function which generates such induction principles.

Best regards,

Julien