The Coq mailing list

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

>I'm 98% sure that the output of
> Program Fixpoint actually really does need to compute through the opaque
> parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing the point.

Yes, this is a known problem, see https://github.com/coq/coq/pull/7060 
(which is not progressing currently, see discussion there)

Gaëtan Gilbert

On 01/11/2018 23:05, Peter E Schmidt-Nielsen wrote:
> Good point Li-yao, I feel really silly for writing "Program Fixpoint" 
> for the nat-fueled version. I copied it over by analogy from the 
> BinNat-fueled version I tried to get to work when I saw Klaus's original 
> suggestion to use fuel. I got stuck on the BinNat version, and somehow 
> had a moment of silliness and forgot that obviously Program Fixpoint's 
> features are completely unnecessary with a plain nat for fuel.
>
> Daniel's sugar for making this easier to write also looks great.
>
> Not to hijack the thread, but I'm really curious if anyone has any leads 
> on getting the BinNat-fueled version (appearing below the nat-fueled one 
> in my gist) to work? The great thing about such a version is that you 
> can just past in some obscene value like 2^200 for the fuel in every 
> case and never worry about it, while with a nat for fuel I'm quite 
> constrained on how much fuel I can provide. (I figure this isn't really 
> thread hijacking, because I think getting a BinNat-fueled version 
> working would basically practically solve this issue for OP.)
>
> I looked at the "Type classes for efficient exact real arithmetic in 
> Coq" paper that was linked, but I'm not sure the laziness suggested via 
> eta expansion solves this problem, as I'm 98% sure that the output of 
> Program Fixpoint actually really does need to compute through the opaque 
> parts of N.lt_pred_l and N.lt_wf_0, although maybe I'm missing the point.
>
> If there were some generic mechanism that could take an opaque term and 
> trace all the dependencies Print Opaque Dependencies style and make a 
> transparent version (or somehow override the opacity) then it would 
> completely solve the problem...
>
> Thanks,
>
> -snp
>
> On Thu, 1 Nov 2018, Daniel Schepler wrote:
>
> > On Thu, Nov 1, 2018 at 9:35 AM Li-yao Xia 
> > <lysxia AT gmail.com>
> >  wrote:
> > > If you're using fuel it is fairly easy to make it structurally
> > > decreasing with a simple Fixpoint because fuel can just decrease by 1,
> > > instead of using a Program and proving decreasingness with respect to 
> > > lt.
> >
> > Or, to put a bit of monad-type synactic sugar around it:
> >
> > Definition fuelled (X : Type) : Type :=
> > nat -> option X.
> >
> > Definition return_ {X : Type} (x : X) : fuelled X :=
> > fun _ => Some x.
> >
> > Definition bind {X : Type} (x : fuelled X)
> >  {Y : Type} (f : X -> fuelled Y) :
> >  fuelled Y :=
> > fun fuel => match x fuel with
> >            | Some x0 => match f x0 fuel with
> >                         | Some y0 => Some y0
> >                         | None => None
> >                         end
> >            | None => None
> >            end.
> >
> > Notation "'do' x0 <- x ; y" := (bind x (fun x0 => y))
> >  (x0 ident, at level 20, right associativity).
> >
> > Definition recursive_call {X:Type} (x : fuelled X) :
> >  fuelled X :=
> > fun fuel => match fuel with
> >            | S fuel_pred => x fuel_pred
> >            | O => None
> >            end.
> >
> > Definition ackermann_fuel : nat -> nat -> fuelled nat :=
> > fix F (m n:nat) (fuel : nat) {struct fuel} : option nat :=
> > match m with
> > | O => return_ (S n)
> > | S m' => match n with
> >          | O => recursive_call (F m' 1)
> >          | S n' =>
> >            do x <- recursive_call (F m n');
> >            recursive_call (F m' x)
> >          end
> > end fuel.
> >
> > Definition run_with_fuel {X:Type} (x : fuelled X)
> >  (fuel : nat) :=
> > x fuel.
> >
> > Compute (run_with_fuel (ackermann_fuel 3 3) 100)
> > --
> > Daniel Schepler