#[allow(unused_imports)]
use super::iset::*;
#[allow(unused_imports)]
use super::multiset::Multiset;
#[allow(unused_imports)]
use super::pervasive::*;
use super::prelude::Seq;
#[allow(unused_imports)]
use super::prelude::*;
#[allow(unused_imports)]
use super::relations::*;
#[allow(unused_imports)]
use super::set::*;

verus! {

broadcast use super::iset::group_iset_lemmas;

impl<A> ISet<A> {
    /// Is `true` if called by a "full" set, i.e., a set containing every element of type `A`.
    pub open spec fn is_full(self) -> bool {
        self == ISet::<A>::full()
    }

    /// Is `true` if called by an "empty" set, i.e., a set containing no elements and has length 0
    pub open spec fn is_empty(self) -> (b: bool) {
        self =~= ISet::<A>::empty()
    }

    /// Returns the set contains an element `f(x)` for every element `x` in `self`.
    pub open spec fn map<B>(self, f: spec_fn(A) -> B) -> ISet<B> {
        ISet::new(|a: B| exists|x: A| self.contains(x) && a == f(x))
    }

    /// `ISet::map_by` is like `ISet::map`, but `map` only takes a forward function `fwd: spec_fn(A) -> B`,
    /// while `map_by` also takes a reverse function `rev: spec_fn(B) -> A`
    /// such that `rev(fwd(a)) == a`.
    /// When `fwd` has such a reverse function, `ISet::map_by` can make proofs easier
    /// by avoiding the "exists" that appears in lemmas about `ISet::map`.
    /// Example: for a set `s: ISet<int>`, to map each `i` in `s` to `(i, 10 * i)`,
    /// we can write either `s.map(|i: int| (i, 10 * i))`
    /// or `s.map_by(|i: int| (i, 10 * i), |p: (int, int)| p.0)`;
    /// the version with `map_by` is usually easier to use in proofs.
    /// If the recommendation `forall|a: A| self.contains(a) ==> rev(fwd(a)) == a` is satisfied,
    /// it is trivially guaranteed that `self.map_by(fwd, rev) == self.map(fwd)`.
    /// Also see the `set_build!` macro for a convenient interface to `map_by`.
    pub open spec fn map_by<B>(self, fwd: spec_fn(A) -> B, rev: spec_fn(B) -> A) -> ISet<B>
        recommends
            forall|a: A| self.contains(a) ==> rev(fwd(a)) == a,
    {
        ISet::new(|b: B| self.contains(rev(b)) && b == fwd(rev(b)))
    }

    /// Similar to `ISet::map_by`, but the forward function returns `ISet<B>` rather than `B`,
    /// and `map_flatten_by` flattens the final result from `ISet<ISet<B>>` to just `ISet<B>`.
    /// This can be easier to work with in proofs than calling `map` and `flatten` separately,
    /// since `map` and `flatten` introduce "exists", while `map_flatten_by` does not.
    /// Also see the `set_build!` macro for a convenient interface to `map_flatten_by`.
    pub open spec fn map_flatten_by<B>(
        self,
        fwd: spec_fn(A) -> ISet<B>,
        rev: spec_fn(B) -> A,
    ) -> ISet<B>
        recommends
            forall|a: A, b: B| #[trigger]
                self.contains(a) && fwd(a).contains(b) ==> #[trigger] rev(b) == a,
    {
        ISet::new(|b: B| self.contains(rev(b)) && fwd(rev(b)).contains(b))
    }

    /// This proof demonstrates that calling `map_flatten_by` is equivalent to
    /// first calling `map`, then calling `flatten`.
    pub proof fn map_flatten_by_is_map_flatten<B>(
        self,
        fwd: spec_fn(A) -> ISet<B>,
        rev: spec_fn(B) -> A,
    )
        requires
            forall|a: A, b: B| #[trigger]
                self.contains(a) && fwd(a).contains(b) ==> #[trigger] rev(b) == a,
        ensures
            self.map_flatten_by(fwd, rev) == self.map(fwd).flatten(),
    {
        assert forall|b: B| self.map_flatten_by(fwd, rev).contains(b) implies #[trigger] self.map(
            fwd,
        ).flatten().contains(b) by {
            let bs = choose|bs: ISet<B>|
                (exists|a: A| self.contains(a) && bs == fwd(a)) && bs.contains(b);
            assert(self.map(fwd).contains(bs) <==> (exists|a: A| self.contains(a) && bs == fwd(a)));
        }
    }

    /// Converts a set into a sequence with an arbitrary ordering.
    pub open spec fn to_seq(self) -> Seq<A>
        recommends
            self.finite(),
        decreases self.len(),
        when self.finite()
    {
        if self.len() == 0 {
            Seq::<A>::empty()
        } else {
            let x = self.choose();
            Seq::<A>::empty().push(x) + self.remove(x).to_seq()
        }
    }

    /// Converts a set into a sequence sorted by the given ordering function `leq`
    pub open spec fn to_sorted_seq(self, leq: spec_fn(A, A) -> bool) -> Seq<A> {
        self.to_seq().sort_by(leq)
    }

    /// A singleton set has at least one element and any two elements are equal.
    pub open spec fn is_singleton(self) -> bool {
        &&& self.len() > 0
        &&& (forall|x: A, y: A| self.contains(x) && self.contains(y) ==> x == y)
    }

    /// Indicates if the function given by `r` is injective on this set,
    /// i.e., whether each element of this set is mapped to a different
    /// value by `r`.
    pub open spec fn injective_on<B>(self, r: spec_fn(A) -> B) -> bool {
        forall|x1: A, x2: A|
            self.contains(x1) && self.contains(x2) && #[trigger] r(x1) == #[trigger] r(x2) ==> x1
                == x2
    }

    /// An element in an ordered set is called a least element (or a minimum), if it is less than
    /// every other element of the set.
    pub open spec fn has_least(self, leq: spec_fn(A, A) -> bool, min: A) -> bool {
        self.contains(min) && forall|x: A| self.contains(x) ==> #[trigger] leq(min, x)
    }

    /// An element in an ordered set is called a minimal element, if no other element is less than it.
    pub open spec fn has_minimum(self, leq: spec_fn(A, A) -> bool, min: A) -> bool {
        self.contains(min) && forall|x: A|
            self.contains(x) && #[trigger] leq(x, min) ==> #[trigger] leq(min, x)
    }

    /// An element in an ordered set is called a greatest element (or a maximum), if it is greater than
    ///every other element of the set.
    pub open spec fn has_greatest(self, leq: spec_fn(A, A) -> bool, max: A) -> bool {
        self.contains(max) && forall|x: A| self.contains(x) ==> #[trigger] leq(x, max)
    }

    /// An element in an ordered set is called a maximal element, if no other element is greater than it.
    pub open spec fn has_maximum(self, leq: spec_fn(A, A) -> bool, max: A) -> bool {
        self.contains(max) && forall|x: A|
            self.contains(x) && #[trigger] leq(max, x) ==> #[trigger] leq(x, max)
    }

    /// If a function is injective on the set `self`, then it is also injective on any subset `other` of `self`.
    pub proof fn lemma_injective_on_subset<B>(self, r: spec_fn(A) -> B, other: Self)
        requires
            other <= self,
            self.injective_on(r),
        ensures
            other.injective_on(r),
    {
        assert forall|a1: A, a2: A|
            other.contains(a1) && other.contains(a2) && #[trigger] r(a1) == #[trigger] r(
                a2,
            ) implies a1 == a2 by {
            assert(self.contains(a1));
            assert(self.contains(a2));
            assert(r(a1) == r(a2));
        }
    }

    /// Any totally-ordered set contains a unique minimal (equivalently, least) element.
    /// Returns an arbitrary value if r is not a total ordering
    pub closed spec fn find_unique_minimal(self, r: spec_fn(A, A) -> bool) -> A
        recommends
            total_ordering(r),
            self.len() > 0,
            self.finite(),
        decreases self.len(),
        when self.finite()
    {
        proof {
            broadcast use group_iset_properties;

        }
        if self.len() <= 1 {
            self.choose()
        } else {
            let x = choose|x: A| self.contains(x);
            let min = self.remove(x).find_unique_minimal(r);
            if r(min, x) {
                min
            } else {
                x
            }
        }
    }

    /// Proof of correctness and expected behavior for `ISet::find_unique_minimal`.
    pub proof fn find_unique_minimal_ensures(self, r: spec_fn(A, A) -> bool)
        requires
            self.finite(),
            self.len() > 0,
            total_ordering(r),
        ensures
            self.has_minimum(r, self.find_unique_minimal(r)) && (forall|min: A|
                self.has_minimum(r, min) ==> self.find_unique_minimal(r) == min),
        decreases self.len(),
    {
        broadcast use group_iset_properties;

        if self.len() == 1 {
            let x = choose|x: A| self.contains(x);
            assert(self.remove(x).insert(x) =~= self);
            assert(self.has_minimum(r, self.find_unique_minimal(r)));
        } else {
            let x = choose|x: A| self.contains(x);
            self.remove(x).find_unique_minimal_ensures(r);
            assert(self.remove(x).has_minimum(r, self.remove(x).find_unique_minimal(r)));
            let y = self.remove(x).find_unique_minimal(r);
            let min_updated = self.find_unique_minimal(r);
            assert(!r(y, x) ==> min_updated == x);
            assert(forall|elt: A|
                self.remove(x).contains(elt) && #[trigger] r(elt, y) ==> #[trigger] r(y, elt));
            assert forall|elt: A|
                self.contains(elt) && #[trigger] r(elt, min_updated) implies #[trigger] r(
                min_updated,
                elt,
            ) by {
                assert(r(min_updated, x) || r(min_updated, y));
                if min_updated == y {  // Case where the new min is the old min
                    assert(self.has_minimum(r, self.find_unique_minimal(r)));
                } else {  //Case where the new min is the newest element
                    assert(self.remove(x).contains(elt) || elt == x);
                    assert(min_updated == x);
                    assert(r(x, y) || r(y, x));
                    assert(!r(x, y) || !r(y, x));
                    assert(!(min_updated == y) ==> !r(y, x));
                    assert(r(x, y));
                    if (self.remove(x).contains(elt)) {
                        assert(r(elt, y) && r(y, elt) ==> elt == y);
                    } else {
                    }
                }
            }
            assert forall|min_poss: A|
                self.has_minimum(r, min_poss) implies self.find_unique_minimal(r) == min_poss by {
                assert(self.remove(x).has_minimum(r, min_poss) || x == min_poss);
                if self.remove(x).has_minimum(r, min_poss) {
                    assert(r(x, min_poss) ==> r(min_poss, x));
                    assert(r(min_poss, self.find_unique_minimal(r)));
                } else {
                    assert(x == min_poss);
                    assert(r(x, y));
                }
            }
        }
    }

    /// Any totally-ordered set contains a unique maximal (equivalently, greatest) element.
    /// Returns an arbitrary value if r is not a total ordering
    pub closed spec fn find_unique_maximal(self, r: spec_fn(A, A) -> bool) -> A
        recommends
            total_ordering(r),
            self.len() > 0,
        decreases self.len(),
        when self.finite()
    {
        proof {
            broadcast use group_iset_properties;

        }
        if self.len() <= 1 {
            self.choose()
        } else {
            let x = choose|x: A| self.contains(x);
            let max = self.remove(x).find_unique_maximal(r);
            if r(x, max) {
                max
            } else {
                x
            }
        }
    }

    /// Proof of correctness and expected behavior for `ISet::find_unique_maximal`.
    pub proof fn find_unique_maximal_ensures(self, r: spec_fn(A, A) -> bool)
        requires
            self.finite(),
            self.len() > 0,
            total_ordering(r),
        ensures
            self.has_maximum(r, self.find_unique_maximal(r)) && (forall|max: A|
                self.has_maximum(r, max) ==> self.find_unique_maximal(r) == max),
        decreases self.len(),
    {
        broadcast use group_iset_properties;

        if self.len() == 1 {
            let x = choose|x: A| self.contains(x);
            assert(self.remove(x) =~= ISet::<A>::empty());
            assert(self.contains(self.find_unique_maximal(r)));
        } else {
            let x = choose|x: A| self.contains(x);
            self.remove(x).find_unique_maximal_ensures(r);
            assert(self.remove(x).has_maximum(r, self.remove(x).find_unique_maximal(r)));
            assert(self.remove(x).insert(x) =~= self);
            let y = self.remove(x).find_unique_maximal(r);
            let max_updated = self.find_unique_maximal(r);
            assert(max_updated == x || max_updated == y);
            assert(!r(x, y) ==> max_updated == x);
            assert forall|elt: A|
                self.contains(elt) && #[trigger] r(max_updated, elt) implies #[trigger] r(
                elt,
                max_updated,
            ) by {
                assert(r(x, max_updated) || r(y, max_updated));
                if max_updated == y {  // Case where the new max is the old max
                    assert(r(elt, max_updated));
                    assert(r(x, max_updated));
                    assert(self.has_maximum(r, self.find_unique_maximal(r)));
                } else {  //Case where the new max is the newest element
                    assert(self.remove(x).contains(elt) || elt == x);
                    assert(max_updated == x);
                    assert(r(x, y) || r(y, x));
                    assert(!r(x, y) || !r(y, x));
                    assert(!(max_updated == y) ==> !r(x, y));
                    assert(r(y, x));
                    if (self.remove(x).contains(elt)) {
                        assert(r(y, elt) ==> r(elt, y));
                        assert(r(y, elt) && r(elt, y) ==> elt == y);
                        assert(r(elt, x));
                        assert(r(elt, max_updated))
                    } else {
                    }
                }
            }
            assert forall|max_poss: A|
                self.has_maximum(r, max_poss) implies self.find_unique_maximal(r) == max_poss by {
                assert(self.remove(x).has_maximum(r, max_poss) || x == max_poss);
                assert(r(max_poss, self.find_unique_maximal(r)));
                assert(r(self.find_unique_maximal(r), max_poss));
            }
        }
    }

    /// Converts a set into a multiset where each element from the set has
    /// multiplicity 1 and any other element has multiplicity 0.
    pub open spec fn to_multiset(self) -> Multiset<A>
        decreases self.len(),
        when self.finite()
    {
        if self.len() == 0 {
            Multiset::<A>::empty()
        } else {
            Multiset::<A>::empty().insert(self.choose()).add(
                self.remove(self.choose()).to_multiset(),
            )
        }
    }

    /// A finite set with length 0 is equivalent to the empty set.
    pub proof fn lemma_len0_is_empty(self)
        requires
            self.finite(),
            self.len() == 0,
        ensures
            self == ISet::<A>::empty(),
    {
        if exists|a: A| self.contains(a) {
            // derive contradiction:
            assert(self.remove(self.choose()).len() + 1 == 0);
        }
        assert(self =~= ISet::empty());
    }

    /// A singleton set has length 1.
    pub proof fn lemma_singleton_size(self)
        requires
            self.is_singleton(),
        ensures
            self.len() == 1,
    {
        broadcast use group_iset_properties;

        assert(self.remove(self.choose()) =~= ISet::empty());
    }

    /// A set has exactly one element, if and only if, it has at least one element and any two elements are equal.
    pub proof fn lemma_is_singleton(s: ISet<A>)
        requires
            s.finite(),
        ensures
            s.is_singleton() == (s.len() == 1),
    {
        if s.is_singleton() {
            s.lemma_singleton_size();
        }
        if s.len() == 1 {
            assert forall|x: A, y: A| s.contains(x) && s.contains(y) implies x == y by {
                let x = choose|x: A| s.contains(x);
                broadcast use group_iset_properties;

                assert(s.remove(x).len() == 0);
                assert(s.insert(x) =~= s);
            }
        }
    }

    /// The result of filtering a finite set is finite and has size less than or equal to the original set.
    pub proof fn lemma_len_filter(self, f: spec_fn(A) -> bool)
        requires
            self.finite(),
        ensures
            self.filter(f).finite(),
            self.filter(f).len() <= self.len(),
        decreases self.len(),
    {
        lemma_len_intersect::<A>(self, ISet::new(f));
    }

    /// In a pre-ordered set, a greatest element is necessarily maximal.
    pub proof fn lemma_greatest_implies_maximal(self, r: spec_fn(A, A) -> bool, max: A)
        requires
            pre_ordering(r),
        ensures
            self.has_greatest(r, max) ==> self.has_maximum(r, max),
    {
    }

    /// In a pre-ordered set, a least element is necessarily minimal.
    pub proof fn lemma_least_implies_minimal(self, r: spec_fn(A, A) -> bool, min: A)
        requires
            pre_ordering(r),
        ensures
            self.has_least(r, min) ==> self.has_minimum(r, min),
    {
    }

    /// In a totally-ordered set, an element is maximal if and only if it is a greatest element.
    pub proof fn lemma_maximal_equivalent_greatest(self, r: spec_fn(A, A) -> bool, max: A)
        requires
            total_ordering(r),
        ensures
            self.has_greatest(r, max) <==> self.has_maximum(r, max),
    {
        assert(self.has_maximum(r, max) ==> forall|x: A|
            !self.contains(x) || !r(max, x) || r(x, max));
    }

    /// In a totally-ordered set, an element is maximal if and only if it is a greatest element.
    pub proof fn lemma_minimal_equivalent_least(self, r: spec_fn(A, A) -> bool, min: A)
        requires
            total_ordering(r),
        ensures
            self.has_least(r, min) <==> self.has_minimum(r, min),
    {
        assert(self.has_minimum(r, min) ==> forall|x: A|
            !self.contains(x) || !r(x, min) || r(min, x));
    }

    /// In a partially-ordered set, there exists at most one least element.
    pub proof fn lemma_least_is_unique(self, r: spec_fn(A, A) -> bool)
        requires
            partial_ordering(r),
        ensures
            forall|min: A, min_prime: A|
                self.has_least(r, min) && self.has_least(r, min_prime) ==> min == min_prime,
    {
        assert forall|min: A, min_prime: A|
            self.has_least(r, min) && self.has_least(r, min_prime) implies min == min_prime by {
            assert(r(min, min_prime));
            assert(r(min_prime, min));
        }
    }

    /// In a partially-ordered set, there exists at most one greatest element.
    pub proof fn lemma_greatest_is_unique(self, r: spec_fn(A, A) -> bool)
        requires
            partial_ordering(r),
        ensures
            forall|max: A, max_prime: A|
                self.has_greatest(r, max) && self.has_greatest(r, max_prime) ==> max == max_prime,
    {
        assert forall|max: A, max_prime: A|
            self.has_greatest(r, max) && self.has_greatest(r, max_prime) implies max
            == max_prime by {
            assert(r(max_prime, max));
            assert(r(max, max_prime));
        }
    }

    /// In a totally-ordered set, there exists at most one minimal element.
    pub proof fn lemma_minimal_is_unique(self, r: spec_fn(A, A) -> bool)
        requires
            total_ordering(r),
        ensures
            forall|min: A, min_prime: A|
                self.has_minimum(r, min) && self.has_minimum(r, min_prime) ==> min == min_prime,
    {
        assert forall|min: A, min_prime: A|
            self.has_minimum(r, min) && self.has_minimum(r, min_prime) implies min == min_prime by {
            self.lemma_minimal_equivalent_least(r, min);
            self.lemma_minimal_equivalent_least(r, min_prime);
            self.lemma_least_is_unique(r);
        }
    }

    /// In a totally-ordered set, there exists at most one maximal element.
    pub proof fn lemma_maximal_is_unique(self, r: spec_fn(A, A) -> bool)
        requires
            self.finite(),
            total_ordering(r),
        ensures
            forall|max: A, max_prime: A|
                self.has_maximum(r, max) && self.has_maximum(r, max_prime) ==> max == max_prime,
    {
        assert forall|max: A, max_prime: A|
            self.has_maximum(r, max) && self.has_maximum(r, max_prime) implies max == max_prime by {
            self.lemma_maximal_equivalent_greatest(r, max);
            self.lemma_maximal_equivalent_greatest(r, max_prime);
            self.lemma_greatest_is_unique(r);
        }
    }

    /// ISet difference with an additional element inserted decreases the size of
    /// the result. This can be useful for proving termination when traversing
    /// a set while tracking the elements that have already been handled.
    pub broadcast proof fn lemma_iset_insert_diff_decreases(self, s: ISet<A>, elt: A)
        requires
            self.contains(elt),
            !s.contains(elt),
            self.finite(),
        ensures
            #[trigger] self.difference(s.insert(elt)).len() < self.difference(s).len(),
    {
        self.difference(s.insert(elt)).lemma_subset_not_in_lt(self.difference(s), elt);
    }

    /// If there is an element not present in a subset, its length is stricly smaller.
    pub proof fn lemma_subset_not_in_lt(self: ISet<A>, s2: ISet<A>, elt: A)
        requires
            self.subset_of(s2),
            s2.finite(),
            !self.contains(elt),
            s2.contains(elt),
        ensures
            self.len() < s2.len(),
    {
        let s2_no_elt = s2.remove(elt);
        assert(self.len() <= s2_no_elt.len()) by {
            lemma_len_subset(self, s2_no_elt);
        }
    }

    /// Inserting an element and mapping a function over a set commute
    pub broadcast proof fn lemma_iset_map_insert_commute<B>(self, elt: A, f: spec_fn(A) -> B)
        ensures
            #[trigger] self.insert(elt).map(f) =~= self.map(f).insert(f(elt)),
    {
        assert forall|x: B| self.map(f).insert(f(elt)).contains(x) implies self.insert(elt).map(
            f,
        ).contains(x) by {
            if x == f(elt) {
                assert(self.insert(elt).contains(elt));
            } else {
                let y = choose|y: A| self.contains(y) && f(y) == x;
                assert(self.insert(elt).contains(y));
            }
        }
    }

    /// `map` and `union` commute
    pub proof fn lemma_map_union_commute<B>(self, t: ISet<A>, f: spec_fn(A) -> B)
        ensures
            (self.union(t)).map(f) =~= self.map(f).union(t.map(f)),
    {
        broadcast use group_iset_lemmas;

        let lhs = self.union(t).map(f);
        let rhs = self.map(f).union(t.map(f));

        assert forall|elem: B| rhs.contains(elem) implies lhs.contains(elem) by {
            if self.map(f).contains(elem) {
                let preimage = choose|preimage: A| self.contains(preimage) && f(preimage) == elem;
                assert(self.union(t).contains(preimage));
            } else {
                assert(t.map(f).contains(elem));
                let preimage = choose|preimage: A| t.contains(preimage) && f(preimage) == elem;
                assert(self.union(t).contains(preimage));
            }
        }
    }

    /// Utility function for more concise universal quantification over sets
    pub open spec fn all(&self, pred: spec_fn(A) -> bool) -> bool {
        forall|x: A| self.contains(x) ==> pred(x)
    }

    /// Utility function for more concise existential quantification over sets
    pub open spec fn any(&self, pred: spec_fn(A) -> bool) -> bool {
        exists|x: A| self.contains(x) && pred(x)
    }

    /// `any` is preserved between predicates `p` and `q` if `p` implies `q`.
    pub broadcast proof fn lemma_any_map_preserved_pred<B>(
        self,
        p: spec_fn(A) -> bool,
        q: spec_fn(B) -> bool,
        f: spec_fn(A) -> B,
    )
        requires
            #[trigger] self.any(p),
            forall|x: A| #[trigger] p(x) ==> q(f(x)),
        ensures
            #[trigger] self.map(f).any(q),
    {
        let x = choose|x: A| self.contains(x) && p(x);
        assert(self.map(f).contains(f(x)));
    }

    /// Collecting all elements `b` where `f` returns `Some(b)`
    pub open spec fn filter_map<B>(self, f: spec_fn(A) -> Option<B>) -> ISet<B> {
        self.map(
            |elem: A|
                match f(elem) {
                    Option::Some(r) => iset!{r},
                    Option::None => iset!{},
                },
        ).flatten()
    }

    /// Inserting commutes with `filter_map`
    pub broadcast proof fn lemma_filter_map_insert<B>(
        s: ISet<A>,
        f: spec_fn(A) -> Option<B>,
        elem: A,
    )
        ensures
            #[trigger] s.insert(elem).filter_map(f) == (match f(elem) {
                Some(res) => s.filter_map(f).insert(res),
                None => s.filter_map(f),
            }),
    {
        broadcast use group_iset_lemmas;
        broadcast use ISet::lemma_iset_map_insert_commute;

        let lhs = s.insert(elem).filter_map(f);
        let rhs = match f(elem) {
            Some(res) => s.filter_map(f).insert(res),
            None => s.filter_map(f),
        };
        let to_set = |elem: A|
            match f(elem) {
                Option::Some(r) => iset!{r},
                Option::None => iset!{},
            };
        assert forall|r: B| #[trigger] lhs.contains(r) implies rhs.contains(r) by {
            if f(elem) != Some(r) {
                let orig = choose|orig: A| #[trigger]
                    s.contains(orig) && f(orig) == Option::Some(r);
                assert(to_set(orig) == iset!{r});
                assert(s.map(to_set).contains(to_set(orig)));
            }
        }
        assert forall|r: B| #[trigger] rhs.contains(r) implies lhs.contains(r) by {
            if Some(r) == f(elem) {
                assert(s.insert(elem).map(to_set).contains(to_set(elem)));
            } else {
                let orig = choose|orig: A| #[trigger]
                    s.contains(orig) && f(orig) == Option::Some(r);
                assert(s.insert(elem).map(to_set).contains(to_set(orig)));
            }
        }
        assert(lhs =~= rhs);
    }

    /// `filter_map` and `union` commute.
    pub broadcast proof fn lemma_filter_map_union<B>(self, f: spec_fn(A) -> Option<B>, t: ISet<A>)
        ensures
            #[trigger] self.union(t).filter_map(f) == self.filter_map(f).union(t.filter_map(f)),
    {
        broadcast use group_iset_lemmas;

        let lhs = self.union(t).filter_map(f);
        let rhs = self.filter_map(f).union(t.filter_map(f));
        let to_set = |elem: A|
            match f(elem) {
                Option::Some(r) => iset!{r},
                Option::None => iset!{},
            };

        assert forall|elem: B| rhs.contains(elem) implies lhs.contains(elem) by {
            if self.filter_map(f).contains(elem) {
                let x = choose|x: A| self.contains(x) && f(x) == Option::Some(elem);
                assert(self.union(t).contains(x));
                assert(self.union(t).map(to_set).contains(to_set(x)));
            }
            if t.filter_map(f).contains(elem) {
                let x = choose|x: A| t.contains(x) && f(x) == Option::Some(elem);
                assert(self.union(t).contains(x));
                assert(self.union(t).map(to_set).contains(to_set(x)));
            }
        }
        assert forall|elem: B| lhs.contains(elem) implies rhs.contains(elem) by {
            let x = choose|x: A| self.union(t).contains(x) && f(x) == Option::Some(elem);
            if self.contains(x) {
                assert(self.map(to_set).contains(to_set(x)));
                assert(self.filter_map(f).contains(elem));
            } else {
                assert(t.contains(x));
                assert(t.map(to_set).contains(to_set(x)));
                assert(t.filter_map(f).contains(elem));
            }
        }
        assert(lhs =~= rhs);
    }

    /// `map` preserves finiteness
    pub proof fn lemma_map_finite<B>(self, f: spec_fn(A) -> B)
        requires
            self.finite(),
        ensures
            self.map(f).finite(),
            self.map(f).len() <= self.len(),
        decreases self.len(),
    {
        broadcast use group_iset_lemmas;
        broadcast use lemma_iset_empty_equivalency_len;

        if self.len() == 0 {
            assert(forall|elem: A| !(#[trigger] self.contains(elem)));
            assert forall|res: B| #[trigger] self.map(f).contains(res) implies false by {
                let x = choose|x: A| self.contains(x) && f(x) == res;
            }
            assert(self.map(f) =~= ISet::<B>::empty());
        } else {
            let x = choose|x: A| self.contains(x);
            assert(self.map(f).contains(f(x)));
            self.remove(x).lemma_map_finite(f);
            assert(self.remove(x).insert(x) == self);
            assert(self.map(f) == self.remove(x).map(f).insert(f(x)));
        }
    }

    /// `map_by` preserves finiteness.
    pub broadcast proof fn lemma_map_by_finite<B>(self, fwd: spec_fn(A) -> B, rev: spec_fn(B) -> A)
        requires
            self.finite(),
        ensures
            #[trigger] self.map_by(fwd, rev).finite(),
    {
        broadcast use lemma_iset_subset_finite;

        assert(self.map_by(fwd, rev).subset_of(self.map(fwd)));
        self.lemma_map_finite(fwd);
    }

    /// `map_flatten_by` preserves finiteness.
    pub broadcast proof fn lemma_map_flatten_by_finite<B>(
        self,
        fwd: spec_fn(A) -> ISet<B>,
        rev: spec_fn(B) -> A,
    )
        requires
            self.finite(),
            forall|a: A| self.contains(a) ==> fwd(a).finite(),
        ensures
            #[trigger] self.map_flatten_by(fwd, rev).finite(),
    {
        broadcast use lemma_iset_subset_finite;

        let s1 = self.map_flatten_by(fwd, rev);
        let s2 = self.map(fwd).flatten();
        assert forall|b: B| s1.contains(b) implies s2.contains(b) by {
            assert(self.map(fwd).contains(fwd(rev(b))));
        }
        assert(s1.subset_of(s2));
        self.lemma_map_finite(fwd);
        self.map(fwd).lemma_flatten_finite();
    }

    /// If `self` is a subset of `s2`, and all elements of `s2`
    /// satisfy predicate `p`, then all elements of `self` satisfy
    /// predicate `p`.
    pub broadcast proof fn lemma_iset_all_subset(self, s2: ISet<A>, p: spec_fn(A) -> bool)
        requires
            #[trigger] self.subset_of(s2),
            s2.all(p),
        ensures
            #[trigger] self.all(p),
    {
        broadcast use group_iset_lemmas;

    }

    /// `filter_map` preserves finiteness.
    pub broadcast proof fn lemma_filter_map_finite<B>(self, f: spec_fn(A) -> Option<B>)
        requires
            self.finite(),
        ensures
            #[trigger] self.filter_map(f).finite(),
        decreases self.len(),
    {
        broadcast use group_iset_lemmas;
        broadcast use ISet::lemma_filter_map_insert;

        let mapped = self.filter_map(f);
        if self.len() == 0 {
            assert(self.filter_map(f) =~= ISet::<B>::empty());
        } else {
            let elem = self.choose();
            self.remove(elem).lemma_filter_map_finite(f);
            assert(self =~= self.remove(elem).insert(elem));
        }
    }

    /// Conversion to a sequence and back to a set is the identity function.
    pub broadcast proof fn lemma_to_seq_to_set_id(self)
        requires
            self.finite(),
        ensures
            #[trigger] self.to_seq().to_set().to_iset() =~= self,
        decreases self.len(),
    {
        broadcast use group_set_lemmas;
        broadcast use group_iset_lemmas;
        broadcast use lemma_iset_empty_equivalency_len;
        broadcast use super::seq_lib::group_seq_lib_default;
        broadcast use super::seq_lib::group_seq_properties;

        if self.len() == 0 {
            assert(self.to_seq().to_set().to_iset() =~= ISet::<A>::empty());
        } else {
            let elem = self.choose();
            self.remove(elem).lemma_to_seq_to_set_id();
            assert(self =~= self.remove(elem).insert(elem));
            assert(self.to_seq().to_set() =~= self.remove(elem).to_seq().to_set().insert(elem));
        }
    }

    /// Any sequence converted from finite iset has no duplicates
    pub broadcast proof fn lemma_to_seq_no_duplicates(self)
        requires
            self.finite(),
        ensures
            #[trigger] self.to_seq().no_duplicates(),
        decreases self.len(),
    {
        broadcast use super::seq::group_seq_axioms;

        if self.len() == 0 {
        } else {
            let x = choose|x: A| #[trigger]
                self.contains(x) && self.to_seq() =~= seq![x] + self.remove(x).to_seq();
            let seq = self.to_seq();
            let seq2 = self.remove(x).to_seq();
            assert(seq2.no_duplicates()) by { self.remove(x).lemma_to_seq_no_duplicates() }
            assert(seq2.to_set().to_iset() == self.remove(x)) by {
                self.remove(x).lemma_to_seq_to_set_id();
            }
            assert(!seq2.contains(x)) by { seq2.to_set_ensures() }
        }
    }

    /// Conversion from finite iset to seq preserves the length
    pub broadcast proof fn lemma_to_seq_len(self)
        requires
            self.finite(),
        ensures
            #[trigger] self.to_seq().len() == self.len(),
        decreases self.len(),
    {
        broadcast use super::seq::group_seq_axioms;

        if self.len() == 0 {
        } else {
            let x = choose|x: A| #[trigger]
                self.contains(x) && self.to_seq() =~= seq![x] + self.remove(x).to_seq();
            self.remove(x).lemma_to_seq_len();
        }
    }
}

impl<A> ISet<ISet<A>> {
    /// This function creates a set from all the elements of all the elements
    /// of `self`.
    pub open spec fn flatten(self) -> ISet<A> {
        ISet::new(
            |elem|
                exists|elem_s: ISet<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem),
        )
    }

    /// Flattening then unioning with another set is equivalent to
    /// inserting that other set and then flattening.
    pub broadcast proof fn flatten_insert_union_commute(self, other: ISet<A>)
        ensures
            self.flatten().union(other) =~= #[trigger] self.insert(other).flatten(),
    {
        broadcast use group_iset_lemmas;

        let lhs = self.flatten().union(other);
        let rhs = self.insert(other).flatten();

        assert forall|elem: A| lhs.contains(elem) implies rhs.contains(elem) by {
            if exists|s: ISet<A>| self.contains(s) && s.contains(elem) {
                let s = choose|s: ISet<A>| self.contains(s) && s.contains(elem);
                assert(self.insert(other).contains(s));
                assert(s.contains(elem));
            } else {
                assert(self.insert(other).contains(other));
            }
        }
    }

    /// If `self` is finite and all its elements are finite, then `self.flatten()`
    /// is also finite.
    pub proof fn lemma_flatten_finite(self)
        requires
            self.finite(),
            forall|s: ISet<A>| self.contains(s) ==> #[trigger] s.finite(),
        ensures
            self.flatten().finite(),
        decreases self.len(),
    {
        broadcast use group_iset_lemmas;

        if self.len() == 0 {
            assert(self.flatten() =~= ISet::<A>::empty());
        } else {
            let s = self.choose();
            let self2 = self.remove(s);
            self2.lemma_flatten_finite();
            self2.flatten_insert_union_commute(s);
        }
    }
}

/// Two sets are equal iff mapping `f` results in equal sets, if `f` is injective.
pub proof fn lemma_isets_eq_iff_injective_map_eq<T, S>(s1: ISet<T>, s2: ISet<T>, f: spec_fn(T) -> S)
    requires
        super::relations::injective(f),
    ensures
        (s1 == s2) <==> (s1.map(f) == s2.map(f)),
{
    broadcast use group_iset_lemmas;

    if (s1.map(f) == s2.map(f)) {
        assert(s1.map(f).len() == s2.map(f).len());
        if !s1.subset_of(s2) {
            let x = choose|x: T| s1.contains(x) && !s2.contains(x);
            assert(s1.map(f).contains(f(x)));
        } else if !s2.subset_of(s1) {
            let x = choose|x: T| s2.contains(x) && !s1.contains(x);
            assert(s2.map(f).contains(f(x)));
        }
        assert(s1 =~= s2);
    }
}

/// Two sets are equal iff applying an injective (in the union of the sets) function `f` to each set produces equal sets.
pub proof fn lemma_isets_eq_iff_injective_map_on_eq<T, S>(
    s1: ISet<T>,
    s2: ISet<T>,
    f: spec_fn(T) -> S,
)
    requires
        (s1 + s2).injective_on(f),
    ensures
        (s1 == s2) <==> (s1.map(f) == s2.map(f)),
{
    broadcast use group_iset_lemmas;

    if (s1.map(f) == s2.map(f)) {
        assert(s1.map(f).len() == s2.map(f).len());
        if !s1.subset_of(s2) {
            let x = choose|x: T| s1.contains(x) && !s2.contains(x);
            assert(s1.map(f).contains(f(x)));
        } else if !s2.subset_of(s1) {
            let x = choose|x: T| s2.contains(x) && !s1.contains(x);
            assert(s2.map(f).contains(f(x)));
        }
        assert(s1 =~= s2);
    }
}

/// The result of inserting an element `a` into a set `s` is finite iff `s` is finite.
pub broadcast proof fn lemma_iset_insert_finite_iff<A>(s: ISet<A>, a: A)
    ensures
        #[trigger] s.insert(a).finite() <==> s.finite(),
{
    if s.insert(a).finite() {
        if s.contains(a) {
            assert(s == s.insert(a));
        } else {
            assert(s == s.insert(a).remove(a));
        }
    }
    assert(s.insert(a).finite() ==> s.finite());
}

/// The result of removing an element `a` into a set `s` is finite iff `s` is finite.
pub broadcast proof fn lemma_iset_remove_finite_iff<A>(s: ISet<A>, a: A)
    ensures
        #[trigger] s.remove(a).finite() <==> s.finite(),
{
    if s.remove(a).finite() {
        if s.contains(a) {
            assert(s == s.remove(a).insert(a));
        } else {
            assert(s == s.remove(a));
        }
    }
}

/// The union of two sets is finite iff both sets are finite.
pub broadcast proof fn lemma_iset_union_finite_iff<A>(s1: ISet<A>, s2: ISet<A>)
    ensures
        #[trigger] s1.union(s2).finite() <==> s1.finite() && s2.finite(),
{
    if s1.union(s2).finite() {
        lemma_iset_union_finite_implies_sets_finite(s1, s2);
    }
}

/// If the union of two `ISet`s is finite, then each of those `ISet`s
/// is also finite.
pub proof fn lemma_iset_union_finite_implies_sets_finite<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s1.union(s2).finite(),
    ensures
        s1.finite(),
        s2.finite(),
    decreases s1.union(s2).len(),
{
    if s1.union(s2) =~= ISet::<A>::empty() {
        assert(s1 =~= ISet::<A>::empty());
        assert(s2 =~= ISet::<A>::empty());
    } else {
        let a = s1.union(s2).choose();
        assert(s1.remove(a).union(s2.remove(a)) == s1.union(s2).remove(a));
        lemma_iset_remove_len(s1.union(s2), a);
        lemma_iset_union_finite_implies_sets_finite(s1.remove(a), s2.remove(a));
        assert(forall|s: ISet<A>|
            #![auto]
            s.remove(a).insert(a) == if s.contains(a) {
                s
            } else {
                s.insert(a)
            });
        lemma_iset_insert_finite_iff(s1, a);
        lemma_iset_insert_finite_iff(s2, a);
    }
}

/// The size of a union of two sets is less than or equal to the size of
/// both individual sets combined.
pub proof fn lemma_len_union<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s1.finite(),
        s2.finite(),
    ensures
        s1.union(s2).len() <= s1.len() + s2.len(),
    decreases s1.len(),
{
    if s1.is_empty() {
        assert(s1.union(s2) =~= s2);
    } else {
        let a = s1.choose();
        if s2.contains(a) {
            assert(s1.union(s2) =~= s1.remove(a).union(s2));
        } else {
            assert(s1.union(s2).remove(a) =~= s1.remove(a).union(s2));
        }
        lemma_len_union::<A>(s1.remove(a), s2);
    }
}

/// The size of a union of two sets is greater than or equal to the size of
/// both individual sets.
pub proof fn lemma_len_union_ind<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s1.finite(),
        s2.finite(),
    ensures
        s1.union(s2).len() >= s1.len(),
        s1.union(s2).len() >= s2.len(),
    decreases s2.len(),
{
    broadcast use group_iset_properties;

    if s2.len() == 0 {
    } else {
        let y = choose|y: A| s2.contains(y);
        if s1.contains(y) {
            assert(s1.remove(y).union(s2.remove(y)) =~= s1.union(s2).remove(y));
            lemma_len_union_ind(s1.remove(y), s2.remove(y))
        } else {
            assert(s1.union(s2.remove(y)) =~= s1.union(s2).remove(y));
            lemma_len_union_ind(s1, s2.remove(y))
        }
    }
}

/// The size of the intersection of finite set `s1` and set `s2` is less than or equal to the size of `s1`.
pub proof fn lemma_len_intersect<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s1.finite(),
    ensures
        s1.intersect(s2).len() <= s1.len(),
    decreases s1.len(),
{
    if s1.is_empty() {
        assert(s1.intersect(s2) =~= s1);
    } else {
        let a = s1.choose();
        assert(s1.intersect(s2).remove(a) =~= s1.remove(a).intersect(s2));
        lemma_len_intersect::<A>(s1.remove(a), s2);
    }
}

/// If `s1` is a subset of finite set `s2`, then the size of `s1` is less than or equal to
/// the size of `s2` and `s1` must be finite.
pub proof fn lemma_len_subset<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s2.finite(),
        s1.subset_of(s2),
    ensures
        s1.len() <= s2.len(),
        s1.finite(),
{
    lemma_len_intersect::<A>(s2, s1);
    assert(s2.intersect(s1) =~= s1);
}

/// A subset of a finite set `s` is finite.
pub broadcast proof fn lemma_iset_subset_finite<A>(s: ISet<A>, sub: ISet<A>)
    requires
        s.finite(),
        sub.subset_of(s),
    ensures
        #![trigger sub.subset_of(s)]
        sub.finite(),
{
    let complement = s.difference(sub);
    assert(sub =~= s.difference(complement));
}

/// The size of the difference of finite set `s1` and set `s2` is less than or equal to the size of `s1`.
pub proof fn lemma_len_difference<A>(s1: ISet<A>, s2: ISet<A>)
    requires
        s1.finite(),
    ensures
        s1.difference(s2).len() <= s1.len(),
    decreases s1.len(),
{
    if s1.is_empty() {
        assert(s1.difference(s2) =~= s1);
    } else {
        let a = s1.choose();
        assert(s1.difference(s2).remove(a) =~= s1.remove(a).difference(s2));
        lemma_len_difference::<A>(s1.remove(a), s2);
    }
}

/// Creates a finite set of integers in the range [lo, hi).
pub open spec fn set_int_range(lo: int, hi: int) -> ISet<int> {
    ISet::new(|i: int| lo <= i && i < hi)
}

/// If a set solely contains integers in the range [a, b), then its size is
/// bounded by b - a.
pub proof fn lemma_int_range(lo: int, hi: int)
    requires
        lo <= hi,
    ensures
        set_int_range(lo, hi).finite(),
        set_int_range(lo, hi).len() == hi - lo,
    decreases hi - lo,
{
    if lo == hi {
        assert(set_int_range(lo, hi) =~= ISet::empty());
    } else {
        lemma_int_range(lo, hi - 1);
        assert(set_int_range(lo, hi - 1).insert(hi - 1) =~= set_int_range(lo, hi));
    }
}

/// If x is a subset of y and the size of x is equal to the size of y, x is equal to y.
pub proof fn lemma_subset_equality<A>(x: ISet<A>, y: ISet<A>)
    requires
        x.subset_of(y),
        x.finite(),
        y.finite(),
        x.len() == y.len(),
    ensures
        x =~= y,
    decreases x.len(),
{
    broadcast use group_iset_properties;

    if x =~= ISet::<A>::empty() {
    } else {
        let e = x.choose();
        lemma_subset_equality(x.remove(e), y.remove(e));
    }
}

/// If an injective function is applied to each element of a set to construct
/// another set, the two sets have the same size.
pub proof fn lemma_map_size<A, B>(x: ISet<A>, y: ISet<B>, f: spec_fn(A) -> B)
    requires
        x.finite(),
        x.injective_on(f),
        x.map(f) == y,
    ensures
        y.finite(),
        x.len() == y.len(),
    decreases x.len(),
{
    broadcast use group_iset_properties;

    if x.len() == 0 {
        if !y.is_empty() {
            let e = y.choose();
        }
    } else {
        let a = x.choose();
        assert(x.remove(a).map(f) == y.remove(f(a)));
        lemma_map_size(x.remove(a), y.remove(f(a)), f);
        assert(y == y.remove(f(a)).insert(f(a)));
    }
}

/// If any function is applied to each element of a set to construct
/// another set, the constructed set's length is at most the original's
pub proof fn lemma_map_size_bound<A, B>(x: ISet<A>, y: ISet<B>, f: spec_fn(A) -> B)
    requires
        x.finite(),
        x.map(f) == y,
    ensures
        y.finite(),
        y.len() <= x.len(),
    decreases x.len(),
{
    broadcast use group_iset_properties;

    if x.is_empty() {
        if !y.is_empty() {
            let e = y.choose();
        }
    } else {
        let xx = x.choose();
        let img = f(xx);
        let pre = x.filter(|a: A| f(a) == f(xx));
        x.lemma_len_filter(|a: A| f(a) == f(xx));
        let wit = choose|a: A| x.contains(a) && f(a) == f(xx);
        assert forall|b: B| (#[trigger] y.remove(f(xx)).contains(b)) implies exists|a: A|
            x.difference(pre).contains(a) && f(a) == b by {
            let pre_wit = choose|a: A| x.contains(a) && f(a) == b;
            assert(x.difference(pre).contains(pre_wit));
        }

        assert(x == x.difference(pre).union(pre));
        assert(y == y.remove(f(xx)).insert(f(xx)));
        assert(x.difference(pre).map(f) == y.remove(f(xx)));
        lemma_map_size_bound(x.difference(pre), y.remove(f(xx)), f);
    }
}

// This verified lemma used to be an axiom in the Dafny prelude
/// Taking the union of sets `a` and `b` and then taking the union of the result with `b`
/// is the same as taking the union of `a` and `b` once.
pub broadcast proof fn lemma_iset_union_again1<A>(a: ISet<A>, b: ISet<A>)
    ensures
        #[trigger] a.union(b).union(b) =~= a.union(b),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
/// Taking the union of sets `a` and `b` and then taking the union of the result with `a`
/// is the same as taking the union of `a` and `b` once.
pub broadcast proof fn lemma_iset_union_again2<A>(a: ISet<A>, b: ISet<A>)
    ensures
        #[trigger] a.union(b).union(a) =~= a.union(b),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
/// Taking the intersection of sets `a` and `b` and then taking the intersection of the result with `b`
/// is the same as taking the intersection of `a` and `b` once.
pub broadcast proof fn lemma_iset_intersect_again1<A>(a: ISet<A>, b: ISet<A>)
    ensures
        #![trigger (a.intersect(b)).intersect(b)]
        (a.intersect(b)).intersect(b) =~= a.intersect(b),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
/// Taking the intersection of sets `a` and `b` and then taking the intersection of the result with `a`
/// is the same as taking the intersection of `a` and `b` once.
pub broadcast proof fn lemma_iset_intersect_again2<A>(a: ISet<A>, b: ISet<A>)
    ensures
        #![trigger (a.intersect(b)).intersect(a)]
        (a.intersect(b)).intersect(a) =~= a.intersect(b),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
/// If set `s2` contains element `a`, then the set difference of `s1` and `s2` does not contain `a`.
pub broadcast proof fn lemma_iset_difference2<A>(s1: ISet<A>, s2: ISet<A>, a: A)
    ensures
        #![trigger s1.difference(s2).contains(a)]
        s2.contains(a) ==> !s1.difference(s2).contains(a),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
/// If sets `a` and `b` are disjoint, meaning they have no elements in common, then the set difference
/// of `a + b` and `b` is equal to `a` and the set difference of `a + b` and `a` is equal to `b`.
pub broadcast proof fn lemma_iset_disjoint<A>(a: ISet<A>, b: ISet<A>)
    ensures
        #![trigger (a + b).difference(a)]  //TODO: this might be too free
        a.disjoint(b) ==> ((a + b).difference(a) =~= b && (a + b).difference(b) =~= a),
{
}

// This verified lemma used to be an axiom in the Dafny prelude
// Dafny encodes the second clause with a single directional, although
// it should be fine with both directions?
// REVIEW: excluded from broadcast group if trigger is too free
//         also not that some proofs in seq_lib requires this lemma
/// ISet `s` has length 0 if and only if it is equal to the empty set. If `s` has length greater than 0,
/// Then there must exist an element `x` such that `s` contains `x`.
pub broadcast proof fn lemma_iset_empty_equivalency_len<A>(s: ISet<A>)
    requires
        s.finite(),
    ensures
        #![trigger s.len()]
        (s.len() == 0 <==> s == ISet::<A>::empty()) && (s.len() != 0 ==> exists|x: A|
            s.contains(x)),
{
    assert(s.len() == 0 ==> s =~= ISet::empty()) by {
        if s.len() == 0 {
            assert(forall|a: A| !(ISet::empty().contains(a)));
            assert(ISet::<A>::empty().len() == 0);
            assert(ISet::<A>::empty().len() == s.len());
            assert((exists|a: A| s.contains(a)) || (forall|a: A| !s.contains(a)));
            if exists|a: A| s.contains(a) {
                let a = s.choose();
                assert(s.remove(a).len() == s.len() - 1) by {
                    lemma_iset_remove_len(s, a);
                }
            }
        }
    }
    assert(s.len() == 0 <== s =~= ISet::empty());
}

// This verified lemma used to be an axiom in the Dafny prelude
/// If sets `a` and `b` are disjoint, meaning they share no elements in common, then the length
/// of the union `a + b` is equal to the sum of the lengths of `a` and `b`.
pub broadcast proof fn lemma_iset_disjoint_lens<A>(a: ISet<A>, b: ISet<A>)
    requires
        a.finite(),
        b.finite(),
    ensures
        a.disjoint(b) ==> #[trigger] (a + b).len() == a.len() + b.len(),
    decreases a.len(),
{
    if a.len() == 0 {
        lemma_iset_empty_equivalency_len(a);
        assert(a + b =~= b);
    } else {
        if a.disjoint(b) {
            let x = a.choose();
            assert(a.remove(x) + b =~= (a + b).remove(x));
            lemma_iset_disjoint_lens(a.remove(x), b);
        }
    }
}

/// Two sets are disjoint iff their intersection is empty
pub proof fn lemma_iset_disjoint_iff_empty_intersection<T>(a: ISet<T>, b: ISet<T>)
    ensures
        a.disjoint(b) <==> a.intersect(b).is_empty(),
{
    broadcast use group_iset_properties;

    if a.disjoint(b) {
        assert(b.disjoint(a));
        assert(forall|x: T| a.contains(x) ==> !(a.contains(x) && b.contains(x)));
        assert(forall|x: T| b.contains(x) ==> !(a.contains(x) && b.contains(x)));
        assert(forall|x: T| !a.intersect(b).contains(x));
    }
    if a.intersect(b).is_empty() {
        assert(forall|x: T| !a.intersect(b).contains(x));
        if !a.disjoint(b) {
            assert(exists|x: T| a.contains(x) && b.contains(x));
            let x = choose|x: T| a.contains(x) && b.contains(x);
            assert(a.intersect(b).contains(x));
            assert(!a.intersect(b).is_empty());
        }
    }
}

// This verified lemma used to be an axiom in the Dafny prelude
/// The length of the union between two sets added to the length of the intersection between the
/// two sets is equal to the sum of the lengths of the two sets.
pub broadcast proof fn lemma_iset_intersect_union_lens<A>(a: ISet<A>, b: ISet<A>)
    requires
        a.finite(),
        b.finite(),
    ensures
        #[trigger] (a + b).len() + #[trigger] a.intersect(b).len() == a.len() + b.len(),
    decreases a.len(),
{
    if a.len() == 0 {
        lemma_iset_empty_equivalency_len(a);
        assert(a + b =~= b);
        assert(a.intersect(b) =~= ISet::empty());
        assert(a.intersect(b).len() == 0);
    } else {
        let x = a.choose();
        lemma_iset_intersect_union_lens(a.remove(x), b);
        if (b.contains(x)) {
            assert(a.remove(x) + b =~= (a + b));
            assert(a.intersect(b).remove(x) =~= a.remove(x).intersect(b));
        } else {
            assert(a.remove(x) + b =~= (a + b).remove(x));
            assert(a.remove(x).intersect(b) =~= a.intersect(b));
        }
    }
}

// This verified lemma used to be an axiom in the Dafny prelude
/// The length of the set difference `A \ B` added to the length of the set difference `B \ A` added to
/// the length of the intersection `A ∩ B` is equal to the length of the union `A + B`.
///
/// The length of the set difference `A \ B` is equal to the length of `A` minus the length of the
/// intersection `A ∩ B`.
pub broadcast proof fn lemma_iset_difference_len<A>(a: ISet<A>, b: ISet<A>)
    requires
        a.finite(),
        b.finite(),
    ensures
        (#[trigger] a.difference(b).len() + b.difference(a).len() + a.intersect(b).len() == (a
            + b).len()) && (a.difference(b).len() == a.len() - a.intersect(b).len()),
    decreases a.len(),
{
    if a.len() == 0 {
        lemma_iset_empty_equivalency_len(a);
        assert(a.difference(b) =~= ISet::empty());
        assert(b.difference(a) =~= b);
        assert(a.intersect(b) =~= ISet::empty());
        assert(a + b =~= b);
    } else {
        let x = a.choose();
        lemma_iset_difference_len(a.remove(x), b);
        if b.contains(x) {
            assert(a.intersect(b).remove(x) =~= a.remove(x).intersect(b));
            assert(a.remove(x).difference(b) =~= a.difference(b));
            assert(b.difference(a.remove(x)).remove(x) =~= b.difference(a));
            assert(a.remove(x) + b =~= a + b);
        } else {
            assert(a.remove(x) + b =~= (a + b).remove(x));
            assert(a.remove(x).difference(b) =~= a.difference(b).remove(x));
            assert(b.difference(a.remove(x)) =~= b.difference(a));
            assert(a.remove(x).intersect(b) =~= a.intersect(b));
        }
    }
}

pub broadcast group group_iset_properties {
    lemma_iset_union_again1,
    lemma_iset_union_again2,
    lemma_iset_intersect_again1,
    lemma_iset_intersect_again2,
    lemma_iset_difference2,
    lemma_iset_disjoint,
    lemma_iset_disjoint_lens,
    lemma_iset_intersect_union_lens,
    lemma_iset_difference_len,
    // REVIEW: exclude from broadcast group if trigger is too free
    //         also note that some proofs in seq_lib requires this lemma
    lemma_iset_empty_equivalency_len,
}

pub broadcast axiom fn axiom_iset_is_empty<A>(s: ISet<A>)
    requires
        !(#[trigger] s.is_empty()),
    ensures
        exists|a: A|
            s.contains(
                a,
            ),
// REVIEW, should this be in `set`, or have a proof?

;

pub broadcast proof fn lemma_iset_is_empty_len0<A>(s: ISet<A>)
    ensures
        #[trigger] s.is_empty() <==> (s.finite() && s.len() == 0),
{
}

#[doc(hidden)]
#[verifier::inline]
pub open spec fn check_argument_is_set<A>(s: ISet<A>) -> ISet<A> {
    s
}

/// Prove two sets equal by extensionality. Usage is:
///
/// ```rust
/// assert_isets_equal!(set1 == set2);
/// ```
///
/// or,
///
/// ```rust
/// assert_isets_equal!(set1 == set2, elem => {
///     // prove that set1.contains(elem) iff set2.contains(elem)
/// });
/// ```
#[macro_export]
macro_rules! assert_isets_equal {
    [$($tail:tt)*] => {
        $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::iset_lib::assert_isets_equal_internal!($($tail)*))
    };
}

#[macro_export]
#[doc(hidden)]
macro_rules! assert_isets_equal_internal {
    (::vstd::prelude::spec_eq($s1:expr, $s2:expr)) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2)
    };
    (::vstd::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
    };
    (crate::prelude::spec_eq($s1:expr, $s2:expr)) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2)
    };
    (crate::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
    };
    (crate::verus_builtin::spec_eq($s1:expr, $s2:expr)) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2)
    };
    (crate::verus_builtin::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock)
    };
    ($s1:expr, $s2:expr $(,)?) => {
        $crate::vstd::iset_lib::assert_isets_equal_internal!($s1, $s2, elem => { })
    };
    ($s1:expr, $s2:expr, $elem:ident $( : $t:ty )? => $bblock:block) => {
        #[verifier::spec] let s1 = $crate::vstd::iset_lib::check_argument_is_set($s1);
        #[verifier::spec] let s2 = $crate::vstd::iset_lib::check_argument_is_set($s2);
        $crate::vstd::prelude::assert_by($crate::vstd::prelude::equal(s1, s2), {
            $crate::vstd::prelude::assert_forall_by(|$elem $( : $t )?| {
                $crate::vstd::prelude::ensures(
                    $crate::vstd::prelude::imply(s1.contains($elem), s2.contains($elem))
                    &&
                    $crate::vstd::prelude::imply(s2.contains($elem), s1.contains($elem))
                );
                { $bblock }
            });
            $crate::vstd::prelude::assert_($crate::vstd::prelude::ext_equal(s1, s2));
        });
    }
}

pub broadcast group group_iset_lib_default {
    axiom_iset_is_empty,
    lemma_iset_is_empty_len0,
    lemma_iset_subset_finite,
    ISet::lemma_map_by_finite,
    ISet::lemma_map_flatten_by_finite,
}

pub use assert_isets_equal_internal;
pub use assert_isets_equal;

} // verus!