Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456145714581459146014611462146314641465146614671468146914701471147214731474147514761477147814791480148114821483148414851486148714881489149014911492149314941495149614971498149915001501150215031504150515061507150815091510151115121513151415151516151715181519152015211522152315241525152615271528152915301531153215331534153515361537153815391540154115421543154415451546154715481549155015511552155315541555155615571558155915601561156215631564156515661567156815691570157115721573157415751576157715781579158015811582158315841585#[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'spub 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 emptypub 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!