mathlib documentation

data.list.alist

Association lists

structure alist {α : Type u} :
(α → Type v)Type (max u v)

alist β is a key-value map stored as a list (i.e. a linked list). It is a wrapper around certain list functions with the added constraint that the list have unique keys.

def list.to_alist {α : Type u} [decidable_eq α] {β : α → Type v} :
list (sigma β)alist β

Given l : list (sigma β), create a term of type alist β by removing entries with duplicate keys.

Equations
@[ext]
theorem alist.ext {α : Type u} {β : α → Type v} {s t : alist β} :
s.entries = t.entriess = t

theorem alist.ext_iff {α : Type u} {β : α → Type v} {s t : alist β} :

@[instance]
def alist.decidable_eq {α : Type u} {β : α → Type v} [decidable_eq α] [Π (a : α), decidable_eq (β a)] :

Equations

keys

def alist.keys {α : Type u} {β : α → Type v} :
alist βlist α

The list of keys of an association list.

Equations
theorem alist.keys_nodup {α : Type u} {β : α → Type v} (s : alist β) :

mem

@[instance]
def alist.has_mem {α : Type u} {β : α → Type v} :
has_mem α (alist β)

The predicate a ∈ s means that s has a value associated to the key a.

Equations
theorem alist.mem_keys {α : Type u} {β : α → Type v} {a : α} {s : alist β} :
a s a s.keys

theorem alist.mem_of_perm {α : Type u} {β : α → Type v} {a : α} {s₁ s₂ : alist β} :
s₁.entries ~ s₂.entries(a s₁ a s₂)

empty

@[instance]
def alist.has_emptyc {α : Type u} {β : α → Type v} :

The empty association list.

Equations
@[instance]
def alist.inhabited {α : Type u} {β : α → Type v} :

Equations
theorem alist.not_mem_empty {α : Type u} {β : α → Type v} (a : α) :

@[simp]
theorem alist.empty_entries {α : Type u} {β : α → Type v} :

@[simp]
theorem alist.keys_empty {α : Type u} {β : α → Type v} :

singleton

def alist.singleton {α : Type u} {β : α → Type v} (a : α) :
β aalist β

The singleton association list.

Equations
@[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) :

lookup

def alist.lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
alist βoption (β a)

Look up the value associated to a key in an association list.

Equations
@[simp]
theorem alist.lookup_empty {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :

theorem alist.lookup_is_some {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : alist β} :

theorem alist.lookup_eq_none {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : alist β} :

theorem alist.perm_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s₁ s₂ : alist β} :
s₁.entries ~ s₂.entriesalist.lookup a s₁ = alist.lookup a s₂

@[instance]
def alist.decidable {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

Equations

replace

def alist.replace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
β aalist βalist β

Replace a key with a given value in an association list. If the key is not present it does nothing.

Equations
@[simp]
theorem alist.keys_replace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : alist β) :

@[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

erase

def alist.erase {α : Type u} {β : α → Type v} [decidable_eq α] :
α → alist βalist β

Erase a key from the map. If the key is not present, do nothing.

Equations
@[simp]
theorem alist.keys_erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

@[simp]
theorem alist.mem_erase {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {s : alist β} :
a' alist.erase a s a' a a' s

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 β) :

@[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 β) :

insert

def alist.insert {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
β aalist βalist β

Insert a key-value pair into an association list and erase any existing pair with the same key.

Equations
@[simp]
theorem alist.insert_entries {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s : alist β} :

theorem alist.insert_entries_of_neg {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s : alist β} :
a s(alist.insert a b s).entries = a, b⟩ :: s.entries

@[simp]
theorem alist.mem_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b' : β a'} (s : alist β) :
a alist.insert a' b' s a = a' a s

@[simp]
theorem alist.keys_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} (s : alist β) :
(alist.insert a b s).keys = a :: s.keys.erase a

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 β) :

@[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 β)) :

@[simp]
theorem alist.insert_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b b' : β a} (s : alist β) :

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} :

@[simp]
theorem alist.entries_to_alist {α : Type u} {β : α → Type v} [decidable_eq α] (xs : list (sigma β)) :

theorem alist.to_alist_cons {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (xs : list (sigma β)) :
(a, b⟩ :: xs).to_alist = alist.insert a b xs.to_alist

extract

def alist.extract {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
alist βoption (β a) × alist β

Erase a key from the map, and return the corresponding value, if found.

Equations
@[simp]
theorem alist.extract_eq_lookup_erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : alist β) :

union

def alist.union {α : Type u} {β : α → Type v} [decidable_eq α] :
alist βalist βalist β

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₁.

Equations
@[instance]
def alist.has_union {α : Type u} {β : α → Type v} [decidable_eq α] :

Equations
@[simp]
theorem alist.union_entries {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ : alist β} :
(s₁ s₂).entries = s₁.entries.kunion s₂.entries

@[simp]
theorem alist.empty_union {α : Type u} {β : α → Type v} [decidable_eq α] {s : alist β} :
s = s

@[simp]
theorem alist.union_empty {α : Type u} {β : α → Type v} [decidable_eq α] {s : alist β} :
s = s

@[simp]
theorem alist.mem_union {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s₁ s₂ : alist β} :
a s₁ s₂ a s₁ a s₂

theorem alist.perm_union {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ s₃ s₄ : alist β} :
s₁.entries ~ s₂.entriess₃.entries ~ s₄.entries(s₁ s₃).entries ~ (s₂ s₄).entries

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₂

theorem alist.union_assoc {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ s₃ : alist β} :
(s₁ s₂ s₃).entries ~ (s₁ (s₂ s₃)).entries

disjoint

def alist.disjoint {α : Type u} {β : α → Type v} :
alist βalist β → Prop

Two associative lists are disjoint if they have no common keys.

Equations
theorem alist.union_comm_of_disjoint {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ : alist β} :
s₁.disjoint s₂(s₁ s₂).entries ~ (s₂ s₁).entries