Re: [isabelle] Approximation tactic for very large numbers



Hi Manuel,

Your concrete example should not be out of reach of the approximation tactic.
On my Mac, I can do e.g., 

lemma "exp (exp 16000 :: real) > 0"
  by (approximation 80)

which proves the goal in about 10s (both in 32 and 64 bit mode).
Therefore I am not sure if it is really the large exponents that pose the problem here.


As a side note on the tactic in general, if you care about performance: In my experience,
you get good results (here about 5s) by setting the precision to about half the precision of the native integer type (i.e., 15 for x86 and 30 for x86_64).

Fabian


> Am 03.03.2018 um 14:25 schrieb Manuel Eberl <eberlm at in.tum.de>:
> 
> Hallo,
> 
> I noticed that the approximation tactic behaves very poorly when the
> input is very large. For instance, attempting to prove "exp (exp 16000
> :: real) > 0" with it results in the tactic running for about a minute
> or two before. The entire Isabelle system becomes unresponsive and
> eventually stops with one of Isabelle/jEdit's "total existence failure"
> messages.
> 
> Now, obviously, I am not expecting the tactic to be able to prove this –
> it uses software floating-point numbers and the exponents here are
> staggeringly large. However, I am wondering if it is possible to make
> the tactic fail gracefully, or at least not take down the entire system.
> Otherwise it is highly problematic to use this tactic as a solver in the
> background, which I intend to do.
> 
> Manuel
> 

Attachment: smime.p7s
Description: S/MIME cryptographic signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.