The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

On 26/03/2014 13:56, Hugo Carvalho wrote:
> I wanted to demonstrate a strong recursion scheme that didn't go through
> the well-founded machinery. The two texts i'm familiar with, and have a
> presentation of general recursion (Coq'Art, and CPDT), use it or
> something even more complicated. My point is, this shows how powerful
> regular "fix" over the naturals can be, instead of requiring you to
> recurse on the structure of some predicate. That's what i found
> unexpected, and would like to know more about.
>
> I don't know how it behaves regarding performance. I do remember,
> however, that computing with well-founded recursion can be tricky,
> sometimes needing you to construct "guarded" Acc proofs, or something
> like that. Perhaps this approach is better; perhaps nested "fix"es are
> even worse in this regard.

I stand by my point: the proof for a strong recursion scheme does not 
need to go through the well-founded machinery. As I said, your example 
is nothing more than the simple structural recursion over natural 
numbers. Here is a Coq script so that my point is clearer:

Definition nat_strong_rect (P : nat -> Type) :
  (forall n : nat, (forall m : nat, m < n -> P m) -> P n) ->
  forall n, P n.
Proof.
intros Hs n.
cut (forall m, m < S n -> P m).
  intros H.
  apply H.
  apply lt_n_Sn.
induction n as [|n In] ; intros m Hm.
  apply Hs.
  rewrite (proj1 (NPeano.Nat.lt_1_r _) Hm).
  intros k Hk.
  elim lt_n_0 with (1 := Hk).
apply gt_S_le in Hm.
destruct (le_lt_eq_dec _ _ Hm) as [H|H].
apply In with (1 := H).
rewrite H.
apply Hs with (1 := In).
Defined.

As you can see, I do not bother creating a well-founded relation here 
nor am I doing anything fancy. I am simply doing a naive recursion on n. 
The proof term contains a straightforward "fix" construct (inside 
nat_rect), so straightforward that it is the only one "induction" knows 
about.

To summarize, while "fix" is a powerful construct, strong recursion is 
not a good example of its power.

Best regards,

Guillaume