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

[Jasmin Blanchette]

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.