Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
12345678910111213141516171819202122232425262728293031323334353637383940414243444546474849505152535455565758596061626364656667686970717273747576777879808182838485868788899091929394959697989910010110210310410510610710810911011111211311411511611711811912012112212312412512612712812913013113213313413513613713813914014114214314414514614714814915015115215315415515615715815916016116216316416516616716816917017117217317417517617717817918018118218318418518618718818919019119219319419519619719819920020120220320420520620720820921021121221321421521621721821922022122222322422522622722822923023123223323423523623723823924024124224324424524624724824925025125225325425525625725825926026126226326426526626726826927027127227327427527627727827928028128228328428528628728828929029129229329429529629729829930030130230330430530630730830931031131231331431531631731831932032132232332432532632732832933033133233333433533633733833934034134234334434534634734834935035135235335435535635735835936036136236336436536636736836937037137237337437537637737837938038138238338438538638738838939039139239339439539639739839940040140240340440540640740840941041141241341441541641741841942042142242342442542642742842943043143243343443543643743843944044144244344444544644744844945045145245345445545645745845946046146246346446546646746846947047147247347447547647747847948048148248348448548648748848949049149249349449549649749849950050150250350450550650750850951051151251351451551651751851952052152252352452552652752852953053153253353453553653753853954054154254354454554654754854955055155255355455555655755855956056156256356456556656756856957057157257357457557657757857958058158258358458558658758858959059159259359459559659759859960060160260360460560660760860961061161261361461561661761861962062162262362462562662762862963063163263363463563663763863964064164264364464564664764864965065165265365465565665765865966066166266366466566666766866967067167267367467567667767867968068168268368468568668768868969069169269369469569669769869970070170270370470570670770870971071171271371471571671771871972072172272372472572672772872973073173273373473573673773873974074174274374474574674774874975075175275375475575675775875976076176276376476576676776876977077177277377477577677777877978078178278378478578678778878979079179279379479579679779879980080180280380480580680780880981081181281381481581681781881982082182282382482582682782882983083183283383483583683783883984084184284384484584684784884985085185285385485585685785885986086186286386486586686786886987087187287387487587687787887988088188288388488588688788888989089189289389489589689789889990090190290390490590690790890991091191291391491591691791891992092192292392492592692792892993093193293393493593693793893994094194294394494594694794894995095195295395495595695795895996096196296396496596696796896997097197297397497597697797897998098198298398498598698798898999099199299399499599699799899910001001100210031004100510061007100810091010101110121013101410151016101710181019102010211022102310241025102610271028102910301031103210331034103510361037103810391040104110421043104410451046104710481049105010511052105310541055105610571058105910601061106210631064106510661067106810691070107110721073107410751076107710781079108010811082108310841085108610871088108910901091109210931094109510961097109810991100110111021103110411051106110711081109111011111112111311141115111611171118111911201121112211231124112511261127112811291130113111321133113411351136113711381139114011411142114311441145114611471148114911501151115211531154115511561157115811591160116111621163116411651166116711681169117011711172117311741175117611771178117911801181118211831184118511861187118811891190119111921193119411951196119711981199120012011202120312041205120612071208120912101211121212131214121512161217121812191220122112221223122412251226122712281229123012311232123312341235123612371238123912401241124212431244124512461247124812491250125112521253125412551256125712581259126012611262126312641265126612671268126912701271127212731274127512761277127812791280128112821283128412851286128712881289129012911292129312941295129612971298129913001301130213031304130513061307130813091310131113121313131413151316131713181319132013211322132313241325132613271328132913301331133213331334133513361337133813391340134113421343134413451346134713481349135013511352135313541355135613571358135913601361136213631364136513661367136813691370137113721373137413751376137713781379138013811382138313841385138613871388138913901391139213931394139513961397139813991400140114021403140414051406140714081409141014111412141314141415141614171418141914201421142214231424142514261427142814291430143114321433143414351436143714381439144014411442144314441445144614471448144914501451145214531454145514561457145814591460146114621463146414651466146714681469147014711472#[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, super::set::group_set_lemmas};
impl<A> Set<A> { /// 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 =~= Set::<A>::empty() }
/// Returns the set contains an element `f(x)` for every element `x` in `self`. pub closed spec fn map<B>(self, f: spec_fn(A) -> B) -> Set<B> { Set::new_from_iset(self.to_iset().map(f)).unwrap() }
/// Since `Self::map` is `closed`, this broadcast lemma is needed /// to make its semantics visible to the verifier. pub broadcast proof fn lemma_map_contains<B>(self, f: spec_fn(A) -> B, b: B) ensures #[trigger] self.map(f).contains(b) <==> exists|a: A| self.contains(a) && b == f(a), { self.to_iset().lemma_map_finite(f); }
/// `Set::map_by` is like `Set::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, `Set::map_by` can make proofs easier /// by avoiding the "exists" that appears in lemmas about `Set::map`. /// Example: for a set `s: Set<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 closed spec fn map_by<B>(self, fwd: spec_fn(A) -> B, rev: spec_fn(B) -> A) -> Set<B> recommends forall|a: A| self.contains(a) ==> rev(fwd(a)) == a, { Set::new_from_iset(self.to_iset().map_by(fwd, rev)).unwrap() }
/// Since `Self::map_by` is `closed`, this broadcast lemma is needed /// to make its semantics visible to the verifier. pub broadcast proof fn lemma_map_by_contains<B>( self, fwd: spec_fn(A) -> B, rev: spec_fn(B) -> A, b: B, ) ensures #[trigger] self.map_by(fwd, rev).contains(b) <==> self.contains(rev(b)) && b == fwd( rev(b), ), decreases self.len(), { self.to_iset().lemma_map_by_finite(fwd, rev); }
/// Similar to `Set::map_by`, but the forward function returns `Set<B>` rather than `B`, /// and `map_flatten_by` flattens the final result from `Set<Set<B>>` to just `Set<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 closed spec fn map_flatten_by<B>( self, fwd: spec_fn(A) -> Set<B>, rev: spec_fn(B) -> A, ) -> Set<B> recommends forall|a: A, b: B| #[trigger] self.contains(a) && fwd(a).contains(b) ==> #[trigger] rev(b) == a, { Set::new(|b: B| self.contains(rev(b)) && fwd(rev(b)).contains(b)).unwrap() }
/// This helper lemma demonstrates that the result of calling `Self::map_by` produces /// a finite, and thus valid, `Set`. proof fn lemma_map_flatten_by_finite<B>(self, fwd: spec_fn(A) -> Set<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 ISet::new(|b: B| self.contains(rev(b)) && fwd(rev(b)).contains(b)).finite(), decreases self.len(), { let map_f = |b: B| self.contains(rev(b)) && fwd(rev(b)).contains(b); if self == Self::empty() { assert(ISet::<B>::new(map_f) =~= ISet::<B>::empty()); } else { lemma_set_is_empty(self); let a: A = choose|a: A| self.contains(a); self.remove(a).lemma_map_flatten_by_finite(fwd, rev); let map_remove_f = |b: B| self.remove(a).contains(rev(b)) && fwd(rev(b)).contains(b); assert(ISet::<B>::new(map_f) =~= ISet::<B>::new(map_remove_f).union(fwd(a).to_iset())); lemma_to_iset_finite(fwd(a)); } }
/// Since `Self::map_flatten_by` is `closed`, this broadcast lemma is needed /// to make its semantics visible to the verifier. pub broadcast proof fn lemma_map_flatten_by_contains<B>( self, fwd: spec_fn(A) -> Set<B>, rev: spec_fn(B) -> A, b: B, ) requires forall|a: A, b: B| #[trigger] self.contains(a) && fwd(a).contains(b) ==> #[trigger] rev(b) == a, ensures #[trigger] self.map_flatten_by(fwd, rev).contains(b) <==> self.contains(rev(b)) && fwd( rev(b), ).contains(b), decreases self.len(), { self.lemma_map_flatten_by_finite(fwd, rev); }
/// 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) -> Set<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(), { broadcast use Set::lemma_flatten_contains; broadcast use Set::lemma_map_flatten_by_contains; broadcast use Set::lemma_map_contains;
self.lemma_map_flatten_by_finite(fwd, rev); 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: Set<B>| (exists|a: A| self.contains(a) && bs == fwd(a)) && #[trigger] 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> decreases self.len(), { 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 { self.to_iset().injective_on(r) }
/// 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.to_iset().has_least(leq, min) }
/// 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.to_iset().has_minimum(leq, min) }
/// 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.to_iset().has_greatest(leq, 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.to_iset().has_maximum(leq, 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), { self.to_iset().lemma_injective_on_subset(r, other.to_iset()); }
/// 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, decreases self.len(), { self.to_iset().find_unique_minimal(r) }
/// Proof of correctness and expected behavior for `Set::find_unique_minimal`. pub proof fn find_unique_minimal_ensures(self, r: spec_fn(A, A) -> bool) requires 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), { self.to_iset().find_unique_minimal_ensures(r); }
/// 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, { self.to_iset().find_unique_maximal(r) }
/// Proof of correctness and expected behavior for `Set::find_unique_maximal`. pub proof fn find_unique_maximal_ensures(self, r: spec_fn(A, A) -> bool) requires 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), { self.to_iset().find_unique_maximal_ensures(r); }
/// 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(), { 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.len() == 0, ensures self == Set::<A>::empty(), { if exists|a: A| self.contains(a) { // derive contradiction: assert(self.remove(self.choose()).len() + 1 == 0); } assert(self =~= Set::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_set_properties;
assert(self.remove(self.choose()) =~= Set::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: Set<A>) 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_set_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) ensures self.filter(f).len() <= self.len(), decreases self.len(), { if self.is_empty() { assert(self.filter(f) =~= self); } else { let a = self.choose(); assert(self.filter(f).remove(a) =~= self.remove(a).filter(f)); self.remove(a).lemma_len_filter(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), { self.to_iset().lemma_maximal_equivalent_greatest(r, 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), { self.to_iset().lemma_minimal_equivalent_least(r, min); }
/// 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, { self.to_iset().lemma_least_is_unique(r); }
/// 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, { self.to_iset().lemma_greatest_is_unique(r); }
/// 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, { self.to_iset().lemma_minimal_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 total_ordering(r), ensures forall|max: A, max_prime: A| self.has_maximum(r, max) && self.has_maximum(r, max_prime) ==> max == max_prime, { self.to_iset().lemma_maximal_is_unique(r); }
/// Set 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_set_insert_diff_decreases(self, s: Set<A>, elt: A) requires self.contains(elt), !s.contains(elt), 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: Set<A>, s2: Set<A>, elt: A) requires self.subset_of(s2), !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_set_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)), { broadcast use Set::lemma_map_contains;
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: Set<A>, f: spec_fn(A) -> B) ensures (self.union(t)).map(f) =~= self.map(f).union(t.map(f)), { broadcast use Set::lemma_map_contains;
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), { broadcast use Set::lemma_map_contains;
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>) -> Set<B> { self.map( |elem: A| match f(elem) { Option::Some(r) => set!{r}, Option::None => set!{}, }, ).flatten() }
/// Inserting commutes with `filter_map` pub broadcast proof fn lemma_filter_map_insert<B>( s: Set<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_set_lemmas; broadcast use Set::lemma_flatten_contains; broadcast use Set::lemma_map_contains; broadcast use Set::lemma_set_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) => set!{r}, Option::None => set!{}, }; 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) == set!{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: Set<A>) ensures #[trigger] self.union(t).filter_map(f) == self.filter_map(f).union(t.filter_map(f)), { broadcast use group_set_lemmas; broadcast use Set::lemma_flatten_contains; broadcast use Set::lemma_map_contains;
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) => set!{r}, Option::None => set!{}, };
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); }
/// 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_set_all_subset(self, s2: Set<A>, p: spec_fn(A) -> bool) requires #[trigger] self.subset_of(s2), s2.all(p), ensures #[trigger] self.all(p), { broadcast use group_set_lemmas;
}
/// Conversion to a sequence and back to a set is the identity function. pub broadcast proof fn lemma_to_seq_to_set_id(self) ensures #[trigger] self.to_seq().to_set() =~= self, decreases self.len(), { broadcast use lemma_set_empty_equivalency_len; broadcast use Seq::to_set_ensures; broadcast use super::seq_lib::group_seq_properties;
if self.len() == 0 { assert(self.to_seq().to_set() =~= Set::<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 set has no duplicates pub broadcast proof fn lemma_to_seq_no_duplicates(self) 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() == self.remove(x)) by { self.remove(x).lemma_to_seq_to_set_id(); } assert(!seq2.contains(x)) by { seq2.to_set_ensures() } } }
/// Conversion from set to seq preserves the length pub broadcast proof fn lemma_to_seq_len(self) 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> Set<Set<A>> { /// This function creates a set from all the elements of all the elements /// of `self`. pub closed spec fn flatten(self) -> Set<A> { Set::new( |elem| exists|elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem), ).unwrap() }
/// This helper lemma demonstrates that `Self::flatten` is finite, /// so it produces a valid `Set`. proof fn lemma_flatten_finite(self) ensures ISet::new( |elem| exists|elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem), ).finite(), decreases self.len(), { let flatten_f = |elem| exists|elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem); if forall|s: Set<A>| !self.contains(s) { assert(self =~= Set::<Set<A>>::empty()); assert(ISet::new(flatten_f) =~= ISet::<A>::empty()); } else { let s = choose|s: Set<A>| self.contains(s); self.remove(s).lemma_flatten_finite(); let flatten_remove_f = |elem| exists|elem_s: Set<A>| #[trigger] self.remove(s).contains(elem_s) && elem_s.contains(elem); assert(s.to_iset().finite()); assert(ISet::new(flatten_f) =~= ISet::new(flatten_remove_f).union(s.to_iset())); } }
/// Since `Self::flatten` is `closed`, this broadcast lemma is /// needed to make its semantics visible to the verifier. pub broadcast proof fn lemma_flatten_contains(self, elem: A) ensures #[trigger] self.flatten().contains(elem) <==> (exists|elem_s: Set<A>| #[trigger] self.contains(elem_s) && elem_s.contains(elem)), { self.lemma_flatten_finite(); }
/// 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: Set<A>) ensures self.flatten().union(other) =~= #[trigger] self.insert(other).flatten(), { broadcast use Set::lemma_flatten_contains; broadcast use Set::lemma_map_contains;
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 self.flatten().contains(elem) { self.lemma_flatten_contains(elem); let s = choose|s: Set<A>| #[trigger] self.contains(s) && s.contains(elem); assert(self.insert(other).contains(s)); assert(s.contains(elem)); } else { assert(other.contains(elem)); assert(self.insert(other).contains(other)); } self.insert(other).lemma_flatten_contains(elem); } }}
pub trait FiniteRange: Sized { spec fn in_range(i: Self, lo: Self, hi: Self) -> bool;
spec fn range_set(lo: Self, hi: Self) -> Set<Self>;
spec fn range_len(lo: Self, hi: Self) -> nat;
proof fn range_properties(lo: Self, hi: Self) ensures forall|i: Self| #[trigger] Self::range_set(lo, hi).contains(i) <==> Self::in_range(i, lo, hi), Self::range_set(lo, hi).len() == Self::range_len(lo, hi), ;}
/// This public broadcast lemma shows that when `A` has trait/// `FiniteRange`, `A::range_set(lo, hi)` has the expected properties./// That is, it contains all values `a: A` such that `lo <= a < hi`,/// and its length is `hi - lo`.pub broadcast proof fn range_set_properties<A: FiniteRange>(lo: A, hi: A) ensures forall|i: A| #[trigger] A::range_set(lo, hi).contains(i) <==> A::in_range(i, lo, hi), (#[trigger] A::range_set(lo, hi)).len() == A::range_len(lo, hi),{ A::range_properties(lo, hi);}
pub trait FiniteFull: Sized { proof fn full_properties() ensures Set::<Self>::full() is Some, ;}
/// This public broadcast lemma shows that when `A` has trait/// `FiniteRange`, `A::full()` has the expected propery of containing/// all values of type `A`.pub broadcast proof fn full_set_properties<A: FiniteFull>() ensures #![trigger Set::<A>::full()] Set::<A>::full() is Some,{ A::full_properties();}
impl<A: FiniteRange> Set<A> { #[verifier::inline] pub open spec fn range(lo: A, hi: A) -> Set<A> { A::range_set(lo, hi) }
#[verifier::inline] pub open spec fn range_inclusive(lo: A, hi: A) -> Set<A> { A::range_set(lo, hi).insert(hi) }}
impl<A: FiniteFull> Set<A> { #[verifier::inline] pub open spec fn from_finite_type(f: spec_fn(A) -> bool) -> Set<A> { Set::<A>::full().unwrap().filter(f) }}
// Macro to implement the trait for every numeric type. We need a macro here// because 'as nat' can't be written as a type generic.macro_rules! range_impls { ([$($t:ty)*]) => { $( verus! { impl FiniteRange for $t { open spec fn in_range(i: Self, lo: Self, hi: Self) -> bool { lo <= i < hi } open spec fn range_set(lo: Self, hi: Self) -> Set<Self> { Set::new(|i: Self| Self::in_range(i, lo, hi)).unwrap() } open spec fn range_len(lo: Self, hi: Self) -> nat { if lo <= hi { (hi - lo) as nat } else { 0 } } proof fn range_properties(lo: Self, hi: Self) decreases hi - lo { proof fn range_properties_helper(lo: $t, hi: $t) ensures ISet::<$t>::new(|i: $t| $t::in_range(i, lo, hi)).finite(), decreases hi - lo, { if lo >= hi { assert(ISet::<$t>::new(|i: $t| $t::in_range(i, lo, hi)) =~= ISet::<$t>::empty()); } else { let hi_minus_1: $t = (hi - 1) as $t; assert(hi_minus_1 == hi - 1); range_properties_helper(lo, hi_minus_1); assert(ISet::<$t>::new(|i: $t| $t::in_range(i, lo, hi)) =~= ISet::<$t>::new(|i: $t| $t::in_range(i, lo, hi_minus_1)).insert(hi_minus_1)); } }
range_properties_helper(lo, hi); if hi <= lo { assert(Self::range_set(lo, hi) =~= Set::<Self>::empty()); } else { let hi1 = (hi - 1) as $t; Self::range_properties(lo, hi1); assert(ISet::new(|i: Self| Self::in_range(i, lo, hi)) =~= ISet::new(|i: Self| Self::in_range(i, lo, hi1)).insert(hi1)); assert(Self::range_set(lo, hi) == Self::range_set(lo, hi1).insert(hi1)); } } } } // verus! )* }}
macro_rules! full_impls { ([$($t:ty)*]) => { $( verus! { impl FiniteFull for $t { proof fn full_properties() { proof fn full_properties_helper(lo: $t, hi: $t) requires lo <= hi, ensures ISet::<$t>::new(|a: $t| lo <= a && a <= hi).finite(), decreases hi - lo, { if lo == hi { assert(ISet::<$t>::new(|a: $t| lo <= a && a <= hi) =~= iset![lo]); } else { let hi_minus_1: $t = (hi - 1) as $t; assert(hi_minus_1 == hi - 1); full_properties_helper(lo, hi_minus_1); assert(ISet::<$t>::new(|a: $t| lo <= a && a <= hi) =~= ISet::<$t>::new(|a: $t| lo <= a && a <= hi_minus_1).insert(hi)); } }
full_properties_helper($t::MIN, $t::MAX); assert(ISet::<$t>::new(|a: $t| true) =~= ISet::<$t>::new(|a: $t| $t::MIN <= a && a <= $t::MAX)); assert(Set::<$t>::full() is Some); Self::range_properties($t::MIN, $t::MAX); assert(Set::<$t>::full().unwrap() == Set::range_inclusive($t::MIN, $t::MAX)); } } } // verus! )* }}
// Make Set::range available for all of the Verus numeric typesrange_impls!([ int nat usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
// Make Set::full available for all of the Verus numeric typesfull_impls!([ usize u8 u16 u32 u64 u128 isize i8 i16 i32 i64 i128]);
/// Two sets are equal iff mapping `f` results in equal sets, if `f` is injective.pub proof fn lemma_sets_eq_iff_injective_map_eq<T, S>(s1: Set<T>, s2: Set<T>, f: spec_fn(T) -> S) requires super::relations::injective(f), ensures (s1 == s2) <==> (s1.map(f) == s2.map(f)),{ broadcast use group_set_lemmas; broadcast use Set::lemma_map_contains;
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_sets_eq_iff_injective_map_on_eq<T, S>(s1: Set<T>, s2: Set<T>, f: spec_fn(T) -> S) requires (s1 + s2).injective_on(f), ensures (s1 == s2) <==> (s1.map(f) == s2.map(f)),{ broadcast use group_set_lemmas; broadcast use Set::lemma_map_contains;
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 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: Set<A>, s2: Set<A>) 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: Set<A>, s2: Set<A>) ensures s1.union(s2).len() >= s1.len(), s1.union(s2).len() >= s2.len(), decreases s2.len(),{ broadcast use group_set_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: Set<A>, s2: Set<A>) 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: Set<A>, s2: Set<A>) requires s1.subset_of(s2), ensures s1.len() <= s2.len(),{ lemma_len_intersect::<A>(s2, s1); assert(s2.intersect(s1) =~= s1);}
/// 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: Set<A>, s2: Set<A>) 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) -> Set<int> { Set::<int>::range(lo, 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 forall|j: int| set_int_range(lo, hi).contains(j) <==> lo <= j < hi, set_int_range(lo, hi).len() == hi - lo, decreases hi - lo,{ broadcast use range_set_properties;
}
/// 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: Set<A>, y: Set<A>) requires x.subset_of(y), x.len() == y.len(), ensures x =~= y, decreases x.len(),{ broadcast use group_set_properties;
if x =~= Set::<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: Set<A>, y: Set<B>, f: spec_fn(A) -> B) requires x.injective_on(f), x.map(f) == y, ensures x.len() == y.len(), decreases x.len(),{ broadcast use group_set_properties; broadcast use Set::lemma_map_contains;
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'spub proof fn lemma_map_size_bound<A, B>(x: Set<A>, y: Set<B>, f: spec_fn(A) -> B) requires x.map(f) == y, ensures y.len() <= x.len(), decreases x.len(),{ broadcast use group_set_properties; broadcast use Set::lemma_map_contains;
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_set_union_again1<A>(a: Set<A>, b: Set<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_set_union_again2<A>(a: Set<A>, b: Set<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_set_intersect_again1<A>(a: Set<A>, b: Set<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_set_intersect_again2<A>(a: Set<A>, b: Set<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_set_difference2<A>(s1: Set<A>, s2: Set<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_set_disjoint<A>(a: Set<A>, b: Set<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/// Set `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_set_empty_equivalency_len<A>(s: Set<A>) ensures #![trigger s.len()] (s.len() == 0 <==> s == Set::<A>::empty()) && (s.len() != 0 ==> exists|x: A| s.contains(x)),{ assert(s.len() == 0 ==> s =~= Set::empty()) by { if s.len() == 0 { assert(forall|a: A| !(Set::empty().contains(a))); assert(Set::<A>::empty().len() == 0); assert(Set::<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_set_remove_len(s, a); } } } } assert(s.len() == 0 <== s =~= Set::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_set_disjoint_lens<A>(a: Set<A>, b: Set<A>) ensures a.disjoint(b) ==> #[trigger] (a + b).len() == a.len() + b.len(), decreases a.len(),{ if a.len() == 0 { lemma_set_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_set_disjoint_lens(a.remove(x), b); } }}
/// Two sets are disjoint iff their intersection is emptypub proof fn lemma_set_disjoint_iff_empty_intersection<T>(a: Set<T>, b: Set<T>) ensures a.disjoint(b) <==> a.intersect(b).is_empty(),{ broadcast use group_set_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_set_intersect_union_lens<A>(a: Set<A>, b: Set<A>) ensures #[trigger] (a + b).len() + #[trigger] a.intersect(b).len() == a.len() + b.len(), decreases a.len(),{ if a.len() == 0 { lemma_set_empty_equivalency_len(a); assert(a + b =~= b); assert(a.intersect(b) =~= Set::empty()); assert(a.intersect(b).len() == 0); } else { let x = a.choose(); lemma_set_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_set_difference_len<A>(a: Set<A>, b: Set<A>) 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_set_empty_equivalency_len(a); assert(a.difference(b) =~= Set::empty()); assert(b.difference(a) =~= b); assert(a.intersect(b) =~= Set::empty()); assert(a + b =~= b); } else { let x = a.choose(); lemma_set_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_set_properties { lemma_set_union_again1, lemma_set_union_again2, lemma_set_intersect_again1, lemma_set_intersect_again2, lemma_set_difference2, lemma_set_disjoint, lemma_set_disjoint_lens, lemma_set_intersect_union_lens, lemma_set_difference_len, // REVIEW: exclude from broadcast group if trigger is too free // also note that some proofs in seq_lib requires this lemma lemma_set_empty_equivalency_len,}
pub broadcast proof fn lemma_set_is_empty<A>(s: Set<A>) requires !(#[trigger] s.is_empty()), ensures exists|a: A| s.contains(a),{ super::iset_lib::axiom_iset_is_empty(s.to_iset());}
pub broadcast proof fn lemma_set_is_empty_len0<A>(s: Set<A>) ensures #[trigger] s.is_empty() <==> s.len() == 0,{}
#[doc(hidden)]#[verifier::inline]pub open spec fn check_argument_is_set<A>(s: Set<A>) -> Set<A> { s}
/// Prove two sets equal by extensionality. Usage is:////// ```rust/// assert_sets_equal!(set1 == set2);/// ```////// or,////// ```rust/// assert_sets_equal!(set1 == set2, elem => {/// // prove that set1.contains(elem) iff set2.contains(elem)/// });/// ```#[macro_export]macro_rules! assert_sets_equal { [$($tail:tt)*] => { $crate::vstd::prelude::verus_proof_macro_exprs!($crate::vstd::set_lib::assert_sets_equal_internal!($($tail)*)) };}
#[macro_export]#[doc(hidden)]macro_rules! assert_sets_equal_internal { (::vstd::prelude::spec_eq($s1:expr, $s2:expr)) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2) }; (::vstd::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock) }; (crate::prelude::spec_eq($s1:expr, $s2:expr)) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2) }; (crate::prelude::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock) }; (crate::verus_builtin::spec_eq($s1:expr, $s2:expr)) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2) }; (crate::verus_builtin::spec_eq($s1:expr, $s2:expr), $elem:ident $( : $t:ty )? => $bblock:block) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, $elem $( : $t )? => $bblock) }; ($s1:expr, $s2:expr $(,)?) => { $crate::vstd::set_lib::assert_sets_equal_internal!($s1, $s2, elem => { }) }; ($s1:expr, $s2:expr, $elem:ident $( : $t:ty )? => $bblock:block) => { #[verifier::spec] let s1 = $crate::vstd::set_lib::check_argument_is_set($s1); #[verifier::spec] let s2 = $crate::vstd::set_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_set_lib_default { lemma_set_is_empty, lemma_set_is_empty_len0, Set::lemma_flatten_contains, Set::lemma_map_contains, Set::lemma_map_by_contains, Set::lemma_map_flatten_by_contains, range_set_properties, full_set_properties,}
pub use assert_sets_equal_internal;pub use assert_sets_equal;
} // verus!