The Coq mailing list

[Vedran Čačić <veky AT math.hr>]

I'm not sure I understand... do you intend to pass a fixed number as a fuel, or to calculate fuel from other arguments of a function? In the first case, of course, you can compute only a finite segment of your intended function. In the second case, how is the function that calculates the fuel needed, classified? If the fuel-calculating function itself is primitive recursive, then yes, the function using that fuel is also primitive recursive (consequence of Kleene's normal form, plus bounded minimization). But for example Ackermann's function uses too much fuel to be expressible as a primitive recursive function.

čet, 18. svi 2023. u 19:36 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> napisao je:

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

--

Vedran Čačić