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 [l...@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@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.
_______________________________________________
Isabelle-dev mailing list
Isabelle-dev@mailbroy.informatik.tu-muenchen.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
