The Coq mailing list

[Pierre Letouzey <letouzey AT lri.fr>]

On Mon, 1 Aug 2005 
roconnor AT theorem.ca
 wrote:

> On Thu, 28 Jul 2005, David Pichardie wrote:
>
> > Hi Russell,
> >
> > In my opinion Fix_F is only provided to propose a fixpoint equation
> > lemma Fix_eq
> > http://coq.inria.fr/library/Coq.Init.Wf.html#Fix_eq ;.
> > Hence you can define your function with a weak type (nat -> nat for
> > example) with the Fix_F
> > constructor and in a second time make proof on it.
> > With Acc_iter, you have to use a strong type which contains the
> > specification (or a part of it)
> > of your function and prove its correctness at the same time you program
> > it.
>
> I'm afraid I don't see this.  The definitions of Acc_iter and Fix_F are
> almost identical, and the terms for well_founded_induction_type and Fix
> are similarly almsot identical,
>

Hi

I recall now that I'm the one that introduced Acc_iter in Wf.v, more than
two years ago, after a remark by Yves Bertot. He noticed that
well_founded_induction was at that time defined using Acc_rec(t) whereas a
weaker induction principle (the current Acc_iter) was enough for the job.

And well ... it seems that I didn't noticed at that time that my newly
added Acc_iter and the Fix_F slightly below were identical. Shame on me...

So we should probably get rid of one of the two. Hopefully, I
doubt that Acc_iter and Fix_F are often used directly in existing
contributions.

Best regards,

Pierre Letouzey