Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575576577578579580581582583584585586587588589590591592593594595596597598599600601602603604605606607608609610611612613614615616617618619620621622623624625626627628629630631632633634635636637638639640641642643644645646647648649650651652653654655656657658659660661662663664665666667668669670671672673674675676677678679680681682683684685686687688689690691692693694695696697698699700701702703704705706707708709710711712713714715716717718719720721722723724725726727728use core::marker;
#[allow(unused_imports)]use super::map::*;#[cfg(verus_keep_ghost)]use super::math::clip;#[cfg(verus_keep_ghost)]use super::math::min;#[allow(unused_imports)]use super::pervasive::*;#[allow(unused_imports)]use super::prelude::*;#[allow(unused_imports)]use super::set::*;
verus! {
broadcast use group_set_lemmas;
/// `Multiset<V>` is an abstract multiset type for specifications.////// `Multiset<V>` can be encoded as a (total) map from elements to natural numbers,/// where the number of nonzero entries is finite.////// Multisets can be constructed in a few different ways:/// * [`Multiset::empty`] constructs an empty multiset./// * [`Multiset::singleton`] constructs a multiset that contains a single element with multiplicity 1./// * [`Multiset::from_map`] constructs a multiset from a map of elements to multiplicities./// * By manipulating existings multisets with [`Multiset::add`], [`Multiset::insert`],/// [`Multiset::sub`], [`Multiset::remove`], [`Multiset::update`], or [`Multiset::filter`]./// * TODO: `multiset!` constructor macro, multiset from set, from map, etc.////// To prove that two multisets are equal, it is usually easiest to use the/// extensionality operator `=~=`.///// We could in principle implement the Multiset via an inductive datatype// and so we can mark its type argument as accept_recursive_types.// Note: Multiset is finite because it isn't entirely obvious how to represent an// infinite multiset in the case where a single value (v: V) has an infinite// multiplicity. It seems to require either:// (1) representing multiplicity by an ordinal or cardinal or something// (2) limiting each multiplicity to be finite// (1) would be complicated and it's not clear what the use would be; (2) has some// weird properties (e.g., you can't in general define a multiset `map` function// since it might map an infinite number of elements to the same one).// Also, note that if multiset were infinite, it couldn't accept_recursive_types.//// Now that Verus has a finite Map that is labeled as accept_recursive_types, this file should// be rewritten as just a wrapper around Map rather than the present pile of trusted axioms.// See https://github.com/verus-lang/verus/discussions/1663//#[verifier::external_body]#[verifier::ext_equal]#[verifier::accept_recursive_types(V)]pub struct Multiset<V> { dummy: marker::PhantomData<V>,}
impl<V> Multiset<V> { /// Returns the _count_, or _multiplicity_ of a single value within the multiset. pub uninterp spec fn count(self, value: V) -> nat;
/// The total size of the multiset, i.e., the sum of all multiplicities over all values. pub uninterp spec fn len(self) -> nat;
/// An empty multiset. pub uninterp spec fn empty() -> Self;
/// Creates a multiset whose elements are given by the domain of the map `m` and whose /// multiplicities are given by the corresponding values of `m[element]`. pub uninterp spec fn from_map(m: Map<V, nat>) -> Self;
pub open spec fn from_set(m: Set<V>) -> Self { Self::from_map(Map::new(m, |v| 1)) }
/// A singleton multiset, i.e., a multiset with a single element of multiplicity 1. pub uninterp spec fn singleton(v: V) -> Self;
/// Takes the union of two multisets. For a given element, its multiplicity in /// the resulting multiset is the sum of its multiplicities in the operands. pub uninterp spec fn add(self, m2: Self) -> Self;
/// Takes the difference of two multisets. /// The multiplicities of `m2` are subtracted from those of `self`; if any element /// occurs more in `m2` then the resulting multiplicity bottoms out at 0. /// (See [`axiom_multiset_sub`] for the precise definition.) /// /// Note in particular that `self == self.sub(m).add(m)` only holds if /// `m` is included in `self`. pub uninterp spec fn sub(self, m2: Self) -> Self;
/// Inserts one instance the value `v` into the multiset. /// /// This always increases the total size of the multiset by 1. pub open spec fn insert(self, v: V) -> Self { self.add(Self::singleton(v)) }
/// Removes one instance of the value `v` from the multiset. /// /// If `v` was absent from the multiset, then the multiset is unchanged. pub open spec fn remove(self, v: V) -> Self { self.sub(Self::singleton(v)) }
/// Updates the multiplicity of the value `v` in the multiset to `mult`. pub open spec fn update(self, v: V, mult: nat) -> Self { let map = Map::new( self.dom().insert(v), |key: V| if key == v { mult } else { self.count(key) }, ); Self::from_map(map) }
/// Returns `true` is the left argument is contained in the right argument, /// that is, if for each value `v`, the number of occurences in the left /// is at most the number of occurences in the right. pub open spec fn subset_of(self, m2: Self) -> bool { forall|v: V| self.count(v) <= m2.count(v) }
#[verifier::inline] pub open spec fn spec_le(self, m2: Self) -> bool { self.subset_of(m2) }
// TODO define this in terms of a more general constructor? pub uninterp 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 }
/// Predicate indicating if the multiset contains the given value. pub open spec fn contains(self, v: V) -> bool { self.count(v) > 0 }
/// Predicate indicating if the set contains the given element: supports `self has a` syntax. #[verifier::inline] pub open spec fn spec_has(self, v: V) -> bool { self.contains(v) }
/// Returns a multiset containing the lower count of a given element /// between the two sets. In other words, returns a multiset with only /// the elements that "overlap". pub open spec fn intersection_with(self, other: Self) -> Self { let m = Map::<V, nat>::new( self.dom(), |v: V| min(self.count(v) as int, other.count(v) as int) as nat, ); Self::from_map(m) }
/// Returns a multiset containing the difference between the count of a /// given element of the two sets. pub open spec fn difference_with(self, other: Self) -> Self { let m = Map::<V, nat>::new(self.dom(), |v: V| clip(self.count(v) - other.count(v))); Self::from_map(m) }
/// Returns true if there exist no elements that have a count greater /// than 0 in both multisets. In other words, returns true if the two /// multisets have no elements in common. pub open spec fn is_disjoint_from(self, other: Self) -> bool { forall|x: V| self.count(x) == 0 || other.count(x) == 0 }
// This module assumes that all well-formed multisets have finite footprint, // so this axiom is reasonable. axiom fn axiom_dom_finite(self) ensures #[trigger] ISet::new(|v: V| self.count(v) > 0).finite(), ;
/// Returns the set of all elements that have a count greater than 0 pub closed spec fn dom(self) -> Set<V> { Set::new(|v: V| self.count(v) > 0).unwrap() }
// dom() won't mean anything unless we know our domain is finite, which is a soundness // invariant that the present axiom-heavy representation promises to maintain. pub broadcast proof fn dom_ensures(self) ensures #![trigger(self.dom())] forall|v: V| #[trigger] self.dom().contains(v) <==> self.count(v) > 0, { self.axiom_dom_finite(); assert forall|v: V| #[trigger] self.dom().contains(v) <==> self.count(v) > 0 by { super::iset::lemma_iset_new(|vv: V| self.count(vv) > 0, v); } }}
// Specification of `empty`/// The empty multiset maps every element to multiplicity 0pub broadcast axiom fn axiom_multiset_empty<V>(v: V) ensures #[trigger] Multiset::empty().count(v) == 0,;
// This verified lemma used to be an axiom in the Dafny prelude/// A multiset is equivalent to the empty multiset if and only if it has length 0./// If the multiset has length greater than 0, then there exists some element in the/// multiset that has a count greater than 0.pub broadcast proof fn lemma_multiset_empty_len<V>(m: Multiset<V>) ensures #[trigger] m.len() == 0 <==> m =~= Multiset::empty(), #[trigger] m.len() > 0 ==> exists|v: V| 0 < m.count(v),{ broadcast use group_multiset_axioms;
assert(m.len() == 0 <==> m =~= Multiset::empty());}
// Specifications of `from_map`/// A call to Multiset::new with input map `m` will return a multiset that maps/// value `v` to multiplicity `m[v]` if `v` is in the domain of `m`.pub broadcast axiom fn axiom_multiset_contained<V>(m: Map<V, nat>, v: V) requires m.dom().contains(v), ensures// #[trigger] Multiset::from_map(m).dom().contains(v),
#[trigger] Multiset::from_map(m).count(v) == m[v],;
/// A call to Multiset::new with input map `m` will return a multiset that maps/// value `v` to multiplicity 0 if `v` is not in the domain of `m`.pub broadcast axiom fn axiom_multiset_new_not_contained<V>(m: Map<V, nat>, v: V) requires !m.dom().contains(v), ensures #[trigger] Multiset::from_map(m).count(v) == 0,;
pub broadcast proof fn lemma_from_map_dom<V>(mymap: Map<V, nat>) requires forall|k| #[trigger] mymap.contains_key(k) ==> mymap[k] > 0, ensures #[trigger] Multiset::from_map(mymap).dom() == mymap.dom(),{ broadcast use { super::set::group_set_lemmas, Multiset::dom_ensures, axiom_multiset_contained, axiom_multiset_new_not_contained, };
let lhs = Multiset::from_map(mymap).dom(); let rhs = mymap.dom(); assert forall|v: V| lhs.contains(v) <==> rhs.contains(v) by { if lhs.contains(v) { assert(Multiset::from_map(mymap).count(v) > 0); if !mymap.dom().contains(v) { axiom_multiset_new_not_contained(mymap, v); assert(false); } } if rhs.contains(v) { assert(mymap.dom().contains(v)); assert(mymap.contains_key(v)); axiom_multiset_contained(mymap, v); assert(mymap[v] > 0); assert(Multiset::from_map(mymap).count(v) > 0); assert(lhs.contains(v)); } }; axiom_set_ext_equal(lhs, rhs);}
// Specification of `singleton`/// A call to Multiset::singleton with input value `v` will return a multiset that maps/// value `v` to multiplicity 1.pub broadcast axiom fn axiom_multiset_singleton<V>(v: V) ensures (#[trigger] Multiset::singleton(v)).count(v) == 1,;
/// A call to Multiset::singleton with input value `v` will return a multiset that maps/// any value other than `v` to 0pub broadcast axiom fn axiom_multiset_singleton_different<V>(v: V, w: V) ensures v != w ==> #[trigger] Multiset::singleton(v).count(w) == 0,;
// Specification of `add`/// The count of value `v` in the multiset `m1.add(m2)` is equal to the sum of the/// counts of `v` in `m1` and `m2` individually.pub broadcast axiom fn axiom_multiset_add<V>(m1: Multiset<V>, m2: Multiset<V>, v: V) ensures #[trigger] m1.add(m2).count(v) == m1.count(v) + m2.count(v),;
// Specification of `sub`/// The count of value `v` in the multiset `m1.sub(m2)` is equal to the difference between the/// count of `v` in `m1` and `m2` individually. However, the difference is cut off at 0 and/// cannot be negative.pub broadcast axiom fn axiom_multiset_sub<V>(m1: Multiset<V>, m2: Multiset<V>, v: V) ensures #[trigger] m1.sub(m2).count(v) == if m1.count(v) >= m2.count(v) { m1.count(v) - m2.count(v) } else { 0 },;
// Extensional equality/// Two multisets are equivalent if and only if they have the same count for every value.pub broadcast axiom fn axiom_multiset_ext_equal<V>(m1: Multiset<V>, m2: Multiset<V>) ensures #[trigger] (m1 =~= m2) <==> (forall|v: V| m1.count(v) == m2.count(v)),;
pub broadcast axiom fn axiom_multiset_ext_equal_deep<V>(m1: Multiset<V>, m2: Multiset<V>) ensures #[trigger] (m1 =~~= m2) <==> m1 =~= m2,;
// Specification of `len`/// The length of the empty multiset is 0.pub broadcast axiom fn axiom_len_empty<V>() ensures (#[trigger] Multiset::<V>::empty().len()) == 0,;
/// The length of a singleton multiset is 1.pub broadcast axiom fn axiom_len_singleton<V>(v: V) ensures (#[trigger] Multiset::<V>::singleton(v).len()) == 1,;
/// The length of the addition of two multisets is equal to the sum of the lengths of each individual multiset.pub broadcast axiom fn axiom_len_add<V>(m1: Multiset<V>, m2: Multiset<V>) ensures (#[trigger] m1.add(m2).len()) == m1.len() + m2.len(),;
// TODO could probably prove this theorem./// The length of the subtraction of two multisets is equal to the difference between the lengths of each individual multiset.pub broadcast axiom fn axiom_len_sub<V>(m1: Multiset<V>, m2: Multiset<V>) requires m2.subset_of(m1), ensures (#[trigger] m1.sub(m2).len()) == m1.len() - m2.len(),;
/// The count for any given value `v` in a multiset `m` must be less than or equal to the length of `m`.pub broadcast axiom fn axiom_count_le_len<V>(m: Multiset<V>, v: V) ensures #[trigger] m.count(v) <= #[trigger] m.len(),;
// Specification of `filter`/// For a given value `v` and boolean predicate `f`, if `f(v)` is true, then the count of `v` in/// `m.filter(f)` is the same as the count of `v` in `m`. Otherwise, the count of `v` in `m.filter(f)` is 0.pub broadcast axiom fn axiom_filter_count<V>(m: Multiset<V>, f: spec_fn(V) -> bool, v: V) ensures (#[trigger] m.filter(f).count(v)) == if f(v) { m.count(v) } else { 0 },;
// Specification of `choose`/// In a nonempty multiset `m`, the `choose` function will return a value that maps to a multiplicity/// greater than 0 in `m`.pub broadcast axiom fn axiom_choose_count<V>(m: Multiset<V>) requires #[trigger] m.len() != 0, ensures #[trigger] m.count(m.choose()) > 0,;
pub broadcast group group_multiset_axioms { axiom_multiset_empty, axiom_multiset_contained, axiom_multiset_new_not_contained, lemma_from_map_dom, axiom_multiset_singleton, axiom_multiset_singleton_different, axiom_multiset_add, axiom_multiset_sub, axiom_multiset_ext_equal, axiom_multiset_ext_equal_deep, axiom_len_empty, axiom_len_singleton, axiom_len_add, axiom_len_sub, axiom_count_le_len, axiom_filter_count, axiom_choose_count,}
// Lemmas about `update`/// The multiset resulting from updating a value `v` in a multiset `m` to multiplicity `mult` will/// have a count of `mult` for `v`.pub broadcast proof fn lemma_update_same<V>(m: Multiset<V>, v: V, mult: nat) ensures #[trigger] m.update(v, mult).count(v) == mult,{ broadcast use { group_set_lemmas, super::map::group_map_lemmas, group_multiset_axioms, Multiset::dom_ensures, };
reveal(Multiset::update); let key_set = m.dom().insert(v); let fv = |key: V| if key == v { mult } else { m.count(key) }; let map = Map::new(key_set, fv); crate::vstd::map_lib::lemma_map_new_domain(key_set, fv); assert(key_set.contains(v)); assert(map.dom().contains(v)); assert(map[v] == mult); axiom_multiset_contained(map, v);}
/// The multiset resulting from updating a value `v1` in a multiset `m` to multiplicity `mult` will/// not change the multiplicities of any other values in `m`.pub broadcast proof fn lemma_update_different<V>(m: Multiset<V>, v1: V, mult: nat, v2: V) requires v1 != v2, ensures #[trigger] m.update(v1, mult).count(v2) == m.count(v2),{ broadcast use {group_set_lemmas, super::map::group_map_lemmas, group_multiset_axioms}; broadcast use {axiom_multiset_contained, Multiset::dom_ensures};
reveal(Multiset::update); let key_set = m.dom().insert(v1); let fv = |key: V| if key == v1 { mult } else { m.count(key) }; let map = Map::new(key_set, fv); crate::vstd::map_lib::lemma_map_new_domain(key_set, fv); if map.dom().contains(v2) { assert(map[v2] == m.count(v2)); axiom_multiset_contained(map, v2); } else { axiom_multiset_new_not_contained(map, v2); assert(!m.dom().contains(v2)) by { if m.dom().contains(v2) { assert(key_set.contains(v2)); assert(map.dom().contains(v2)); assert(false); } } m.dom_ensures(); assert(m.count(v2) == 0); }}
// Lemmas about `insert`// This verified lemma used to be an axiom in the Dafny prelude/// If you insert element x into multiset m, then element y maps/// to a count greater than 0 if and only if x==y or y already/// mapped to a count greater than 0 before the insertion of x.pub broadcast proof fn lemma_insert_containment<V>(m: Multiset<V>, x: V, y: V) ensures 0 < #[trigger] m.insert(x).count(y) <==> x == y || 0 < m.count(y),{ broadcast use group_multiset_axioms;
}
// This verified lemma used to be an axiom in the Dafny prelude/// Inserting an element `x` into multiset `m` will increase the count of `x` in `m` by 1.pub broadcast proof fn lemma_insert_increases_count_by_1<V>(m: Multiset<V>, x: V) ensures #[trigger] m.insert(x).count(x) == m.count(x) + 1,{ broadcast use group_multiset_axioms;
}
// This verified lemma used to be an axiom in the Dafny prelude/// If multiset `m` maps element `y` to a multiplicity greater than 0, then inserting any element `x`/// into `m` will not cause `y` to map to a multiplicity of 0. This is a way of saying that inserting `x`/// will not cause any counts to decrease, because it accounts both for when x == y and when x != y.pub broadcast proof fn lemma_insert_non_decreasing<V>(m: Multiset<V>, x: V, y: V) ensures 0 < m.count(y) ==> 0 < #[trigger] m.insert(x).count(y),{ broadcast use group_multiset_axioms;
}
// This verified lemma used to be an axiom in the Dafny prelude/// Inserting an element `x` into a multiset `m` will not change the count of any other element `y` in `m`.pub broadcast proof fn lemma_insert_other_elements_unchanged<V>(m: Multiset<V>, x: V, y: V) ensures x != y ==> m.count(y) == #[trigger] m.insert(x).count(y),{ broadcast use group_multiset_axioms;
}
// This verified lemma used to be an axiom in the Dafny prelude/// Inserting an element `x` into a multiset `m` will increase the length of `m` by 1.pub broadcast proof fn lemma_insert_len<V>(m: Multiset<V>, x: V) ensures #[trigger] m.insert(x).len() == m.len() + 1,{ broadcast use group_multiset_axioms;
}
// Lemmas about `intersection_with`// This verified lemma used to be an axiom in the Dafny prelude/// The multiplicity of an element `x` in the intersection of multisets `a` and `b` will be the minimum/// count of `x` in either `a` or `b`.pub broadcast proof fn lemma_intersection_count<V>(a: Multiset<V>, b: Multiset<V>, x: V) ensures #[trigger] a.intersection_with(b).count(x) == min(a.count(x) as int, b.count(x) as int),{ broadcast use {group_set_lemmas, super::map::group_map_lemmas, group_multiset_axioms}; broadcast use {group_multiset_axioms, Multiset::dom_ensures};
let m = Map::new(a.dom(), |v: V| min(a.count(v) as int, b.count(v) as int) as nat); crate::vstd::map_lib::lemma_map_new_domain( a.dom(), |v: V| min(a.count(v) as int, b.count(v) as int) as nat, ); if m.dom().contains(x) { assert(m[x] == min(a.count(x) as int, b.count(x) as int) as nat); axiom_multiset_contained(m, x); } else { axiom_multiset_new_not_contained(m, x); assert(!a.dom().contains(x)); a.dom_ensures(); assert(a.count(x) == 0) by { if a.count(x) != 0 { assert(a.count(x) > 0); assert(a.dom().contains(x)); assert(false); } } assert(min(a.count(x) as int, b.count(x) as int) == 0); }}
// This verified lemma used to be an axiom in the Dafny prelude/// Taking the intersection of multisets `a` and `b` and then taking the resulting multiset's intersection/// with `b` again is the same as just taking the intersection of `a` and `b` once.pub broadcast proof fn lemma_left_pseudo_idempotence<V>(a: Multiset<V>, b: Multiset<V>) ensures #[trigger] a.intersection_with(b).intersection_with(b) =~= a.intersection_with(b),{ broadcast use group_multiset_axioms;
assert forall|x: V| #[trigger] a.intersection_with(b).count(x) == min(a.count(x) as int, b.count(x) as int) by { lemma_intersection_count(a, b, x); } assert forall|x: V| #[trigger] a.intersection_with(b).intersection_with(b).count(x) == min( a.count(x) as int, b.count(x) as int, ) by { lemma_intersection_count(a.intersection_with(b), b, x); assert(min(min(a.count(x) as int, b.count(x) as int) as int, b.count(x) as int) == min( a.count(x) as int, b.count(x) as int, )); }}
// This verified lemma used to be an axiom in the Dafny prelude/// Taking the intersection of multiset `a` with the result of taking the intersection of `a` and `b`/// is the same as just taking the intersection of `a` and `b` once.pub broadcast proof fn lemma_right_pseudo_idempotence<V>(a: Multiset<V>, b: Multiset<V>) ensures #[trigger] a.intersection_with(a.intersection_with(b)) =~= a.intersection_with(b),{ broadcast use group_multiset_axioms;
assert forall|x: V| #[trigger] a.intersection_with(b).count(x) == min(a.count(x) as int, b.count(x) as int) by { lemma_intersection_count(a, b, x); } assert forall|x: V| #[trigger] a.intersection_with(a.intersection_with(b)).count(x) == min( a.count(x) as int, b.count(x) as int, ) by { lemma_intersection_count(a, a.intersection_with(b), x); assert(min(a.count(x) as int, min(a.count(x) as int, b.count(x) as int) as int) == min( a.count(x) as int, b.count(x) as int, )); }}
// Lemmas about `difference_with`// This verified lemma used to be an axiom in the Dafny prelude/// The multiplicity of an element `x` in the difference of multisets `a` and `b` will be/// equal to the difference of the counts of `x` in `a` and `b`, or 0 if this difference is negative.pub broadcast proof fn lemma_difference_count<V>(a: Multiset<V>, b: Multiset<V>, x: V) ensures #[trigger] a.difference_with(b).count(x) == clip(a.count(x) - b.count(x)),{ broadcast use { group_set_lemmas, super::map::group_map_lemmas, group_multiset_axioms, Multiset::dom_ensures, };
let map = Map::<V, nat>::new(a.dom(), |v: V| clip(a.count(v) - b.count(v))); crate::vstd::map_lib::lemma_map_new_domain(a.dom(), |v: V| clip(a.count(v) - b.count(v))); if map.dom().contains(x) { assert(map[x] == clip(a.count(x) - b.count(x))); axiom_multiset_contained(map, x); } else { axiom_multiset_new_not_contained(map, x); assert(!a.dom().contains(x)); a.dom_ensures(); assert(a.count(x) == 0) by { if a.count(x) != 0 { assert(a.count(x) > 0); assert(a.dom().contains(x)); assert(false); } } assert(clip(a.count(x) - b.count(x)) == 0); }}
// This verified lemma used to be an axiom in the Dafny prelude/// If the multiplicity of element `x` is less in multiset `a` than in multiset `b`, then the multiplicity/// of `x` in the difference of `a` and `b` will be 0.pub broadcast proof fn lemma_difference_bottoms_out<V>(a: Multiset<V>, b: Multiset<V>, x: V) ensures #![trigger a.count(x), b.count(x), a.difference_with(b)] a.count(x) <= b.count(x) ==> a.difference_with(b).count(x) == 0,{ broadcast use group_multiset_axioms;
lemma_difference_count(a, b, x);}
#[macro_export]macro_rules! assert_multisets_equal { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::multiset::assert_multisets_equal_internal!($($tail)*)) };}
#[macro_export]macro_rules! assert_multisets_equal_internal { (::verus_builtin::spec_eq($m1:expr, $m2:expr)) => { $crate::vstd::multiset::assert_multisets_equal_internal!($m1, $m2) }; (::verus_builtin::spec_eq($m1:expr, $m2:expr), $k:ident $( : $t:ty )? => $bblock:block) => { $crate::vstd::multiset::assert_multisets_equal_internal!($m1, $m2, $k $( : $t )? => $bblock) }; (crate::verus_builtin::spec_eq($m1:expr, $m2:expr)) => { $crate::vstd::multiset::assert_multisets_equal_internal!($m1, $m2) }; (crate::verus_builtin::spec_eq($m1:expr, $m2:expr), $k:ident $( : $t:ty )? => $bblock:block) => { $crate::vstd::multiset::assert_multisets_equal_internal!($m1, $m2, $k $( : $t )? => $bblock) }; ($m1:expr, $m2:expr $(,)?) => { $crate::vstd::multiset::assert_multisets_equal_internal!($m1, $m2, key => { }) }; ($m1:expr, $m2:expr, $k:ident $( : $t:ty )? => $bblock:block) => { #[verifier::spec] let m1 = $m1; #[verifier::spec] let m2 = $m2; $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(m1, m2), { $crate::vstd::prelude::assert_forall_by(|$k $( : $t )?| { $crate::vstd::prelude::ensures([ $crate::vstd::prelude::equal(m1.count($k), m2.count($k)) ]); { $bblock } }); $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(m1, m2)); }); }}
pub broadcast group group_multiset_properties { lemma_update_same, lemma_update_different, lemma_multiset_empty_len, lemma_insert_containment, lemma_insert_increases_count_by_1, lemma_insert_non_decreasing, lemma_insert_other_elements_unchanged, lemma_insert_len, lemma_intersection_count, lemma_left_pseudo_idempotence, lemma_right_pseudo_idempotence, lemma_difference_count, lemma_difference_bottoms_out, Multiset::dom_ensures,}
#[doc(hidden)]pub use assert_multisets_equal_internal;pub use assert_multisets_equal;
} // verus!