Add choose() and its axiom to multiset (#579)

This PR adds choose() to multiset, and an axiom saying that if the multiset's len is not zero, then the chosen value is in the multiset, similarly to set.

source/pervasive/multiset.rs

@@ -108,6 +108,17 @@ impl<V> Multiset<V> {
 
     // TODO define this in terms of a more general constructor?
     pub spec fn filter(self, f: impl Fn(V) -> bool) -> Self;
+
+    /// Chooses an arbitrary value of the multiset.
+    ///
+    /// This is often useful for proofs by induction.
+    ///
+    /// (Note that, although the result is arbitrary, it is still a _deterministic_ function
+    /// like any other `spec` function.)
+
+    pub open spec fn choose(self) -> V {
+        choose|v: V| self.count(v) > 0
+    }
 }
 
 // Specification of `empty`
@@ -200,6 +211,17 @@ pub proof fn axiom_filter_count<V>(m: Multiset<V>, f: FnSpec(V) -> bool, v: V)
         if f(v) { m.count(v) } else { 0 }
 {}
 
+// Specification of `choose`
+
+#[verifier(external_body)]
+#[verifier(broadcast_forall)]
+pub proof fn axiom_choose_count<V>(m: Multiset<V>)
+    requires
+        #[trigger] m.len() != 0,
+    ensures
+        #[trigger] m.count(m.choose()) > 0,
+{}
+
 #[macro_export]
 macro_rules! assert_multisets_equal {
     (::builtin::spec_eq($m1:expr, $m2:expr)) => {

source/rust_verify_test/tests/multiset.rs

@@ -58,6 +58,24 @@ test_verify_one_file! {
             assert(a.sub(b).add(b).ext_equal(a));
         }
 
+        pub proof fn choose_count<V>(m: Multiset<V>)
+            requires
+                m.len() != 0,
+        {
+            assert(m.count(m.choose()) > 0);
+        }
+
+        pub proof fn len_is_zero_if_count_for_each_value_is_zero<V>(m: Multiset<V>)
+            requires
+                forall |v| m.count(v) == 0,
+            ensures
+                m.len() == 0,
+        {
+            if m.len() != 0 {
+                assert(m.count(m.choose()) > 0);
+            }
+        }
+
     } => Ok(())
 }
 
@@ -96,3 +114,15 @@ test_verify_one_file! {
         }
     } => Err(err) => assert_one_fails(err)
 }
+
+test_verify_one_file! {
+    #[test] multiset_fail4 verus_code! {
+        use vstd::multiset::*;
+
+        pub proof fn choose_count<V>(m: Multiset<V>)
+        {
+            // Missing the precondition `m.len() != 0`
+            assert(m.count(m.choose()) > 0); // FAILS
+        }
+    } => Err(err) => assert_one_fails(err)
+}