The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

As I am not used to Coq.Init.Fix_eq, I do not fully understand the question, but if you can prove something like "AccRx : Acc R x" then if you start your proof with "induction AccRx." then you should have to prove that "forall x, (forall y, R x y -> Q x (@Fix A R Rwf P F y)) -> Q x (@Fix A R Rwf P F y)".
From there, you do your "intros x Hx", and your rewrite Coq.Init.Fix_eq to go to the point where you have to face something like "Q y (@Fix A R Rwf P F y)". There you apply Hx, and you only have to prove that you have "R x y", which I guess should be the case.

2014-10-16 4:09 GMT+02:00 Jason Gross <jasongross9 AT gmail.com>:

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

--
.../Sedrikov\...