The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Hi everyone,

Is it always possible to turn a non-primitive (terminating) recursive
function into a primitive recursive function by passing a natural
number as a fuel? If so, is there any formal underpinning for this,
i.e., turning a non-primitive (terminating) recursive function into a
primitive recursive function by passing a natural number, or is it
just obvious? My intuition says it's true but I am very keen to see
some formal reasoning.

For example, I can write a function that computes a byte list from a
(binary) natural number like this [1] (I call it non-primitive
(terminating) recursive function but I may not be correct with my
terminology):

Definition length_byte_list_without_guard : N -> list byte.
 Proof.
    intro np.
    cut (Acc lt (N.to_nat np));
    [revert np |].
    +
      refine(fix length_byte_list_without_guard np (acc : Acc lt (N.to_nat 
np))
        {struct acc} :=
      match acc with
      | Acc_intro _ f =>
        match (np <? 256) as npp
          return _ = npp -> _
        with
        | true => fun Ha => List.cons (np_total np Ha) List.nil
        | false => fun Ha =>
            let r := N.modulo np 256 in
            let t := N.div np 256 in
            List.cons (np_total r _) (length_byte_list_without_guard t _)
        end eq_refl
      end).
      ++
        apply N.ltb_lt, (nmod_256 np).
      ++
        apply N.ltb_ge in Ha.
        assert (Hc : (N.to_nat t < N.to_nat np)%nat).
        unfold t. rewrite N2Nat.inj_div.
        eapply Nat.div_lt; try abstract nia.
        exact (f (N.to_nat t) Hc).
    +
      apply lt_wf.
 Defined.

But I can also write the same function by passing a natural number [2]
(from top level,
I just need to ensure the right amount of fuel):

Fixpoint byte_list_from_N_fuel (n : nat) (up : N) : list byte :=
  match n with
  | 0%nat => [np_total (N.modulo up 256) (nmod_256_dec up)]
  | S n' =>
    let r := N.modulo up 256 in
    let t := N.div up 256 in
    List.cons (np_total r (nmod_256_dec up)) (byte_list_from_N_fuel n' t)
  end.

Best,
Mukesh

[1] https://github.com/mukeshtiwari/Coq-automation/blob/master/Opaque.v#L75
[2] 
https://github.com/mukeshtiwari/Formally_Verified_Verifiable_Group_Generator/blob/main/src/Sha256.v#L239