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 [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
