The Coq mailing list

[roconnor AT theorem.ca]

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,

well_founded_induction_type =
fun (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Type)
  (X : forall x : A, (forall y : A, R y x -> P y) -> P x) (a : A) =>
Acc_iter P X (Rwf a)

Fix =
fun (A : Set) (R : A -> A -> Prop) (Rwf : well_founded R) (P : A -> Set)
  (F : forall x : A, (forall y : A, R y x -> P y) -> P x) (x : A) =>
Fix_F P F (Rwf x)

The only difference is one has P : A->Type, and the other has P : A->Set.
So I don't see how one can require a proof up-front and the other does
not.

It seems like it would be better to remove the Fix stuff and prove the
fixpoint equation for Acc_iter.

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