The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

The FAQ is on the wiki https://github.com/coq/coq/wiki/The-Coq-FAQ so you 
don't need a Coq maintainer to edit it.

Related: 
https://github.com/coq/coq/blob/9f2d0734338da7db55b4438c1985b10a3abfc17f/theories/Init/Wf.v#L172

Gaëtan Gilbert

On 20/05/2023 10:32, Xavier Leroy wrote:
> On Fri, May 19, 2023 at 9:19 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com 
> <mailto:mukeshtiwari.iiitm AT gmail.com>> wrote:
>
>     "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). 
>
>
> You can use Braibant's trick: 
> https://sympa.inria.fr/sympa/arc/coq-club/2010-02/msg00016.html 
> <https://sympa.inria.fr/sympa/arc/coq-club/2010-02/msg00016.html>
>
> Note to the Coq FAQ maintainers: this question (how to evaluate well-founded 
> recursions) comes up repeatedly.  What about putting Braibant's trick in the 
> FAQ?
> - Xavier Leroy
>
>     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
>  
> <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 
> <mailto:xavier.leroy AT college-de-france.fr>> wrote:
>      >
>      > On Fri, May 19, 2023 at 6:45 PM mukesh tiwari <mukeshtiwari.iiitm AT gmail.com 
> <mailto: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 
> <mailto: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 
> <mailto: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 
> <mailto: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 
> <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 
> <mailto: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 
> <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
>  
> <https://github.com/mukeshtiwari/Formally_Verified_Verifiable_Group_Generator/blob/main/src/Sha256.v#L239>
>      >> >>>
>      >> >>>
>      >> >