Re: [isabelle] Auto and set ordering -- unpredictable?



Hi John,

I tried this example with "trace simplifier" enabled, and it reveals
what the problem is. Here is the first part of the tracing output:

[1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
⟦f i1 = 1; f i2 = 2; Set = {i1, i2}⟧ ⟹ {i2} = {x ∈ {i1, i2}. f x = 2}

[1]Adding rewrite rule "??.unknown":
f i2 ≡ 2

[1]Adding rewrite rule "??.unknown":
{i1, i2} ≡ Set

Note the orientation of the rule in the last line.

Usually, when you have an assumption of the form "lhs = rhs", the
simplifier will add the rewrite rule "lhs == rhs" to the local
simpset. But depending on some heuristic, the simplifier may decide to
add the rewrite "rhs == lhs", or even "(lhs = rhs) == True" instead. I
have seen this behavior before in situations where the rule "lhs ==
rhs" would obviously loop, so it only makes sense to use the opposite
orientation. "(lhs = rhs) == True" is used when either orientation
would obviously loop.

Apparently the heuristic also reorients rules like "Set = {i1, i2}",
where the lhs is a top-level constant. Usually this reorientation
makes sense (for example, with the assumption "[] = xs", it is better
to replace each occurrence of "xs" with "[]" than vice-versa) since
for most top-level constants, there will be further applicable simp
rules in the simpset.

Note that the heuristic does not apply to locally-fixed variables. So
the following proof works:

lemma
  fixes f :: "nat => nat" and Set :: "nat set" and i1 :: nat and i2 :: nat
  assumes f1 : "f i1 = 1" and f2 : "f i2 = 2" and s1 : "Set = {i1, i2}"
  shows "{i2} = {x : {i1, i2}. f x = 2}"
using f1 f2 s1
by auto

I expect that if you changed your axiomatization to a locale, the
reorientation would similarly go away.

Also, if you use "simp add" instead of "using", the reorientation does
not happen:

lemma "{i2} = {x : {i1, i2}. f x = 2}"
by (auto simp add: f1 f2 s1)

- Brian

On Tue, Feb 1, 2011 at 2:25 PM,  <munddr at gmail.com> wrote:
> Hi,
>
> I'm trying to prove a very simple lemma in the following simple example:
>
> axiomatization
> f :: "nat => nat" and
> Set :: "nat set" and
> i1 :: nat and
> i2 :: nat
> where
> f1 : "f i1 = 1" and
> f2 : "f i2 = 2" and
> s1 : "Set = {i1,i2}"
>
> lemma "{i2} = {x : {i2,i1}. fx = 2}"
> using f1 f2 s1
> by auto
>
> It works and I know s1 is redundant here. Now, let's try:
>
> lemma "{i2} = {x : {i1,i2}. fx = 2}"
> using f1 f2 s1
> by auto
>
> Auto doesn't work. However, if s1 was removed, it works. So how come using
> the redundant fact "s1" requires the set to be ordered in a particular way?
> It doesn't seem intuitive.
>
> Help will be appreciated!
>
> Thanks
> John
>





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.