coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Induction principle for Fix?, Jason Gross, 10/16/2014
- Re: [Coq-Club] Induction principle for Fix?, Cedric Auger, 10/16/2014
- Re: [Coq-Club] Induction principle for Fix?, Jason Gross, 10/16/2014
- <Possible follow-up(s)>
- Re: [Coq-Club] Induction principle for Fix?, julien . forest, 10/16/2014
- Re: [Coq-Club] Induction principle for Fix?, Cedric Auger, 10/16/2014
Archive powered by MHonArc 2.6.18.