[isabelle-dev] FW: Safe approach to hypothesis substitution

[Thomas Sewell]

Let me try to explain the difference from the perspective of a user. There are three classical tools that will behave differently: safe, clarify and clarsimp. Each of these will, when it would have substituted and removed equalities in the past, now substitute those equalities, possibly reorient them, and leave them as hypotheses.

The additional equality will then be seen at all later points throughout tactic proofs. Given the ubiquity of clarsimp in my work, I suspect this changes the subgoal state at a significant number of points. The additional hypothesis will have little impact on most tools, but there are three kinds of tactic step with which it is a problem:
  1) Subgoals where a bound variable (typically 'x' or 'y') is renamed (to 'xa' or 'ya') because facts about x or y persist in the goal. This means that explicit instantiations in subgoal_tac etc may need to be updated.
  2) Explicit use of a drule or erule which can unify with an equality hypothesis (drule sym, drule_tac f=... in arg_cong, etc).
  3) Induction steps, where additional hypotheses complicate the induction hypothesis generated.

The changes to the HOL sources in the patch I sent reflect these three issues. None of these issues seem to be common, but maintainers of large repositories (HOL, the AFP, L4.verified etc) may still find them inconvenient.

The main advantage of the preserving an equality on a free variable is if that variable is reintroduced via facts from the context at a later point in the proof script. I think this is unlikely to occur in a terminal tactic (auto, blast, fastsimp, etc) and thus they are unlikely to benefit from the change. For this reason I added an unsafe wrapper which simulated the old behaviour. I haven't tested whether this was really necessary. I may do that tomorrow.

Yours,
    Thomas.

________________________________________
From: Lawrence Paulson [lp15 at cam.ac.uk]
Sent: Tuesday, August 31, 2010 8:21 PM
To: Thomas Sewell
Cc: Isabelle Developers Mailing List
Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution

Thanks for looking into this problem, which has been around in one way or another from the very beginning.

Lost in all the technical discussions is the question of what the user will see. We have the option of leaving blast and force as they are now to minimise danger of incompatibility, though it would be disappointing if existing calls to these stopped working after what should be an improvement. I would expect them, on the contrary, to solve more problems than before. Anyway, the main methods to be affected are presumably safe and auto.

I have made a small table showing the number of times the classical proof methods are used in the HOL distribution:

safe    956
auto    23389
clarify 1403
force   1692
fastsimp 560
blast   7609
fast    1079
best    43

If the only method that behaves differently is safe, I wonder whether there's any point to doing this. It would be better to improve all the methods. If the new version is identical to the old one except that occasionally some equalities persist, then it ought to work as a drop-in replacement in nearly every instance. Is this what you see?

Larry

On 23 Aug 2010, at 08:52, Thomas Sewell wrote:

> As previously discussed in the thread "Safe for boolean equality", the current strategy for using equality hypotheses 'x = expr', in which substitution for x is done and then the hypothesis is discarded, is unsafe. The conclusion of that discussion was that the problem was annoying but fairly rare, that there is some concern it may become more common as local are used more extensively, and that fixing it would probably require a painful change to the behaviour of auto.
>
> The problem is that by forgetting what x equates to in our goal, we lose the connection from the goal to the context outside our goal. There may be other facts available that name x. There may also be schematic variables which could be instantiated to "hd x" but not the bound variable replacing it.
>
> The simple solution in my mind is to keep the equality in the goal, and since noone else seemed interested I thought I'd attempt to do this myself and see how difficult it was. I attach the resulting patch. After several rounds of bugfixes and compatibility improvements, it requires 23 lines of changes to theories to rebuild HOL, HOL-ex and HOL-Word.
>
> The code change in Provers/hypsubst.ML adds code for counting the free and bound variables in a goal, and checking whether either side of an equality hypothesis is a unique variable, occuring nowhere else. The main substitution algorithms avoid using such equalities and also preserve rather than delete the hypothesis they select. There is a new tactic for discarding these equalities, which is added as an unsafe wrapper in Context_Rules, allowing all unsafe tactics to behave roughly as before. The version of hypsubst called by blast is left unchanged, as blast proofs seem to be highly sensitive to changes. There is plenty of room for optimisation, I tried to keep the diff readable.
>
> Three kinds of proofs seem to need fixing:
>  1. proofs where subgoal_tac or similar now needs to refer to xa rather than x.
>  2. proofs where erule ssubst, drule sym/arg_cong/fun_cong etc need to be further specialised.
>  3. proofs where variables are eliminated and then induction is performed, i.e. the word library. Explicitly adding "apply hypsubst_thin" seems the best solution.
>
> At this stage I'm not sure how to proceed. I would be very happy to see safe get safer, but I'm not sure how acceptable this level of incompatibility is in an Isabelle change. There's an alternative approach I thought of recently but haven't tried yet - replacing used equalities with meta-equalities - which might reduce the incompatibilities of type 2.
>
> I haven't checked whether there are any performance implications.
>
> I'd be keen to hear what other Isabelle developers think.
>
> Yours,
>    Thomas.
>
>
> <hypsubst-diff.txt>_______________________________________________
> Isabelle-dev mailing list
> Isabelle-dev at mailbroy.informatik.tu-muenchen.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


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.