1

I have read the very helpful (Dafny: What does no terms found to trigger on mean?) but can any one tell me how to prove the two assertions marked with /**/.

Not even sure if they can be proven. The logically equivalent assertions with the defined function inters are proven and may be that is as far as you can go. Any insight greatly appreciated.

    function inters(a:set<int>, b:set<int>): set<int> {a*b}
method pingo(a:set<int>, b:set<int>) 
  {     
     assert  (forall x:int  :: (x !in inters(a , b) ) <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in  a*b)           <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in inters(a , b) )) <==> 
             (forall x:int  :: (x in a ==> x!in b ));
/**/ assert  (forall x:int  :: (x !in  a*b))        <==> 
             (forall x:int  :: (x in a ==> x!in b ));
     
     assert  ((a*b) == {}) <==> (forall x:int  ::(x in a ==> x!in b )) ;
     assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  inters(a , b) ));
/**/ assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  a*b )) ;
 }
david streader
  • 589
  • 2
  • 7
  • Your file verifies on my machine (except for some trigger warnings, which you can ignore until they bite you later). What version of Dafny and Z3 are you using? – James Wilcox Jul 23 '20 at 16:41
  • I'll also give a little mini answer here: the problem is that intersection (`*`) is not allowed to be a trigger. For some of your quantifiers, that means there are no allowed triggers, which means that Dafny/Z3 will have trouble using these quantified facts. When using set union/intersection under quantifiers, I recommend either wrapping them in a function like you did, or expanding them (as in `x in a && x in b` instead of `x in a*b`). – James Wilcox Jul 23 '20 at 16:47
  • if you figured it out, can you post a self-answer? if not, let us know what you're still stuck on. – James Wilcox Jul 28 '20 at 05:09
  • 1
    Slowly I am getting to understand the idea behind triggers but am far from fluent in using them. Having a history of using natural deduction and isabelle HOL I feel these offer a more solid ground on which I can construct proofs. This may simply be familiarity I will not be able to tell for quite some time. But at the moment I am left "grouping in the dark". It may be that the HOL-Boogie work will offer an alternative but at the moment teaching prevents me from exploring this avenue. – david streader Aug 07 '20 at 22:41

1 Answers1

0

I know this answer comes a bit later and indeed does not offer anything new, but I coded the original problem (the same code as David Streader but where all the inters(a,b) have been substituted by a*b) and the solution (all the a*b replaced by inters(a,b)). Just if someone wants to play:

Original problem (full of warnings):

function inters(a:set<int>, b:set<int>): set<int> {a*b}

method pingo(a:set<int>, b:set<int>) 
  {     
     assert  (forall x:int  :: (x !in (a*b) ) <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in  a*b)           <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in a*b )) <==> 
             (forall x:int  :: (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in  a*b))        <==> 
             (forall x:int  :: (x in a ==> x!in b ));
     
     assert  ((a*b) == {}) <==> (forall x:int  ::(x in a ==> x!in b )) ;
     assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  a*b ));
     assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  a*b )) ;
 }

Solution (no warnings):

function inters(a:set<int>, b:set<int>): set<int> {a*b}

method pingo(a:set<int>, b:set<int>) 
  {     
     assert  (forall x:int  :: (x !in inters(a , b) ) <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in  inters(a , b) )           <==> (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in inters(a , b) )) <==> 
             (forall x:int  :: (x in a ==> x!in b ));
     assert  (forall x:int  :: (x !in  inters(a , b) ))        <==> 
             (forall x:int  :: (x in a ==> x!in b ));
     
     assert  ((a*b) == {}) <==> (forall x:int  ::(x in a ==> x!in b )) ;
     assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  inters(a , b) ));
     assert  ((a*b) == {})  ==> (forall x:int  :: (x !in  inters(a , b)  )) ;
 }

//

So in this case, if we take James Wilcox's answer, only the first suggestion can be used (wrap the forall... in a function). That's because here is no case where we can apply the ‘expansion’, because there are only cases like x!in ..., and x!in inters(a,b) is not the same as x!in (a) && x!in(b).

Theo Deep
  • 666
  • 4
  • 15