Email Gateway (Aug 18 2022 at 16:13): Email Gateway (Aug 18 2022 at 16:13):From: miramirkhani@ce.sharif.edu
Dear All,
I want to prove a simple theorem. The proof seems to be straightforward
but I cant figure out the mistakes Im making.
The first three lemmas bellow are proved and I want to prove the 4th
lemma. P is a predicate and f,g,h and r are functions.
[iff] "P(x) -> f(x) \<in> g(x)"
[iff]"P(x)-> ( f(x) \<in> r(g((x)) )"
"y \<in> r(g(z)) => y \<in> h(w)"
"P(x) -> f(x) \<in> h(w)"
I give the first two to the simplifier by using the iff attribute, then I
add the 3rd lemma to the simplification rules and use the simp method but
it fails and I get :
Empty result sequence
..
Whats wrong with my proof?
Any hints would be of a great help to me
Email Gateway (Aug 18 2022 at 16:13):From: Lukas Bulwahn <bulwahn@in.tum.de>
Hello Najma,
I copied your lemmas to Isabelle, corrected the syntax and used the
counterexample generators refute and nitpick (based on SAT solving
technology) to find an counterexample why the fourth does not follow
from the first three:
lemma
assumes "P x --> f x \<in> g x"
assumes "P x --> f x \<in> r (g x)"
assumes "y \<in> r(g z) --> y \<in> h w"
shows "P x --> f x \<in> h w"
refute
nitpick[show_consts]
Both tools output a model that show that you cannot derive the fourth
from the first three in general.
refute says:
* Model found: *
Size of types: 'a: 2, 'b: 1, 'c: 1
w: c0
h: {(c0, {(b0, False)})}
y: b0
z: a0
r: {({(b0, True)}, {(b0, True)}), ({(b0, False)}, {(b0, False)})}
f: {(a0, b0), (a1, b0)}
g: {(a0, {(b0, False)}), (a1, {(b0, True)})}
x: a1
P: {(a0, False), (a1, True)}
and nitpick says:
Nitpick found a counterexample for card 'a = 2, card 'b = 2, and card 'c
= 2:
Constants:
P = {a1, a2?}
f = (%x. _)(a1 := b1)
g = (%x. _)(a1 := {b1}, a2 := {})
h = (%x. _)(c1 := {b2?}, c2 := ?)
r = (%x. _)({b1, b2} := ?, {b1} := {b1, b2?}, {b2} := ?, {} := {b1?})
w = c1
x = a1
y = b2
z = a2
But just try it yourself...
So in your case, you are either trying to prove something that does not
hold (the counterexample should give you a hint why not) or
the proof is really dependent on the definitions of the functions f,
g,h,r and predicate P.
I hope this helps.
Lukas
Email Gateway (Aug 18 2022 at 16:13):From: Viorel Preoteasa <viorel.preoteasa@abo.fi>
Hello Najma, Lukas,
It seems that Lukas' counter example is for a different problem
than the original one.
It is important what are constants and what are variables in
the original lemmas of Najma. If P, f, g, r and h are constants,
and all other are variables, than lemma 4 is provable using lemmas
2 and 3.
consts
f1 :: "'a => 'b"
g1 :: "'a => 'b set"
r1 :: "'b set => 'b set"
h1 :: "'c => 'b set"
P1 :: "'a => bool";
lemma B1: "P1(x) ==> ( f1(x) \<in> r1(g1((x)) ))";
sorry;
lemma C1: "y \<in> r1(g1(z)) ==> y \<in> h1(w)";
sorry;
lemma "P1(x) ==> f1(x) \<in> h1(w)"
apply (rule C1);
apply (rule B1);
by simp;
Automating this proof is a different problem that I don't know how
to answer.
Best regards,
Viorel
Email Gateway (Aug 18 2022 at 16:13):From: Lars Noschinski <noschinl@in.tum.de>
In this case it would by solved "by (auto intro: B1 C1).
Email Gateway (Aug 18 2022 at 16:14):From: Lars Noschinski <noschinl@in.tum.de>
The simplifier can only make use of the third lemma if it can prove its
precondition to be true (to see why it cannot solve this, you can look
at the simplifier's trace). As the third lemma is not an equation, you
are better off using it as an introduction rule (using the rule method
or e.g. the intro: option of auto).
Email Gateway (Aug 18 2022 at 16:14):From: miramirkhani@ce.sharif.edu
Thanks so much to Lukas and Viorel for their help. According to the
Viorels post, the lemma could be proved easily but my first two lemmas
use longrightarrow (-->) instead of Longrightarrow( ==>)and that was the
point that made me confused about the proof and I thought it should be
proved. So using refute I got a counter example.
Last updated: Nov 21 2024 at 12:39 UTC