The Coq mailing list

[Hugo Carvalho <hugoccomp AT gmail.com>]

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!

The rest of this email is Coq code establishing so. But can someone point me towards a reference indicating this is actually known? That is, just how strong can the application of nested fixpoints be in Coq?


Require Import NArith.

Lemma obv : forall m, m < 1 -> m = 0.
intros. unfold lt in H.
symmetry. apply Le.le_n_0_eq.
auto with arith. Defined.

Definition lt_fun_comp_create :
forall (P: nat -> Type) n, P n ->
(forall m : nat, m < n -> P m) ->
(forall m : nat, m < (S n) -> P m ). intros.
destruct (Compare_dec.le_lt_eq_dec _ _ H).
apply X0.
SearchAbout lt. apply (Lt.lt_S_n _ _ l).
SearchAbout S. rewrite (eq_add_S _ _ e). apply X. Defined.

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.
refine (
 fix F (a:nat) : P a :=
   match a as a0 return (P a0) with
   | 0 => _
   | S b => _
   end
).
apply f0. intros. exfalso. apply (Lt.lt_n_0 _ H).
apply f0.
refine (
(fix aux (i:nat) :=
              match i as i0
                return (P i0 -> forall m : nat, m < S i0 -> P m) with
              | 0 => _
              | S i' => _
              end (F i)) b
). intros. rewrite (obv _ H). apply X.
intro fi. apply lt_fun_comp_create. apply fi. apply aux. Defined.

2014-03-18 17:27 GMT-03:00 Pierre Boutillier <pierre.boutillier AT pps.univ-paris-diderot.fr>:

Le 18 mars 2014 à 02:10, Geoff Hulette <ghulette AT gmail.com> a écrit :

> Is there an easy way to convince Coq to accept the following recursion?

Yes but it implies to know about the gory detail of the guard condition…

if something is a parameter (identical for all recursive calls) put it as so :
Definition sum_to (f : nat -> nat): nat -> nat :=
fix aux i :=

  match i with
  | O => f O

  | S i' => f i + (aux i')
  end.

This is not enough : O when i is O and when i is a sub term is not a sub term … but i (that is equal to O) is so :
Definition sum_to (f : nat -> nat): nat -> nat :=
fix aux i :=

  match i with
  | O => f i

  | S i' => f i + (aux i')
  end.
is the sum_to definition that will make problem works !

> Parameter G : nat -> nat.
>
> Fixpoint problem (t : nat) : nat :=
>   match t with
>   | O => G O
>   | S t' => sum_to t' (fun t_i => G (problem t_i))
>   end.

All the best,
Pierre B.