Re: [isabelle] Mistakes in Proving



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.