Re: [isabelle] Mistakes in Proving



Thanks so much to Lukas and Viorel for their help. According to the
Viorel?s 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.

--
Kind Regards
Najma

> 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
>
>
>
> On Wed, 2010-10-13 at 22:34 +0200, Lukas Bulwahn wrote:
>> 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.