The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

We have a bit of discussion on avoiding evaluation of such
propositions in section 4.4. of our paper on real number computation
here.
A trick is to wrap it in a /-abstraction. We observe that this would
not be needed if Coq evaluated propositions lazily.

Type classes for efficient exact real arithmetic in Coq
Robbert Krebbers, Bas Spitters
https://arxiv.org/abs/1106.3448
On Thu, Nov 1, 2018 at 5:13 PM Peter E Schmidt-Nielsen 
<snp AT mit.edu>
 wrote:
>
> 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.
> >>
> >>
> >>
> >
> >