The Coq mailing list

[Peter E Schmidt-Nielsen <snp AT mit.edu>]

Using a fuel quantity seems like a reasonable solution whenever you can 
easily produce a default value when you run out of fuel. Here's an example 
of performing this transformation generically on a recursive function, 
using a nat to track the fuel:

https://gist.github.com/petersn/361c40b3394a3ad9721b738ac61d48b1

Of course, if we switched to using a binary number for the fuel then we 
could trivially just pass in 2^300 for the fuel and get a definition which 
won't run out of fuel before the heat death of the universe.

However, some library theorems (N.lt_pred_l and N.lt_wf_0) are opaque, 
blocking the binary version in the above gist from computing. I'm 
wondering if anyone more experienced here knows if there're some 
transparent versions elsewhere I don't know about, or if I'm missing 
something silly?

-snp

On Thu, 1 Nov 2018, Klaus Ostermann wrote:

> It's maybe not particularly elegant or sophisticated, but what about
> just adding "fuel" as an additional argument
> and initializing with a sufficient amout of fuel?
>
> Klaus
>
>
> Am 01.11.18 um 12:21 schrieb Thorsten Altenkirch:
> > Is there a way to run possibly non-terminating programs in the coq
> > type checker. In Agda you can just switch off the termination checker.
> >
> >  
> >
> > I think this is useful if you want to use something whose termination
> > you haven't yet proven but want to exploit reduction.
> >
> >  
> >
> > Hence it is not enough to add the assumption that it terminates as an
> > axiom because this won't reduce. 
> >
> > Thorsten
> >
> > This message and any attachment are intended solely for the addressee
> > and may contain confidential information. If you have received this
> > message in error, please contact the sender and delete the email and
> > attachment.
> >
> > Any views or opinions expressed by the author of this email do not
> > necessarily reflect the views of the University of Nottingham. Email
> > communications with the University of Nottingham may be monitored
> > where permitted by law.