The Coq mailing list

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

"Both for programming and for mathematics, I'd rather use well-founded
recursion than nat-valued fuel. "

Agree but there are few cases, e.g., if you want to evaluate a
function inside the Coq itself, then well-founded functions may not
reduce due to some opaque proof terms (at least this is my
experience). In one project, I wanted to evaluate the SHA256  hash [1]
inside the Coq itself and therefore picked the fuel based solution,
rather than well-founded.

Best,
Mukesh

[1] 
https://github.com/mukeshtiwari/Formally_Verified_Verifiable_Group_Generator/blob/main/src/Sha256.v#L879

On Fri, May 19, 2023 at 6:07 PM Xavier Leroy
<xavier.leroy AT college-de-france.fr> wrote:
>
> On Fri, May 19, 2023 at 6:45 PM mukesh tiwari 
> <mukeshtiwari.iiitm AT gmail.com> wrote:
>>
>> Thanks Yannick and Mario! I was somehow under a (flawed) assumption
>> that functions that computes fuel were alway primitive recursive, but
>> it may or may not be the case. So my understanding is: theoretically
>> it is possible to turn an non-primitive recursive function into a
>> primitive recursive function (Kleene's normal form theorem) by means
>> of using nat as a fuel, but computing the fuel may be as complicated
>> as computing the original function, i.e., it may not be primitive
>> recursive.  I also came up with a counterexample for my flawed
>> assumption: I can write a division function on natural numbers using
>> the subtraction function (I know it is not a great way to write
>> division function):
>>
>> Theorem nat_div :  nat -> forall (b : nat),
>>     0 < b -> nat * nat.
>>   Proof.
>>     intro a.
>>     cut (Acc lt a);
>>     [revert a |].
>>     +
>>       refine(fix nat_div a (acc : Acc lt a) {struct acc} :
>>         forall b : nat, 0 < b -> nat * nat :=
>>         match acc with
>>         | Acc_intro _ f => fun b Ha =>
>>           match (lt_eq_lt_dec a b) with
>>           | inleft Hb =>
>>             match Hb with
>>             | left Hc => (0, a)
>>             | right Hc => (1, 0)
>>             end
>>           | inright Hb =>
>>             match nat_div (a - b) _ b Ha with
>>             | (q, r) => (S q, r)
>>             end
>>           end
>>         end).
>>       assert (Hc : (a - b) < a).
>>       abstract nia.
>>       exact (f (a - b) Hc).
>>     +
>>       eapply lt_wf.
>>   Defined.
>>
>> But if I want to turn this into a primitive recursive function by
>> means of fuel, then computing fuel itself requires a division
>> function.
>
>
> Not in this case.  You  can always over-approximate how much fuel you need. 
>  In this case taking "a" as the fuel should suffice.
>
>
>>
>> In conclusion, theoretically it is possible but there could
>> be a situation where it is not a very good idea for programming
>> (constructive mathematics?).
>
>
> Both for programming and for mathematics, I'd rather use well-founded 
> recursion than nat-valued fuel.  Think of well-founded recursion as 
> recursing on a fuel that is a proof of accessibility in an order of your 
> choice.  This gives more flexibility than recursing on silly Peano natural 
> numbers.  In particular, because you can choose the order, proving 
> accessibility is generally easier than proving the existence of a large 
> enough nat-valued fuel.
>
> For what it's worth...
>
> - Xavier Leroy
>
>
>
>
>>
>>
>>
>> Best,
>> Mukesh
>>
>>
>>
>> On Thu, May 18, 2023 at 7:12 PM Yannick Forster <yannick AT yforster.de> 
>> wrote:
>> >
>> > Sure, computing the fuel is not going to be primitive recursive because 
>> > the fuel is large. But given a defined Coq (or any other constructive 
>> > type theory) function f : nat -> nat it can be turned into a primitive 
>> > recursive function f' : nat -> nat -> nat such that f' n x = S v, then 
>> > for all n' >= n, f' n x = S v and forall x, exists n, f' n x = S (f x).
>> >
>> > Here, f' is a primitive recursive function expecting fuel n and an 
>> > argument x, and then computes f for large enough fuel (and else returns 
>> > 0). The n might, as you say, have to be very large, but constructing f' 
>> > is always possible.
>> >
>> >
>> > On 18 May 2023 20:04:06 Mario Carneiro <di.gama AT gmail.com> wrote:
>> >>
>> >> This doesn't sound quite correct. While Kleene's T tells you that for 
>> >> any terminating computation there is *some* bound for the fuel you need 
>> >> to compute the value, the bound itself might be quite large, and so you 
>> >> are reduced to computing very fast growing functions, to compute the 
>> >> initial fuel value you use to power the rest of the computation. These 
>> >> functions need just as much "power" from the theory as the original 
>> >> recursion did. There are functions which are not primitive recursive, 
>> >> like the ackermann function, and if you rewrite them to use a fuel 
>> >> variable you will need to supply a function which grows about as fast 
>> >> as the ackermann function to get the initial fuel value, and that 
>> >> function is also not primitive recursive.
>> >>
>> >> Now, Ackermann's function is computable in Coq because it has higher 
>> >> order functions and hence goes beyond the traditional conception of 
>> >> primitive recursive function, but I think you might still need more 
>> >> than just N-indexed inductions to get the full power of Coq terminating 
>> >> functions. There are inductive types with a much larger rank than N 
>> >> around, and I don't think you can get epsilon_0 induction simply by 
>> >> composing inductions of rank omega.
>> >>
>> >> On Thu, May 18, 2023 at 1:48 PM Yannick Forster <yannick AT yforster.de> 
>> >> wrote:
>> >>>
>> >>> Hi Mukesh,
>> >>>
>> >>> in computability theory this intuition is behind Kleene's normal form 
>> >>> theorem: https://en.m.wikipedia.org/wiki/Kleene%27s_T_predicate
>> >>>
>> >>> You can prove the normal form theorem for computable functions in Coq 
>> >>> when defining them using some model of computation. But since given 
>> >>> any concrete Coq function (over natural numbers or some suitable 
>> >>> datatype isomorphic to numbers) you could have implemented it as a 
>> >>> function in a model of computation provided enough time and endurance, 
>> >>> this means you can re-write any definable Coq function as a fueled 
>> >>> primitive recursive function, yes.
>> >>>
>> >>> Best
>> >>> Yannick
>> >>>
>> >>> On 18 May 2023 19:35:56 mukesh tiwari <mukeshtiwari.iiitm AT gmail.com> 
>> >>> wrote:
>> >>>
>> >>>> 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
>> >>>
>> >>>
>> >