From f3d609f0f6ef889bb066cc31ee514bb9671f4799 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Tue, 10 Mar 2015 15:33:11 -0700
Subject: 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

---
 Binaries/DafnyPrelude.bpl         | 13 +++++-
 Test/dafny0/SmallTests.dfy        | 95 +++++++++++++++++++++++++++++++++++++++
 Test/dafny0/SmallTests.dfy.expect |  2 +-
 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
-- 
cgit v1.2.3