[isabelle-dev] Safe approach to hypothesis substitution

[Thomas Sewell]

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.

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.

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.

________________________________________
From: Alexander Krauss [krauss at in.tum.de]
Sent: Monday, August 23, 2010 7:35 PM
To: Thomas Sewell
Cc: Isabelle Developers Mailing List
Subject: Re: [isabelle-dev] Safe approach to hypothesis substitution

Hi Thomas,

Thanks for digging into this. The concrete patch is exactly what was
needed to advance this discussion. Here are a few comments. I am sure
others will have more...

> 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.

So it is painful (as there are a much more theories out there), but it
may work, and it may be worth the trouble in the long run.

> 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.

Do I understand correctly that substituting the hypothesis is safe, but
discarding them afterwards is unsafe? Then, why should they not be used?

More importantly, why is it safe to use and discard an equality when the
variable occurs elsewhere in the goal? The equality itself could
interact with a fact from the context? Consider the contrived example

locale l =
   fixes x :: nat
   assumes neq: "x ~= 0"
begin

lemma "x = 0 ==> x <= x + 1 ==> False"
apply safe

After "safe", the lemma becomes unprovable, since the hypothesis that
contradicts the context is removed. It seems that your patch does not
fix this... (I haven't tried... just guessing from reading the code)


[...]

A few concrete remarks concerning the patch (which seems to be relative
to Isabelle2009-2):


> diff -r 2e1b6a8a0fdd src/HOL/Parity.thy
> --- a/src/HOL/Parity.thy      Wed Jul 28 06:38:17 2010 +1000
> +++ b/src/HOL/Parity.thy      Mon Aug 23 17:33:59 2010 +1000
> @@ -66,9 +66,10 @@
>    by presburger
>
>  lemma even_times_anything: "even (x::int) ==> even (x * y)"
> -  by algebra
> +  by (simp add: int_even_iff_2_dvd)
>
> -lemma anything_times_even: "even (y::int) ==> even (x * y)" by algebra
> +lemma anything_times_even: "even (y::int) ==> even (x * y)"
> +  by (simp add: int_even_iff_2_dvd)
>
>  lemma odd_times_odd: "odd (x::int) ==> odd y ==> odd (x * y)"
>    by (simp add: even_def zmod_zmult1_eq)

?!? Why is the behaviour of the "algebra" method changed?

> diff -r 2e1b6a8a0fdd src/Provers/hypsubst.ML
> --- a/src/Provers/hypsubst.ML Wed Jul 28 06:38:17 2010 +1000
> +++ b/src/Provers/hypsubst.ML Mon Aug 23 17:33:59 2010 +1000

> +(* Counts the occurences of Free and Bound variables in a term. *)
> +fun count_vars' _ (Free f) = Termtab.map_default (Free f, 0) (fn x => x + 1)
> +  | count_vars' _ (Var _) = I
> +  | count_vars' _ (Const _) = I
> +  | count_vars' n (Bound m) = Termtab.map_default (Bound (m - n), 0)
> +      (fn x => x + 1)
> +  | count_vars' n (Abs (_, _, t)) = count_vars' (n + 1) t
> +  | count_vars' n (f $ x) = count_vars' n f o count_vars' n x
> +
> +fun count_vars ts = fold (count_vars' 0) ts Termtab.empty

This is very strange, since it counts the bound variables in
"(%f. f) (%x. x)" as the same variable. It doesn't seem to produce a
problem now, since the variables in a hypothesis are goal parameters,
which are nested linearly, but it is confusing nevertheless.

> +
> +(* An equality hypothesis 'x = y' is trivial if substituting with it would have
> +   no useful effect. The principal test for this is if x or y is a unique
> +   variable, occuring nowhere else in the goal.  The exception to the rule is
> +   if x is bound and y is unique but free. *)

What is a "useful effect"? This is not a rhetorical question -- I really
don't understand. Is the second sentence the actual definition?

A more general remark:
Larry's comments in hypsubst.ML:
> (*If novars then we forbid Vars in the equality.
>   If bnd then we only look for Bound variables to eliminate.
>   When can we safely delete the equality?
>     Not if it equates two constants; consider 0=1.
>     Not if it resembles x=t[x], since substitution does not eliminate x.
>     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
>     Not if it involves a variable free in the premises,
>         but we can't check for this -- hence bnd and bound_hyp_subst_tac

The last point really indicates the main problem: "the premises" are
actually facts in the surrounding context. In other words, it is almost
never safe to eliminate Frees, unless we know for some reason that all
relevant facts have already been inserted in the goal...

So it seems the only really conservative step is to eliminate bound
variables only??? How many proofs would have to be fixed if "safe
methods" were restricted to this? I gues it's a lot more, but it may
still be better than trading one heuristic for a more complex one, which
is still unsafe...

Alex


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.