[isabelle-dev] Safe approach to hypothesis substitution
Thomas.Sewell at nicta.com.au
Mon Aug 23 09:52:56 CEST 2010
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.
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the isabelle-dev