[isabelle-dev] Safe approach to hypothesis substitution

[Lawrence Paulson]

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