The Coq mailing list

[Xavier Leroy <xavier.leroy AT inria.fr>]

On 2014-03-26 05:22, Hugo Carvalho wrote:
> Whoa, hold on. I looked at this, and thought, "Surely it can't work
> Coq's fix is primitive recursive, so no way this kind of definition
> works without some well-founded trickery!". 

As Guillaume hinted, you can derive your induction principle

Definition mult_rect_str (P : nat -> Type)
  (f0 : forall n0 : nat, (forall m : nat, m < n0 -> P m) -> P n0) :
  forall n:nat, P n.

from the primitive recursor nat_rect:

nat_rect: forall Q : nat -> Type,
       Q 0 -> (forall n : nat, Q n -> Q (S n)) -> forall n : nat, Q n

just by taking Q := fun n => forall m, m < n -> P m.

So, no black magic here.

> That is, just how strong can the application of nested fixpoints be
> in Coq?

As a case in point, you can define Ackermann's function with a fix
nested in a fix.  So, clearly, you're going beyond primitive
recursion...

- Xavier Leroy