The Coq mailing list

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

Hi Vedran,

"> 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?"

So when I asked this question, it did not occur to me that I needed to
take fuel computation also into consideration. In my limited
experience of using Coq, it is always the second case, "computing the
fuel from arguments of a function", e.g., in computing the byte_list
function, I need (log256 np) amount of fuel for a (binary) natural
number np. But I never came across any interesting function that just
takes a fixed number (independent of function input) as fuel, so I
guess it was never in my mind but of course, it was not explicit in
the question.

"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."

Yep, this is also my understanding.

Best,
Mukesh




>
> č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ć