Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Induction principle for Fix?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Induction principle for Fix?


Chronological Thread 
  • From: julien.forest AT ensiie.fr
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Induction principle for Fix?
  • Date: Thu, 16 Oct 2014 07:29:00 +0200


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





Archive powered by MHonArc 2.6.18.

Top of Page