Re: [isabelle] Mistakes in Proving



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

On 10/13/2010 10:07 PM, miramirkhani at ce.sharif.edu wrote:
Dear All,

I want to prove a simple theorem. The proof seems to be straightforward
but I can’t figure out the mistakes I’m 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.

1. [iff] "P(x) ->  f(x) \<in>  g(x)"

2. [iff]"P(x)->  ( f(x) \<in>  r(g((x)) )"

3. "y \<in>  r(g(z)) =>  y \<in>  h(w)"

4. "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….”.

What’s wrong with my proof?

Any hints would be of a great help to me

--
Kind Regards
Najma












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