
Hi,
I have observed that Dafny (maybe, Z3) has some difficulties to prove formulas where existential is involved. But I'm really surprised that Dafny (maybe, Z3) is not able to deal with the basic logical equivalence that relates exists with forall. I mean e.g.
the following assertion.
lemma Test (x:int)
{
assert (!(exists n:int :: x/2 == n )) <==> (forall n:int :: x/2 != n) ;
}
Could someone suggest some hint for this kind of properties?
Thanks,
Paqui


Sep 1, 2014 at 5:15 PM
Edited Sep 1, 2014 at 5:27 PM

Hello Paqui
It can be solved by encapsulate the quantifier body as a predicate. As a result, I think there will be an implicit trigger (i.e. {f(x,n)} ) generated for both quantifier that hints the SMT solver how to instantiate them.
predicate f (x: int, n: int)
{ n== x/2 }
ghost method Test (x:int)
{
assert (forall n:int :: f(x, n)) ==> (!(exists n:int :: !f(x,n)));
}
Three good resources I found that explain the trigger mechanism nicely:
[1] K. Rustan M. Leino. This is Boogie 2.
[2] Johannes Kanig. An Introduction to SMT Solvers.
[3] K. Rustan M. Leino and Rosemary Monahan. Reasoning about Comprehensions with FirstOrder SMT Solvers.
regs,
Zheng



Thank you, very much.
Paqui



Hello Zheng,
I have another strange behaviour with an existential formula.
Please, have a look to the following code.
Have you some explanation/solution?
Paqui
lemma DivBy2Exact (z:int)
requires z >= 2 && z % 2 == 0 ;
ensures exists n:int :: (n>=1 && z == 2*n);
{
calc {
z >= 2 && z % 2 == 0;
==>
z/2 >= 1 && 2*(z/2) == z;
==>
exists n:int :: n>=1 && z == 2*n;
}
}
/* However this does not verifies
lemma Test1 (x:int)
{
calc {
x>=2 && x % 2 == 0 ;
==> { DivBy2Exact(x);}
exists n:int :: (n>=1 && x == 2*n) ;
}
}



It verifies for me with one extra assertion in the calc statement of the DivBy2Exact lemma.
http://rise4fun.com/Dafny/MKK9
lemma DivBy2Exact (z:int)
requires z >= 2 && z % 2 == 0 ;
ensures exists n:int :: (n>=1 && z == 2*n);
{
calc {
z >= 2 && z % 2 == 0;
==>
z/2 >= 1 && 2*(z/2) == z;
==> {assert z/2>=1 && z == 2*(z/2);}
exists n:int :: n>=1 && z == 2*n;
}
}
lemma Test1 (x:int)
{
calc
{
x>=2 && x % 2 == 0 ;
==> { DivBy2Exact(x);}
exists n:int :: (n>=1 && x == 2*n) ;
}
}



There is also another way to do existential quantification by returning values from lemmas. Which may or may not be useful in your situation.
http://rise4fun.com/Dafny/slFK7
lemma DivBy2Exact (z:int) returns (n:int)
requires z >= 2 && z % 2 == 0 ;
ensures (n>=1 && z == 2*n);
{
n := z/2;
}
lemma Test1 (x:int)
{
assert (x>=2 && x % 2 == 0) ==> exists n :: (n>=1 && x == 2*n);
}



Hello Paqui,
Sorry, I am not sure. My understanding is that we give Dafny a harder subproblem (i.e. the intermediate calculation [z/2 >= 1 && 2*(z/2) == z] ) to prove, but the original problem can be solve without it.
Regards,
Zheng



Hi,
Many thanks for all the hints on dealing with existential quantifiers.
But I'm still wondering why the lemma
lemma DivBy2Exact (z:int)
requires z >= 2 && z % 2 == 0 ;
ensures exists n:int :: (n>=1 && z == 2*n);
{
calc {
z >= 2 && z % 2 == 0;
==>
z/2 >= 1 && 2*(z/2) == z;
==>
exists n:int :: n>=1 && z == 2*n;
}
}
(statically) verifies, but itself doesn't verify when we add another lemma:
lemma Test1 (x:int)
{
calc {
x>=2 && x % 2 == 0 ;
==> { DivBy2Exact(x);}
exists n:int :: (n>=1 && x == 2*n) ;
}
}
This seems rare in static verification, doesn't it?
Best,
Paqui



Could be some kind of bug? Seems strange to me too.
This does not verify:
http://rise4fun.com/Dafny/ea8t
lemma DivBy2Exact (z:int)
requires z >= 2 && z % 2 == 0 ;
ensures exists n:int :: (n>=1 && z == 2*n);
{
calc {
z >= 2 && z % 2 == 0;
==>
z/2 >= 1 && 2*(z/2) == z;
==>
exists n:int :: n>=1 && z == 2*n;
}
}
lemma X(x:int)
But this does:
http://rise4fun.com/Dafny/sl3Sr
lemma DivBy2Exact (z:int)
requires z >= 2 && z % 2 == 0 ;
ensures exists n:int :: (n>=1 && z == 2*n);
{
calc {
z >= 2 && z % 2 == 0;
==>
z/2 >= 1 && 2*(z/2) == z;
==>
exists n:int :: n>=1 && z == 2*n;
}
}

