Function vstd::map_lib::lemma_map_properties

source ·

pub proof fn lemma_map_properties<K, V>()

Expand description

ensures

forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| {
    #[trigger] Map::<K, V>::new(fk, fv).dom() == Set::<K>::new(|k: K| fk(k))
},

forall |fk: FnSpec(K) -> bool, fv: FnSpec(K) -> V| {
    #[trigger] Map::<K, V>::new(fk, fv).values()
        == Set::<V>::new(|v: V| exists |k: K| #[trigger] fk(k) && #[trigger] fv(k) == v)
},

Properties of maps from the Dafny prelude (which were axioms in Dafny, but proven here in Verus)