*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Mistakes in Proving*From*: miramirkhani at ce.sharif.edu*Date*: Sun, 17 Oct 2010 12:51:56 +0330 (IRST)*Cc*: Lukas Bulwahn <bulwahn at in.tum.de>, miramirkhani at ce.sharif.edu, Viorel Preoteasa <viorel.preoteasa at abo.fi>*Importance*: Normal*In-reply-to*: <1287056331.1934.15.camel@bool>*References*: <39157.188.136.139.90.1287000445.squirrel@ce.sharif.edu> <4CB617E7.6050506@in.tum.de> <1287056331.1934.15.camel@bool>*User-agent*: SquirrelMail/1.4.9a

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 >> > >> > >> > >> > >> > >> > >> > > > >

**References**:**[isabelle] Mistakes in Proving***From:*miramirkhani

**Re: [isabelle] Mistakes in Proving***From:*Lukas Bulwahn

**Re: [isabelle] Mistakes in Proving***From:*Viorel Preoteasa

- Previous by Date: [isabelle] Postdoc and PhD Studentship: Automatic Proof Procedures with Engineering Applications
- Next by Date: [isabelle] Minor type-setting mistake in http://isabelle.in.tum.de/dist/Isabelle/doc/sugar.pdf
- Previous by Thread: Re: [isabelle] Mistakes in Proving
- Next by Thread: Re: [isabelle] Mistakes in Proving
- Cl-isabelle-users October 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list