use 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 0
pub 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 0
pub 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!