The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Indeed, I can prove:

  Definition Fix_rect

          A (R : A -> A -> Prop) (Rwf : well_founded R)

          (P : A -> Type) (F : forall x : A, (forall y : A, R y x -> P y) -> P x)

          (Q : forall x, P x -> Type)

          (H : forall x, (forall y, R y x -> Q y (@Fix A R Rwf P F y)) -> Q x (@F x (fun (y : A) (_ : R y x) => @Fix A R Rwf P F y)))

          (F_ext : forall (x : A) (f g : forall y : A, R y x -> P y),

                   (forall (y : A) (p : R y x), f y p = g y p) -> F _ f = F _ g).

          x

  : @Q x (@Fix A R Rwf P F x).

  Proof.

    induction (Rwf x).

    rewrite Init.Wf.Fix_eq; auto.

  Defined.

Thanks,

Jason

On Thu, Oct 16, 2014 at 5:29 AM, Cedric Auger <sedrikov AT gmail.com> wrote:

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\...