Stream: Mirror: Isabelle Development Mailing List

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


view this post on Zulip Email Gateway (Aug 15 2020 at 13:57):

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

view this post on Zulip Email Gateway (Aug 17 2020 at 10:36):

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

view this post on Zulip Email Gateway (Aug 17 2020 at 11:30):

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

view this post on Zulip Email Gateway (Aug 17 2020 at 11:40):

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

view this post on Zulip Email Gateway (Aug 17 2020 at 12:04):

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

view this post on Zulip Email Gateway (Aug 17 2020 at 17:28):

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: Mar 04 2024 at 10:08 UTC