[isabelle-dev] A suggestion: call eval with try0

[Manuel Eberl]

Yes, that's called code_simp.

The difference, however, is often several orders of magnitude, which
makes code_simp unfeasible in most cases.

I always wondered /why/ it is that slow and whether this is just not
optimised that well or whether it's some unavoidable bottleneck.

Manuel


On 17/08/2020 13:30, lammich at in.tum.de wrote:
> Hi
> Isn't there a (slower) possibility to Eval via the simplifier?
> 
> Peter
> 
> 
> -------- Original Message --------
> Subject: Re: [isabelle-dev] A suggestion: call eval with try0
> From: Jasmin Blanchette <j.c.blanchette at vu.nl>
> To: "Dr A. Koutsoukou-Argyraki" <ak2110 at cam.ac.uk>
> CC: Isabelle-dev list <isabelle-dev at mailbroy.informatik.tu-muenchen.de>
> 
> 
>     Dear Angeliki,
> 
>     > eval is not one of the many methods called by try0, and to my
>     experience so far Sledgehammer doesn't suggest it either.
>     > I've noticed several very simple proofs that work just "by eval"
>     and yet automation won't suggest any proof.
>     >
>     > Do people agree that it would be practical to include eval in the
>     methods tried with try0?
>     >
>     > and would this be feasible ?
> 
>     Technically, this would be very feasible. The question is more
>     whether it's desirable to have "try0" and Sledgehammer suggest
>     tactics that bypass the LCF-style kernel and its strong guarantees.
>     These are not just "academic" worries. Just a few years ago, there
>     was a debilitating bug in "eval" that made it succeed every time,
>     even if your conjuecture was literally "False". (I can't find it in
>     "NEWS", but I vividly remember the discussion on the mailing list.)
> 
>     Maybe a mention "(oracle)" next to "eval" would be enough? If it's
>     clear enough that "eval" doesn't have the same status as the other
>     tactics, I wouldn't mind enhancing "try0" in this way. Many users
>     who rely on "try0" are novices that learn Isabelle and its tactics
>     partly through "try0".
> 
>     Cheers,
> 
>     Jasmin
> 
>     P.S. I believe your email might interest other users of Isabelle.
>     You might not reach them by writing to isabelle-dev.
> 
>     _______________________________________________
>     isabelle-dev mailing list
>     isabelle-dev at in.tum.de
>     https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
>