Association lists
@[instance]
def
alist.decidable_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
[Π (a : α), decidable_eq (β a)] :
decidable_eq (alist β)
Equations
- alist.decidable_eq = λ (xs ys : alist β), _.mpr (list.decidable_eq xs.entries ys.entries)
keys
mem
empty
@[instance]
The empty association list.
@[instance]
Equations
- alist.inhabited = {default := ∅}
singleton
The singleton association list.
@[simp]
theorem
alist.singleton_entries
{α : Type u}
{β : α → Type v}
(a : α)
(b : β a) :
(alist.singleton a b).entries = [⟨a, b⟩]
@[simp]
theorem
alist.keys_singleton
{α : Type u}
{β : α → Type v}
(a : α)
(b : β a) :
(alist.singleton a b).keys = [a]
lookup
Look up the value associated to a key in an association list.
Equations
- alist.lookup a s = list.lookup a s.entries
@[simp]
theorem
alist.lookup_is_some
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : alist β} :
↥((alist.lookup a s).is_some) ↔ a ∈ s
theorem
alist.lookup_eq_none
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : alist β} :
alist.lookup a s = option.none ↔ a ∉ s
theorem
alist.perm_lookup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : alist β} :
s₁.entries ~ s₂.entries → alist.lookup a s₁ = alist.lookup a s₂
@[instance]
Equations
- alist.decidable a s = decidable_of_iff ↥((alist.lookup a s).is_some) _
replace
Replace a key with a given value in an association list. If the key is not present it does nothing.
Equations
- alist.replace a b s = {entries := list.kreplace a b s.entries, nodupkeys := _}
@[simp]
theorem
alist.keys_replace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(s : alist β) :
(alist.replace a b s).keys = s.keys
@[simp]
theorem
alist.mem_replace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b : β a}
{s : alist β} :
a' ∈ alist.replace a b s ↔ a' ∈ s
theorem
alist.perm_replace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : alist β} :
s₁.entries ~ s₂.entries → (alist.replace a b s₁).entries ~ (alist.replace a b s₂).entries
def
alist.foldl
{α : Type u}
{β : α → Type v}
{δ : Type w} :
(δ → Π (a : α), β a → δ) → δ → alist β → δ
Fold a function over the key-value pairs in the map.
Equations
- alist.foldl f d m = list.foldl (λ (r : δ) (a : sigma β), f r a.fst a.snd) d m.entries
erase
Erase a key from the map. If the key is not present, do nothing.
Equations
- alist.erase a s = {entries := list.kerase a s.entries, nodupkeys := _}
@[simp]
theorem
alist.keys_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
(alist.erase a s).keys = s.keys.erase a
@[simp]
theorem
alist.perm_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : alist β} :
s₁.entries ~ s₂.entries → (alist.erase a s₁).entries ~ (alist.erase a s₂).entries
@[simp]
theorem
alist.lookup_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
alist.lookup a (alist.erase a s) = option.none
@[simp]
theorem
alist.lookup_erase_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{s : alist β} :
a ≠ a' → alist.lookup a (alist.erase a' s) = alist.lookup a s
theorem
alist.erase_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a a' : α)
(s : alist β) :
alist.erase a' (alist.erase a s) = alist.erase a (alist.erase a' s)
insert
Insert a key-value pair into an association list and erase any existing pair with the same key.
Equations
- alist.insert a b s = {entries := list.kinsert a b s.entries, nodupkeys := _}
@[simp]
theorem
alist.insert_entries
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s : alist β} :
(alist.insert a b s).entries = ⟨a, b⟩ :: list.kerase a s.entries
theorem
alist.insert_entries_of_neg
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s : alist β} :
@[simp]
theorem
alist.mem_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b' : β a'}
(s : alist β) :
@[simp]
theorem
alist.keys_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
(s : alist β) :
theorem
alist.perm_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : alist β} :
s₁.entries ~ s₂.entries → (alist.insert a b s₁).entries ~ (alist.insert a b s₂).entries
@[simp]
theorem
alist.lookup_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
(s : alist β) :
alist.lookup a (alist.insert a b s) = option.some b
@[simp]
theorem
alist.lookup_insert_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b' : β a'}
{s : alist β} :
a ≠ a' → alist.lookup a (alist.insert a' b' s) = alist.lookup a s
@[simp]
theorem
alist.lookup_to_alist
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
(s : list (sigma β)) :
alist.lookup a s.to_alist = list.lookup a s
@[simp]
theorem
alist.insert_insert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b b' : β a}
(s : alist β) :
alist.insert a b' (alist.insert a b s) = alist.insert a b' s
theorem
alist.insert_insert_of_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b : β a}
{b' : β a'}
(s : alist β) :
a ≠ a' → (alist.insert a' b' (alist.insert a b s)).entries ~ (alist.insert a b (alist.insert a' b' s)).entries
@[simp]
theorem
alist.insert_singleton_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b b' : β a} :
alist.insert a b (alist.singleton a b') = alist.singleton a b
@[simp]
theorem
alist.entries_to_alist
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(xs : list (sigma β)) :
xs.to_alist.entries = xs.erase_dupkeys
theorem
alist.to_alist_cons
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(xs : list (sigma β)) :
extract
Erase a key from the map, and return the corresponding value, if found.
Equations
- alist.extract a s = have this : (list.kextract a s.entries).snd.nodupkeys, from _, alist.extract._match_1 a (list.kextract a s.entries) this
- alist.extract._match_1 a (b, l) h = (b, {entries := l, nodupkeys := h})
@[simp]
theorem
alist.extract_eq_lookup_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s : alist β) :
alist.extract a s = (alist.lookup a s, alist.erase a s)
union
s₁ ∪ s₂ is the key-based union of two association lists. It is
left-biased: if there exists an a ∈ s₁, lookup a (s₁ ∪ s₂) = lookup a s₁.
@[instance]
Equations
- alist.has_union = {union := alist.union (λ (a b : α), _inst_1 a b)}
@[simp]
@[simp]
@[simp]
@[simp]
theorem
alist.union_erase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(s₁ s₂ : alist β) :
alist.erase a (s₁ ∪ s₂) = alist.erase a s₁ ∪ alist.erase a s₂
@[simp]
theorem
alist.lookup_union_left
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : alist β} :
a ∈ s₁ → alist.lookup a (s₁ ∪ s₂) = alist.lookup a s₁
@[simp]
theorem
alist.lookup_union_right
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s₁ s₂ : alist β} :
a ∉ s₁ → alist.lookup a (s₁ ∪ s₂) = alist.lookup a s₂
@[simp]
theorem
alist.mem_lookup_union
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : alist β} :
b ∈ alist.lookup a (s₁ ∪ s₂) ↔ b ∈ alist.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ alist.lookup a s₂
theorem
alist.mem_lookup_union_middle
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ s₃ : alist β} :
b ∈ alist.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ alist.lookup a (s₁ ∪ s₂ ∪ s₃)
theorem
alist.insert_union
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{s₁ s₂ : alist β} :
alist.insert a b (s₁ ∪ s₂) = alist.insert a b s₁ ∪ s₂
disjoint
theorem
alist.union_comm_of_disjoint
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{s₁ s₂ : alist β} :