Negation of existential formulas

Sep 1, 2014 at 3:20 PM
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 4:15 PM
Edited Sep 1, 2014 at 4: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 First-Order SMT Solvers.

regs,
Zheng
Marked as answer by rustanleino on 9/9/2014 at 4:11 PM
Sep 1, 2014 at 4:46 PM
Thank you, very much.
Paqui
Sep 3, 2014 at 2:12 PM
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) ;
     }
}
Sep 3, 2014 at 3:53 PM
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) ;
     }
}
Sep 3, 2014 at 8:20 PM
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);
}
Sep 4, 2014 at 2:56 PM
Hello Paqui,

Sorry, I am not sure. My understanding is that we give Dafny a harder sub-problem (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
Sep 11, 2014 at 11:48 AM
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
Sep 15, 2014 at 9:07 PM
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; 
     }
}