mathlib3 documentation

data.list.alist

Association Lists #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines association lists. An association list is a list where every element consists of a key and a value, and no two entries have the same key. The type of the value is allowed to be dependent on the type of the key.

This type dependence is implemented using sigma: The elements of the list are of type sigma β, for some type index β.

Main definitions #

Association lists are represented by the alist structure. This file defines this structure and provides ways to access, modify, and combine alists.

alist.keys returns a list of keys of the alist.
alist.has_mem returns membership in the set of keys.
alist.erase removes a certain key.
alist.insert adds a key-value mapping to the list.
alist.union combines two association lists.

References #

https://en.wikipedia.org/wiki/Association_list

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

Type (max u v)

entries : list (sigma β)
nodupkeys : self.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.

Instances for alist

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

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

Equations

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

@[ext]

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

s.entries = t.entries → s = t

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

s = t ↔ s.entries = t.entries

@[protected, 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 #

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

The list of keys of an association list.

Equations

s.keys = s.entries.keys

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

mem #

@[protected, 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}

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 β} (p : s₁.entries ~ s₂.entries) :

a ∈ s₁ ↔ a ∈ s₂

empty #

@[protected, 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 := _}}

@[protected, instance]

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

inhabited (alist β)

Equations

alist.inhabited = {default := ∅}

@[simp]

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

@[simp]

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

∅.entries = list.nil

@[simp]

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

∅.keys = list.nil

singleton #

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

The singleton association list.

Equations

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

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

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

@[simp]

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

alist.lookup a ∅ = option.none

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.mem_lookup_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {s : alist β} :

b ∈ alist.lookup a s ↔ ⟨a, b⟩ ∈ s.entries

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₂

@[protected, instance]

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

decidable (a ∈ s)

Equations

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

replace #

def alist.replace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : 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 := _}

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

erase #

def alist.erase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (s : 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 := _}

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

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 β} (h : 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 #

def alist.insert {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (s : 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 := _}

@[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 β} (h : a ∉ s) :

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

theorem alist.insert_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, nodupkeys := _}

@[simp]

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

alist.insert a b ∅ = alist.singleton a b

@[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 β} (p : 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 β} (h : 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 β) (h : 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.dedupkeys

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

theorem alist.mk_cons_eq_insert {α : Type u} {β : α → Type v} [decidable_eq α] (c : sigma β) (l : list (sigma β)) (h : (c :: l).nodupkeys) :

{entries := c :: l, nodupkeys := h} = alist.insert c.fst c.snd {entries := l, nodupkeys := _}

def alist.insert_rec {α : Type u} {β : α → Type v} [decidable_eq α] {C : alist β → Sort u_1} (H0 : C ∅) (IH : Π (a : α) (b : β a) (l : alist β), a ∉ l → C l → C (alist.insert a b l)) (l : alist β) :

C l

Recursion on an alist, using insert. Use as induction l using alist.insert_rec.

Equations

alist.insert_rec H0 IH {entries := c :: l, nodupkeys := h} = _.mpr (IH c.fst c.snd {entries := l, nodupkeys := _} _ (alist.insert_rec H0 IH {entries := l, nodupkeys := _}))
alist.insert_rec H0 IH {entries := list.nil (sigma β), nodupkeys := _x} = H0

@[simp]

theorem alist.insert_rec_empty {α : Type u} {β : α → Type v} [decidable_eq α] {C : alist β → Sort u_1} (H0 : C ∅) (IH : Π (a : α) (b : β a) (l : alist β), a ∉ l → C l → C (alist.insert a b l)) :

alist.insert_rec H0 IH ∅ = H0

theorem alist.insert_rec_insert {α : Type u} {β : α → Type v} [decidable_eq α] {C : alist β → Sort u_1} (H0 : C ∅) (IH : Π (a : α) (b : β a) (l : alist β), a ∉ l → C l → C (alist.insert a b l)) {c : sigma β} {l : alist β} (h : c.fst ∉ l) :

alist.insert_rec H0 IH (alist.insert c.fst c.snd l) = IH c.fst c.snd l h (alist.insert_rec H0 IH l)

theorem alist.recursion_insert_mk {α : Type u} {β : α → Type v} [decidable_eq α] {C : alist β → Sort u_1} (H0 : C ∅) (IH : Π (a : α) (b : β a) (l : alist β), a ∉ l → C l → C (alist.insert a b l)) {a : α} (b : β a) {l : alist β} (h : a ∉ l) :

alist.insert_rec H0 IH (alist.insert a b l) = IH a b l h (alist.insert_rec H0 IH l)

extract #

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

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

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

@[protected, 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)}

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

@[simp]

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

@[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 β} (p₁₂ : s₁.entries ~ s₂.entries) (p₃₄ : s₃.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} (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

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