Email Gateway (Aug 18 2022 at 17:08): Email Gateway (Aug 18 2022 at 17:08):From: munddr@gmail.com
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
Email Gateway (Aug 18 2022 at 17:08):From: Brian Huffman <brianh@cs.pdx.edu>
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)
Last updated: Apr 24 2024 at 04:17 UTC