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



On 10/12/13 05:36, Makarius wrote:
> 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
>

Ah, that helps explains why this suddenly came up when I couldn't see
any relevant changes to "blast" itself in the Isabelle2013/Isabele2013-1
diff.

> 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.

When I use the word "bug", I tend to mean a behaviour of a computer
program that is unexpected, unintended and undesirable. There is
certainly subjectivity in whether particular behaviours are unexpected,
unintended and/or undesirable, but that doesn't make the word "bug"
meaningless.

> 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.

Indeed it is funny. I would even go so far as to say it is unexpected,
unintended and undesirable.

> 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?

Thanks for the suggestion.

I will make the change and see how it affects all the top-secret proofs
available in the dark cellars around here and report back.

Cheers,
David


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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