The Coq mailing list

[David Pichardie <david.pichardie AT irisa.fr>]

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. It's a beautiful experience but
it gives sometimes a headache...
The problem with Fix_F is that it requires an extra hypothesis on the 
functionnal you use (F_ext).

See the chapter about general recursion in the Coq'Art for more details.

Hope this helps,

David.

Le 27 juil. 05, à 18:34, 
roconnor AT theorem.ca
 a écrit :

> On Wed, 27 Jul 2005 
> roconnor AT theorem.ca
>  wrote:
>
> > What's the difference between Fix_F and Acc_iter?
>
> The follow up question is then ``What is the difference between Fix and
> well_founded_induction?''; other than the fact that Fix has a bunch of
> nice lemmas about it, while well_founded_induction does not.
>
> --
> Russell O'Connor                                      <http://r6.ca/>
> ``All talk about `theft,''' the general counsel of the American 
> Graphophone
> Company wrote, ``is the merest claptrap, for there exists no property 
> in
> ideas musical, literary or artistic, except as defined by statute.''
> --------------------------------------------------------
> Bug reports: http://coq.inria.fr/bin/coq-bugs
> Archives: http://pauillac.inria.fr/pipermail/coq-club
>           http://pauillac.inria.fr/bin/wilma/coq-club
> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - 
-
David Pichardie
http://www.irisa.fr/lande/pichardie/index.en.html