mathlib docs: data.list.alist

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

Type (max u v)

entries : list (sigma β)
nodupkeys : c.entries.nodupkeys

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.

source

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

alist β

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

Equations

l.to_alist = {entries := l.erase_dupkeys, nodupkeys := _}

source

@[ext]

theorem alist.ext {α : Type u} {β : α → Type v} {s t : alist β} (a : s.entries = t.entries) :

s = t

source

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

s = t ↔ s.entries = t.entries

source

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

source

def alist.keys {α : Type u} {β : α → Type v} (s : alist β) :

list α

The list of keys of an association list.

Equations

s.keys = s.entries.keys

source

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

s.keys.nodup

source

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

alist.has_mem = {mem := λ (a : α) (s : alist β), a ∈ s.keys}

source

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

a ∈ s ↔ a ∈ s.keys

source

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

a ∈ s₁ ↔ a ∈ s₂

source

@[instance]

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

has_emptyc (alist β)

The empty association list.

Equations

alist.has_emptyc = {emptyc := {entries := list.nil (sigma β), nodupkeys := _}}

source

@[instance]

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

inhabited (alist β)

Equations

alist.inhabited = {default := ∅}

source

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

a ∉ ∅

source

@[simp]

theorem alist.empty_entries {α : Type u} {β : α → Type v} :

∅.entries = list.nil

source

@[simp]

theorem alist.keys_empty {α : Type u} {β : α → Type v} :

∅.keys = list.nil

source

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

alist β

The singleton association list.

Equations

alist.singleton a b = {entries := [⟨a, b⟩], nodupkeys := _}

source

@[simp]

theorem alist.singleton_entries {α : Type u} {β : α → Type v} (a : α) (b : β a) :

(alist.singleton a b).entries = [⟨a, b⟩]

source

@[simp]

theorem alist.keys_singleton {α : Type u} {β : α → Type v} (a : α) (b : β a) :

(alist.singleton a b).keys = [a]

source

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

option (β a)

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

Equations

alist.lookup a s = list.lookup a s.entries

source

@[simp]

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

alist.lookup a ∅ = none

source

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

↥((alist.lookup a s).is_some) ↔ a ∈ s

source

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

alist.lookup a s = none ↔ a ∉ s

source

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

alist.lookup a s₁ = alist.lookup a s₂

source

@[instance]

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

decidable (a ∈ s)

Equations

alist.decidable a s = decidable_of_iff ↥((alist.lookup a s).is_some) _

source

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

alist β

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

source

@[simp]

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

(alist.replace a b s).keys = s.keys

source

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

source

theorem alist.perm_replace {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ : alist β} (a_1 : s₁.entries ~ s₂.entries) :

(alist.replace a b s₁).entries ~ (alist.replace a b s₂).entries

source

def alist.foldl {α : Type u} {β : α → Type v} {δ : Type w} (f : δ → Π (a : α), β a → δ) (d : δ) (m : 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

source

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

alist β

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

source

@[simp]

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

(alist.erase a s).keys = s.keys.erase a

source

@[simp]

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

a' ∈ alist.erase a s ↔ a' ≠ a ∧ a' ∈ s

source

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

(alist.erase a s₁).entries ~ (alist.erase a s₂).entries

source

@[simp]

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

alist.lookup a (alist.erase a s) = none

source

@[simp]

theorem alist.lookup_erase_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {s : alist β} (h : a ≠ a') :

alist.lookup a (alist.erase a' s) = alist.lookup a s

source

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)

source

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

alist β

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

source

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

source

theorem alist.insert_entries_of_neg {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s : alist β} (h : a ∉ s) :

(alist.insert a b s).entries = ⟨a, b⟩ :: s.entries

source

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

source

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

source

theorem alist.perm_insert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ : alist β} (p : s₁.entries ~ s₂.entries) :

(alist.insert a b s₁).entries ~ (alist.insert a b s₂).entries

source

@[simp]

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

alist.lookup a (alist.insert a b s) = some b

source

@[simp]

theorem alist.lookup_insert_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b' : β a'} {s : alist β} (h : a ≠ a') :

alist.lookup a (alist.insert a' b' s) = alist.lookup a s

source

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

source

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

source

theorem alist.insert_insert_of_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b : β a} {b' : β a'} (s : alist β) (h : a ≠ a') :

(alist.insert a' b' (alist.insert a b s)).entries ~ (alist.insert a b (alist.insert a' b' s)).entries

source

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

source

@[simp]

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

xs.to_alist.entries = xs.erase_dupkeys

source

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

source

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

option (β a) × alist β

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

source

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

source

def alist.union {α : Type u} {β : α → Type v} [decidable_eq α] (s₁ s₂ : 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

s₁.union s₂ = {entries := s₁.entries.kunion s₂.entries, nodupkeys := _}

source

@[instance]

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

has_union (alist β)

Equations

alist.has_union = {union := alist.union (λ (a b : α), _inst_1 a b)}

source

@[simp]

theorem alist.union_entries {α : Type u} {β : α → Type v} [decidable_eq α] {s₁ s₂ : alist β} :

(s₁ ∪ s₂).entries = s₁.entries.kunion s₂.entries

source

@[simp]

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

∅ ∪ s = s

source

@[simp]

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

s ∪ ∅ = s

source

@[simp]

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

a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

source

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

(s₁ ∪ s₃).entries ~ (s₂ ∪ s₄).entries

source

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₂

source

@[simp]

theorem alist.lookup_union_left {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s₁ s₂ : alist β} (a_1 : a ∈ s₁) :

alist.lookup a (s₁ ∪ s₂) = alist.lookup a s₁

source

@[simp]

theorem alist.lookup_union_right {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s₁ s₂ : alist β} (a_1 : a ∉ s₁) :

alist.lookup a (s₁ ∪ s₂) = alist.lookup a s₂

source

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

source

theorem alist.mem_lookup_union_middle {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s₁ s₂ s₃ : alist β} (a_1 : b ∈ alist.lookup a (s₁ ∪ s₃)) (a_2 : a ∉ s₂) :

b ∈ alist.lookup a (s₁ ∪ s₂ ∪ s₃)

source

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₂

source

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

(s₁ ∪ s₂ ∪ s₃).entries ~ (s₁ ∪ (s₂ ∪ s₃)).entries

source

def alist.disjoint {α : Type u} {β : α → Type v} (s₁ s₂ : alist β) :

Prop

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

Equations

s₁.disjoint s₂ = ∀ (k : α), k ∈ s₁.keys → k ∉ s₂.keys

source

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

(s₁ ∪ s₂).entries ~ (s₂ ∪ s₁).entries

mathlib documentation

Association lists

keys

mem

empty

singleton

lookup

replace

erase

insert

extract

union

disjoint