[isabelle-dev] Safe approach to hypothesis substitution

[Andreas Schropp]

On 08/23/2010 12:30 PM, Thomas Sewell wrote:
> Hello again isabelle-dev.
>
> I should clear up some confusion that may have been caused by my mail. I was trying to avoid repeating all that had been said on this issue, and it seems I left out some that hadn't been said as well.
>
> This approach avoids ever deleting an equality on a Free variable during a 'safe' reasoning step. It will substitute with that equality but keep it in place. This is a significant change to the intermediate state of some tactic scripts, thus the incompatibilities, especially on induction. It is somewhat surprising there aren't more such incompatibilities. There's no truly safe way to delete an equality on a Free variable without inspecting the whole context.
>    

Naive questions:
   * why is inspecting the whole context infeasible?
   * why can't we just collect (and cache?) the Frees occuring in 
assumptions managed
     by assumption.ML and never delete equalities involving them?

> Since equalities are not deleted, care must be taken to avoid an infinite loop in which a substitution is repeatedly attempted. This is the reason for the uniqueness check - if x appears only in 'x = expr' then there is no more substitution to be done. Some subtleties were discovered experimentally:
>    - 'x = y' should not be substituted if either x or y is unique, or else we enter a loop substituting x ->  y ->  x
>    - 'expr = x' needs to be reoriented when it is substituted, or else hypsubst and simp will loop doing opposite substitutions.
>    - 'x = y' is OK to substitute if y is a unique free and x is a non-unique Bound.
>
> This is what is meant by a 'useful' substitution in the comment. Other equalities, which would cause a no-effect or cyclic substitution, are referred to as trivial (abbreviated triv) in this code. The language should probably be cleanup up to use a consistent set of names.
>    

Sounds complicated, but cool.

You adapted blast_hyp_subst_tac in that way too, right?
The subtlety here is that blast tries to approximate the effect of that 
tactic
in the search and has accuracy problems even now. The more complicated
the substitution criterion, the more weirdness is induced here.

With the current situation before the patch, the accuracy problems can be
fully repaired it seems; what works best for blast is a simple criterion of
substitutability which is decidable from the hyp (and possibly 
information that
stays constant in the whole search) only.


> Let me address Alex's detailed comments:
>
> 1. In the HOL sources the algebra method is used to solve two problems about parity essentially by accident. No Groebner bases were involved, but the surrouding logic, which appeals to clarify_tac and a custom simpset, happened to solve the goal. With this change the simplified goal had an extra quantifier in it. Note that with this change terminal tactics operating in 'unsafe' mode - fast, best, etc - will call thin_triv_tac via Context_Rules and behave similarly to before. It is terminal tactics which take safe steps - like algebra - that are most likely to break.
>
> 2. Yes, count vars is a bit strange, as it will consider "(%f. f) (%x. x)" to contain two copies of Bound -1. The point is to count loose Bounds in the hypotheses as returned by Logic.strip_assums_hyp, which it gets right.
>
> Yours,
>      Thomas.
>