Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Proving equivalence


view this post on Zulip Email Gateway (Aug 18 2022 at 16:49):

From: Steve W <s.wong.731@gmail.com>
Hi all,

I'm having problem proving the following. Say I have:

axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real"
where ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"

lemma "ALL p r v e. bax r e = bar p e"
using ax1
by auto

The lemma can be proved. However, if I change the signature of bax to "real
=> real => real => real":

axiomatization
foo :: "real => real => real" and
bar :: "real => real => real" and
bax :: "real => real => real => real"
where ax2: "ALL q p r v e. (r = foo p e & v = bar p e) = (bax q r e = v)"

lemma "ALL q p r v e. bax q r e = bar p e"
using ax2
by auto

Auto can't find a proof. How come this is so difficult for auto? What is the
proper way to do this proof?

Thanks

Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 16:49):

From: Tjark Weber <webertj@in.tum.de>
Steve,

both "by blast" and "by metis" succeed. I didn't investigate why auto
fails.

Kind regards,
Tjark

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: Brian Huffman <brianh@cs.pdx.edu>
Hi Steve,

As Tjark pointed out recently, axioms are evil. It just so happens
that both of your example axiomatizations are inconsistent. As you can
see:

lemma "(0::real) = 1"
using ax1 by metis

(The same proof works also for ax2.)

This might explain why metis can easily solve your lemma: because from
ax1 or ax2 metis can prove any equation between real numbers!

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: s.wong.731@gmail.com
Hi,

Thanks for pointing out the inconsistency. Just curious, how could you
could spot the inconsistency? How could "(0::real) = 1" be derived from
that axiom?

Thanks again

Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: s.wong.731@gmail.com
Actually, proving "(0::real) = 1" using that as a fact doesn't make it
inconsistent, right? It just means that it has at least one unsatisfying
model.

Steve

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: Brian Huffman <brianh@cs.pdx.edu>
Start with your axiom:

ax1: "ALL p r v e. (r = foo p e & v = bar p e) = (bax r e = v)"

Now instantiate "v" to "bax r e":

"ALL p r e. (r = foo p e & bax r e = bar p e) = (bax r e = bax r e)"

Simplify:

"ALL p r e. (r = foo p e & bax r e = bar p e) = True"
"ALL p r e. r = foo p e & bax r e = bar p e"

Take the first conjunct:

"ALL p r e. r = foo p e"

This states that all real numbers "r" are equal to the same value "foo
p e", which is obviously inconsistent.

view this post on Zulip Email Gateway (Aug 18 2022 at 16:50):

From: Brian Huffman <brianh@cs.pdx.edu>
If "False" can be derived as a theorem from some set of axioms, then
any proposition can be derived as a theorem, and so by definition that
set of axioms is inconsistent.

Note that my proof of "(0::real) = 1" from ax1 did not rely on any
extra assumptions about the constants "foo", "bar", etc. so the proof
applies to all potential models.


Last updated: Mar 29 2024 at 08:18 UTC