Finite maps over multiset
multisets of sigma types
Multiset of keys of an association multiset.
Equations
- s.keys = multiset.map sigma.fst s
nodupkeys s means that s has no duplicate keys.
Equations
- s.nodupkeys = quot.lift_on s list.nodupkeys multiset.nodupkeys._proof_1
finmap
lifting from alist
induction
extensionality
mem
keys
empty
@[instance]
The empty map.
@[instance]
Equations
- finmap.inhabited = {default := ∅}
@[simp]
singleton
The singleton map.
Equations
- finmap.singleton a b = (alist.singleton a b).to_finmap
@[simp]
theorem
finmap.keys_singleton
{α : Type u}
{β : α → Type v}
(a : α)
(b : β a) :
(finmap.singleton a b).keys = {a}
@[simp]
theorem
finmap.mem_singleton
{α : Type u}
{β : α → Type v}
(x y : α)
(b : β y) :
x ∈ finmap.singleton y b ↔ x = y
@[instance]
def
finmap.has_decidable_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
[Π (a : α), decidable_eq (β a)] :
decidable_eq (finmap β)
Equations
- finmap.has_decidable_eq s₁ s₂ = decidable_of_iff (s₁.entries = s₂.entries) finmap.ext_iff
lookup
Look up the value associated to a key in a map.
Equations
- finmap.lookup a s = s.lift_on (alist.lookup a) _
@[simp]
theorem
finmap.lookup_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
finmap.lookup a s.to_finmap = alist.lookup a s
@[simp]
theorem
finmap.lookup_list_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : list (sigma β)) :
finmap.lookup a s.to_finmap = list.lookup a s
@[simp]
theorem
finmap.lookup_is_some
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : finmap β} :
↥((finmap.lookup a s).is_some) ↔ a ∈ s
theorem
finmap.lookup_eq_none
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : finmap β} :
finmap.lookup a s = option.none ↔ a ∉ s
@[simp]
theorem
finmap.lookup_singleton_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a} :
finmap.lookup a (finmap.singleton a b) = option.some b
@[instance]
Equations
- finmap.decidable a s = decidable_of_iff ↥((finmap.lookup a s).is_some) _
theorem
finmap.mem_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : finmap β} :
a ∈ s ↔ ∃ (b : β a), finmap.lookup a s = option.some b
theorem
finmap.mem_of_lookup_eq_some
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s : finmap β} :
finmap.lookup a s = option.some b → a ∈ s
theorem
finmap.ext_lookup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{s₁ s₂ : finmap β} :
(∀ (x : α), finmap.lookup x s₁ = finmap.lookup x s₂) → s₁ = s₂
replace
Replace a key with a given value in a finite map. If the key is not present it does nothing.
Equations
- finmap.replace a b s = s.lift_on (λ (t : alist β), (alist.replace a b t).to_finmap) _
@[simp]
theorem
finmap.replace_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(s : alist β) :
finmap.replace a b s.to_finmap = (alist.replace a b s).to_finmap
@[simp]
theorem
finmap.keys_replace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(s : finmap β) :
(finmap.replace a b s).keys = s.keys
@[simp]
theorem
finmap.mem_replace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b : β a}
{s : finmap β} :
a' ∈ finmap.replace a b s ↔ a' ∈ s
foldl
Fold a commutative function over the key-value pairs in the map
Equations
- finmap.foldl f H d m = multiset.foldl (λ (d : δ) (s : sigma β), f d s.fst s.snd) _ d m.entries
any f s returns tt iff there exists a value v in s such that f v = tt.
Equations
- finmap.any f s = finmap.foldl (λ (x : bool) (y : α) (z : β y), decidable.to_bool (↥x ∨ ↥(f y z))) _ bool.ff s
all f s returns tt iff f v = tt for all values v in s.
Equations
- finmap.all f s = finmap.foldl (λ (x : bool) (y : α) (z : β y), decidable.to_bool (↥x ∧ ↥(f y z))) _ bool.ff s
erase
Erase a key from the map. If the key is not present it does nothing.
Equations
- finmap.erase a s = s.lift_on (λ (t : alist β), (alist.erase a t).to_finmap) _
@[simp]
theorem
finmap.erase_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
finmap.erase a s.to_finmap = (alist.erase a s).to_finmap
@[simp]
theorem
finmap.keys_erase_to_finset
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
@[simp]
theorem
finmap.keys_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : finmap β) :
(finmap.erase a s).keys = s.keys.erase a
@[simp]
theorem
finmap.mem_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{s : finmap β} :
theorem
finmap.not_mem_erase_self
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : finmap β} :
a ∉ finmap.erase a s
@[simp]
theorem
finmap.lookup_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : finmap β) :
finmap.lookup a (finmap.erase a s) = option.none
@[simp]
theorem
finmap.lookup_erase_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{s : finmap β} :
a ≠ a' → finmap.lookup a (finmap.erase a' s) = finmap.lookup a s
theorem
finmap.erase_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{s : finmap β} :
finmap.erase a (finmap.erase a' s) = finmap.erase a' (finmap.erase a s)
sdiff
sdiff s s' consists of all key-value pairs from s and s' where the keys are in s or
s' but not both.
Equations
- s.sdiff s' = finmap.foldl (λ (s : finmap β) (x : α) (_x : β x), finmap.erase x s) finmap.sdiff._proof_1 s s'
@[instance]
Equations
- finmap.has_sdiff = {sdiff := finmap.sdiff (λ (a b : α), _inst_1 a b)}
insert
Insert a key-value pair into a finite map, replacing any existing pair with the same key.
Equations
- finmap.insert a b s = s.lift_on (λ (t : alist β), (alist.insert a b t).to_finmap) _
@[simp]
theorem
finmap.insert_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(s : alist β) :
finmap.insert a b s.to_finmap = (alist.insert a b s).to_finmap
theorem
finmap.insert_entries_of_neg
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s : finmap β} :
@[simp]
theorem
finmap.mem_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b' : β a'}
{s : finmap β} :
@[simp]
theorem
finmap.lookup_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
(s : finmap β) :
finmap.lookup a (finmap.insert a b s) = option.some b
@[simp]
theorem
finmap.lookup_insert_of_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b : β a}
(s : finmap β) :
a' ≠ a → finmap.lookup a' (finmap.insert a b s) = finmap.lookup a' s
@[simp]
theorem
finmap.insert_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b b' : β a}
(s : finmap β) :
finmap.insert a b' (finmap.insert a b s) = finmap.insert a b' s
theorem
finmap.insert_insert_of_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b : β a}
{b' : β a'}
(s : finmap β) :
a ≠ a' → finmap.insert a' b' (finmap.insert a b s) = finmap.insert a b (finmap.insert a' b' s)
theorem
finmap.to_finmap_cons
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(xs : list (sigma β)) :
theorem
finmap.mem_list_to_finmap
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(xs : list (sigma β)) :
@[simp]
theorem
finmap.insert_singleton_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b b' : β a} :
finmap.insert a b (finmap.singleton a b') = finmap.singleton a b
extract
Erase a key from the map, and return the corresponding value, if found.
Equations
- finmap.extract a s = s.lift_on (λ (t : alist β), prod.map id alist.to_finmap (alist.extract a t)) _
@[simp]
theorem
finmap.extract_eq_lookup_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : finmap β) :
finmap.extract a s = (finmap.lookup a s, finmap.erase a s)
union
s₁ ∪ s₂ is the key-based union of two finite maps. It is left-biased: if
there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.
@[instance]
Equations
- finmap.has_union = {union := finmap.union (λ (a b : α), _inst_1 a b)}
@[simp]
theorem
finmap.mem_union
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : finmap β} :
@[simp]
@[simp]
theorem
finmap.lookup_union_left
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : finmap β} :
a ∈ s₁ → finmap.lookup a (s₁ ∪ s₂) = finmap.lookup a s₁
@[simp]
theorem
finmap.lookup_union_right
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : finmap β} :
a ∉ s₁ → finmap.lookup a (s₁ ∪ s₂) = finmap.lookup a s₂
theorem
finmap.lookup_union_left_of_not_in
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : finmap β} :
a ∉ s₂ → finmap.lookup a (s₁ ∪ s₂) = finmap.lookup a s₁
@[simp]
theorem
finmap.mem_lookup_union
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : finmap β} :
b ∈ finmap.lookup a (s₁ ∪ s₂) ↔ b ∈ finmap.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ finmap.lookup a s₂
theorem
finmap.mem_lookup_union_middle
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ s₃ : finmap β} :
b ∈ finmap.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ finmap.lookup a (s₁ ∪ s₂ ∪ s₃)
theorem
finmap.insert_union
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : finmap β} :
finmap.insert a b (s₁ ∪ s₂) = finmap.insert a b s₁ ∪ s₂
@[simp]
@[simp]
theorem
finmap.erase_union_singleton
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(s : finmap β) :
finmap.lookup a s = option.some b → finmap.erase a s ∪ finmap.singleton a b = s
disjoint
@[instance]
Equations
- finmap.decidable_rel = λ (x y : finmap β), id multiset.decidable_dforall_multiset
theorem
finmap.disjoint_union_left
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(x y z : finmap β) :
theorem
finmap.disjoint_union_right
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(x y z : finmap β) :
theorem
finmap.union_comm_of_disjoint
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{s₁ s₂ : finmap β} :