Re: [isabelle] "blast" eliminates unrelated flex-flex pairs in Isabelle2013-1 and Isabelle2013-2.



On Mon, 9 Dec 2013, Lawrence Paulson wrote:

If you get these constraints in a proof, even if it currently works, it might be a good idea to look for a different proof (by explicitly instantiating a variable that is currently left uninstantiated) to get rid of them yourself.

It is definitely a good idea to avoid relying on such boundary situations, like pending flex-flex pairs, back tracking after 'apply' etc.


Anyway, the reason why blast works slightly differently in Isabelle2013-2 (and the obsolete Isabelle2013-1) is this detail from the NEWS:

  * SELECT_GOAL now retains the syntactic context of the overall goal
  state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
  situations.

The change to SELECT_GOAL (210bca64b894) ensures that the goal context is preserved more rigorously, with add-on information like maxidxs, flex-flex pairs etc. That was the very purpose of the change, in order to prevent other oddities from the following mailing list threads about "SELECT_GOAL and schematic variables":

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00118.html
http://www.mail-archive.com/isabelle-dev at mailbroy.informatik.tu-muenchen.de/msg04268.html

Note that in these threads there was never any talk about "bugs" nor "fixes" -- the notoriously meaningless words. The NEWS entry correctly anticipates some "potential INCOMPATIBILITY", although I did not know about this particular case when writing that piece of text.


It is funny that blast smashes flex-flex pairs in the first place, and thus affects the overall goal state, not just the subgoal where it is applied.

That detail goes back to Isabelle/93a84eb6c522 from 02-Jan-1998, where Larry writes in the log entry "Blast_tac now squashes flex-flex pairs immediately", but it is unclear why. Maybe Larry remembers why he was smashing flex-flex pairs on purpose 15 years ago.

Trying without, i.e. removing the following line http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-2/src/Provers/blast.ML#l1261 shows that there is no change in the success of the immediately reachable universe of Isabelle + AFP examples.

Maybe there is a different impact on top-secret proofs that are locked-up in some cellar like the Lost Ark in some Indiana Jones movie, but who knows?


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.