Beefed up collection axioms (in particular, for maps) to improve the chance of proving the existence check of let-such-that and assign-such-that

3 files changed, 107 insertions, 3 deletions

diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl
index 0e91bf95..4972517b 100644
--- a/Binaries/DafnyPrelude.bpl
+++ b/Binaries/DafnyPrelude.bpl
@@ -686,7 +686,14 @@ axiom (forall<T> s: Seq T :: { Seq#Length(s) } 0 <= Seq#Length(s));
 

 function Seq#Empty<T>(): Seq T;

 axiom (forall<T> :: Seq#Length(Seq#Empty(): Seq T) == 0);

-axiom (forall<T> s: Seq T :: { Seq#Length(s) } Seq#Length(s) == 0 ==> s == Seq#Empty());

+axiom (forall<T> s: Seq T :: { Seq#Length(s) }

+  (Seq#Length(s) == 0 ==> s == Seq#Empty())

+// The following would be a nice fact to include, because it would enable verifying the

+// GenericPick.SeqPick* methods in Test/dafny0/SmallTests.dfy.  However, it substantially

+// slows down performance on some other tests, including running seemingly forever on

+// some.

+//  && (Seq#Length(s) != 0 ==> (exists x: T :: Seq#Contains(s, x)))

+  );

 

 // The empty sequence $Is any type

 axiom (forall<T> t: Ty :: {$Is(Seq#Empty(): Seq T, t)} $Is(Seq#Empty(): Seq T, t));

@@ -887,7 +894,9 @@ function Map#Empty<U, V>(): Map U V;
 axiom (forall<U, V> u: U ::

         { Map#Domain(Map#Empty(): Map U V)[u] }

         !Map#Domain(Map#Empty(): Map U V)[u]);

-axiom (forall<U, V> m: Map U V :: { Map#Card(m) } Map#Card(m) == 0 <==> m == Map#Empty());

+axiom (forall<U, V> m: Map U V :: { Map#Card(m) }

+ (Map#Card(m) == 0 <==> m == Map#Empty()) &&

+ (Map#Card(m) != 0 ==> (exists x: U :: Map#Domain(m)[x])));

 

 function Map#Glue<U, V>([U] bool, [U]V, Ty): Map U V;

 axiom (forall<U, V> a: [U] bool, b:[U]V, t:Ty ::

diff --git a/Test/dafny0/SmallTests.dfy b/Test/dafny0/SmallTests.dfy
index 02335678..65db7f7f 100644
--- a/Test/dafny0/SmallTests.dfy
+++ b/Test/dafny0/SmallTests.dfy
@@ -715,3 +715,98 @@ class GT {
     }

   }

 }

+

+// ----- tests of various ways to express that a collection is nonempty, showing that these all lead to being

+// ----- able to pick an element from the (domain of the) collection

+

+module GenericPick {

+  function SetPick0<U>(s: set<U>): U

+    requires s != {}

+  {

+    var x :| x in s; x

+  }

+  function SetPick1<U>(s: set<U>): U

+    requires |s| != 0

+  {

+    var x :| x in s; x

+  }

+  function SetPick2<U>(s: set<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+

+  function MultisetPick0<U>(s: multiset<U>): U

+    requires s != multiset{}

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick1<U>(s: multiset<U>): U

+    requires |s| != 0

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick2<U>(s: multiset<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+  function MultisetPick3<U>(s: multiset<U>): U

+    requires exists x :: s[x] > 0

+  {

+    var x :| x in s; x

+  }

+

+  function SeqPick0<U>(s: seq<U>): U

+    requires s != []

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick1<U>(s: seq<U>): U

+    requires |s| != 0

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick2<U>(s: seq<U>): U

+    requires exists x :: x in s

+  {

+    var x :| x in s; x

+  }

+  function SeqPick3<U>(s: seq<U>): U

+    requires exists i :: 0 <= i < |s|

+  {

+    EquivalentWaysOfSayingSequenceIsNonempty(s);  // I wish this wasn't needed; see comment near Seq#Length axioms in DafnyPrelude.bpl

+    var x :| x in s; x

+  }

+  function SeqPick4<U>(s: seq<U>): U

+    requires exists i :: 0 <= i < |s|

+  {

+    var i :| 0 <= i < |s|; s[i]

+  }

+  lemma EquivalentWaysOfSayingSequenceIsNonempty<U>(s: seq<U>)

+    requires s != []

+          || |s| != 0

+          || exists i :: 0 <= i < |s|

+    ensures exists x :: x in s

+  {

+    assert s[0] in s;

+  }

+

+  function MapPick0<U,V>(m: map<U,V>): U

+    requires m != map[]

+  {

+    var x :| x in m; x

+  }

+  function MapPick1<U,V>(m: map<U,V>): U

+    requires |m| != 0

+  {

+    var x :| x in m; x

+  }

+  function MapPick2<U,V>(m: map<U,V>): U

+    requires exists x :: x in m

+  {

+    var x :| x in m; x

+  }

+}

diff --git a/Test/dafny0/SmallTests.dfy.expect b/Test/dafny0/SmallTests.dfy.expect
index 1983d2ac..5f766cd6 100644
--- a/Test/dafny0/SmallTests.dfy.expect
+++ b/Test/dafny0/SmallTests.dfy.expect
@@ -196,6 +196,6 @@ SmallTests.dfy(673,9): Error: cannot establish the existence of LHS values that
 Execution trace:

     (0,0): anon0

 

-Dafny program verifier finished with 87 verified, 35 errors

+Dafny program verifier finished with 104 verified, 35 errors

 

 Dafny program verifier finished with 0 verified, 0 errors