The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

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 don't think you really had an issue with the explicit "fix" in the script, but just in case, i've cleaned it up.


Require Import NArith.

Section nat_strong_rect.

  Variable (P: nat -> Type).

  Section helper_function.

    Definition helper_base_case (Po : P 0) (j : nat) (j_lt_1 : j < 1) :=
      eq_rect _ _ Po _ (Le.le_n_0_eq _ (Le.le_S_n _ _ j_lt_1)).

    Definition helper_recursive_case (n : nat) (f: forall m : nat, m < n -> P m)
     (Pn : P n) (m : nat) (m_lt_Sn : m < S n) :=
      match Compare_dec.le_lt_eq_dec _ _ m_lt_Sn with
      | left l => f _ (Lt.lt_S_n _ _ l)
      | right r => eq_rect_r _ Pn (eq_add_S _ _ r)
      end.

    Variable (F: forall n, P n).

    Fixpoint helper_fun (i:nat) :=
      match i return (P i -> forall j : nat, j < S i -> P j) with
      | 0 => helper_base_case
      | S i' => helper_recursive_case _ (helper_fun i')
      end (F i).

  End helper_function.

  Variable (f0 : forall n0 : nat, (forall m : nat, m < n0 -> P m) -> P n0).
   
  Fixpoint nat_strong_rect (a:nat) := f0 a
    match a return (forall m : nat, m < a -> P m) with
    | O => fun m H => False_rect (P m) (Lt.lt_n_O m H)
    | S b => helper_fun nat_strong_rect b
    end.
      
End nat_strong_rect.

2014-03-26 4:31 GMT-03:00 Guillaume Melquiond <guillaume.melquiond AT inria.fr>:

On 26/03/2014 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!". Sure enough, it does work,
and even more surprisingly, you can prove a strong recursion scheme over
the naturals using the same trick!

There must be something I am missing, as I don't understand how the example shows anything.

Strong recursion is just simple recursion applied to a more general property. So, by explicitly writing "fix" in your proof script, you are just complicating and obfuscating a proof that is trivial.

If the obtained lambda term was executing faster (less reduction steps for some evaluation strategy) with nested "fix"s rather than with a simple structural induction, that would be convincing. But that does not even seem to be true on your example.

Best regards,

Guillaume