From: "Dr A. Koutsoukou-Argyraki" <ak2110@cam.ac.uk>
Dear all,
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 ?
Best wishes,
Angeliki
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: Jasmin Blanchette <j.c.blanchette@vu.nl>
Dear Angeliki,
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@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: "lammich@in.tum.de" <lammich@in.tum.de>
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: Manuel Eberl <eberlm@in.tum.de>
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
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: "lammich@in.tum.de" <lammich@in.tum.de>
isabelle-dev mailing list
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
There is e.g. no proper counter part for abstract data types. Nowadays
I would not consider code_simp a serious business any longer.
Btw. this discussion would fit in scope to the Isabelle user mailing list.
Cheers,
Florian
signature.asc
Last updated: Oct 12 2024 at 20:18 UTC