Association Lists

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

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.

• entries : List (Sigma β)

  The underlying List of an AList

• nodupKeys : List.NodupKeys self.entries

  There are no duplicate keys in entries

def List.toAList {α : Type u} [DecidableEq α] {β : α → Type v} (l : List (Sigma β)) : AList β

Given l : List (Sigma β), create a term of type AList β by removing entries with duplicate keys.

Equations

• List.toAList l = { entries := List.dedupKeys l, nodupKeys := ⋯ }

theorem AList.ext {α : Type u} {β : α → Type v} {s : AList β} {t : AList β} : s.entries = t.entries → s = t

theorem AList.ext_iff {α : Type u} {β : α → Type v} {s : AList β} {t : AList β} : s = t ↔ s.entries = t.entries

instance AList.instDecidableEqAList {α : Type u} {β : α → Type v} [DecidableEq α] [(a : α) → DecidableEq (β a)] : DecidableEq (AList β)

Equations

• AList.instDecidableEqAList xs ys = Eq.mpr ⋯ inferInstance

keys

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

The list of keys of an association list.

Equations

• AList.keys s = List.keys s.entries

theorem AList.keys_nodup {α : Type u} {β : α → Type v} (s : AList β) : List.Nodup (AList.keys s)

mem

instance AList.instMembershipAList {α : Type u} {β : α → Type v} : Membership α (AList β)

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

Equations

• AList.instMembershipAList = { mem := fun (a : α) (s : AList β) => a ∈ AList.keys s }

theorem AList.mem_keys {α : Type u} {β : α → Type v} {a : α} {s : AList β} : a ∈ s ↔ a ∈ AList.keys s

theorem AList.mem_of_perm {α : Type u} {β : α → Type v} {a : α} {s₁ : AList β} {s₂ : AList β} (p : List.Perm s₁.entries s₂.entries) : a ∈ s₁ ↔ a ∈ s₂

empty

instance AList.instEmptyCollectionAList {α : Type u} {β : α → Type v} : EmptyCollection (AList β)

The empty association list.

Equations

• AList.instEmptyCollectionAList = { emptyCollection := { entries := [], nodupKeys := ⋯ } }

instance AList.instInhabitedAList {α : Type u} {β : α → Type v} : Inhabited (AList β)

Equations

• AList.instInhabitedAList = { default := ∅ }

@[simp]

theorem AList.not_mem_empty {α : Type u} {β : α → Type v} (a : α) : a ∉ ∅

@[simp]

theorem AList.empty_entries {α : Type u} {β : α → Type v} : ∅.entries = []

@[simp]

theorem AList.keys_empty {α : Type u} {β : α → Type v} : AList.keys ∅ = []

singleton

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

The singleton association list.

Equations

• AList.singleton a b = { entries := [{ fst := a, snd := b }], nodupKeys := ⋯ }

@[simp]

theorem AList.singleton_entries {α : Type u} {β : α → Type v} (a : α) (b : β a) : (AList.singleton a b).entries = [{ fst := a, snd := b }]

@[simp]

theorem AList.keys_singleton {α : Type u} {β : α → Type v} (a : α) (b : β a) : AList.keys (AList.singleton a b) = [a]

lookup

def AList.lookup {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Option (β a)

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

Equations

• AList.lookup a s = List.dlookup a s.entries

@[simp]

theorem AList.lookup_empty {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : AList.lookup a ∅ = none

theorem AList.lookup_isSome {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : AList β} : Option.isSome (AList.lookup a s) = true ↔ a ∈ s

theorem AList.lookup_eq_none {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : AList β} : AList.lookup a s = none ↔ a ∉ s

theorem AList.mem_lookup_iff {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : AList β} : b ∈ AList.lookup a s ↔ { fst := a, snd := b } ∈ s.entries

theorem AList.perm_lookup {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} (p : List.Perm s₁.entries s₂.entries) : AList.lookup a s₁ = AList.lookup a s₂

instance AList.instDecidableMemAListInstMembershipAList {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Decidable (a ∈ s)

Equations

• AList.instDecidableMemAListInstMembershipAList a s = decidable_of_iff (Option.isSome (AList.lookup a s) = true) ⋯

theorem AList.keys_subset_keys_of_entries_subset_entries {α : Type u} {β : α → Type v} {s₁ : AList β} {s₂ : AList β} (h : s₁.entries ⊆ s₂.entries) : AList.keys s₁ ⊆ AList.keys s₂

replace

def AList.replace {α : Type u} {β : α → Type v} [DecidableEq α] (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 := ⋯ }

@[simp]

theorem AList.keys_replace {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (s : AList β) : AList.keys (AList.replace a b s) = AList.keys s

@[simp]

theorem AList.mem_replace {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {b : β a} {s : AList β} : a' ∈ AList.replace a b s ↔ a' ∈ s

theorem AList.perm_replace {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} : List.Perm s₁.entries s₂.entries → List.Perm (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 (fun (r : δ) (a : Sigma β) => f r a.fst a.snd) d m.entries

erase

def AList.erase {α : Type u} {β : α → Type v} [DecidableEq α] (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 := ⋯ }

@[simp]

theorem AList.keys_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : AList.keys (AList.erase a s) = List.erase (AList.keys s) a

@[simp]

theorem AList.mem_erase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {a' : α} {s : AList β} : a' ∈ AList.erase a s ↔ a' ≠ a ∧ a' ∈ s

theorem AList.perm_erase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} : List.Perm s₁.entries s₂.entries → List.Perm (AList.erase a s₁).entries (AList.erase a s₂).entries

@[simp]

theorem AList.lookup_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : AList.lookup a (AList.erase a s) = none

@[simp]

theorem AList.lookup_erase_ne {α : Type u} {β : α → Type v} [DecidableEq α] {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} [DecidableEq α] (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} [DecidableEq α] (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 := ⋯ }

@[simp]

theorem AList.insert_entries {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : AList β} : (AList.insert a b s).entries = { fst := a, snd := b } :: List.kerase a s.entries

theorem AList.insert_entries_of_neg {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : AList β} (h : a ∉ s) : (AList.insert a b s).entries = { fst := a, snd := b } :: s.entries

theorem AList.insert_of_neg {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s : AList β} (h : a ∉ s) : AList.insert a b s = { entries := { fst := a, snd := b } :: s.entries, nodupKeys := ⋯ }

@[simp]

theorem AList.insert_empty {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) : AList.insert a b ∅ = AList.singleton a b

@[simp]

theorem AList.mem_insert {α : Type u} {β : α → Type v} [DecidableEq α] {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} [DecidableEq α] {a : α} {b : β a} (s : AList β) : AList.keys (AList.insert a b s) = a :: List.erase (AList.keys s) a

theorem AList.perm_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} (p : List.Perm s₁.entries s₂.entries) : List.Perm (AList.insert a b s₁).entries (AList.insert a b s₂).entries

@[simp]

theorem AList.lookup_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} (s : AList β) : AList.lookup a (AList.insert a b s) = some b

@[simp]

theorem AList.lookup_insert_ne {α : Type u} {β : α → Type v} [DecidableEq α] {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_insert_eq_none {α : Type u} {β : α → Type v} [DecidableEq α] {l : AList β} {k : α} {k' : α} {v : β k} : AList.lookup k' (AList.insert k v l) = none ↔ k' ≠ k ∧ AList.lookup k' l = none

@[simp]

theorem AList.lookup_to_alist {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} (s : List (Sigma β)) : AList.lookup a (List.toAList s) = List.dlookup a s

@[simp]

theorem AList.insert_insert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {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} [DecidableEq α] {a : α} {a' : α} {b : β a} {b' : β a'} (s : AList β) (h : a ≠ a') : List.Perm (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} [DecidableEq α] {a : α} {b : β a} {b' : β a} : AList.insert a b (AList.singleton a b') = AList.singleton a b

@[simp]

theorem AList.entries_toAList {α : Type u} {β : α → Type v} [DecidableEq α] (xs : List (Sigma β)) : (List.toAList xs).entries = List.dedupKeys xs

theorem AList.toAList_cons {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (xs : List (Sigma β)) : List.toAList ({ fst := a, snd := b } :: xs) = AList.insert a b (List.toAList xs)

theorem AList.mk_cons_eq_insert {α : Type u} {β : α → Type v} [DecidableEq α] (c : Sigma β) (l : List (Sigma β)) (h : List.NodupKeys (c :: l)) : { entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := ⋯ }

def AList.insertRec {α : Type u} {β : α → Type v} [DecidableEq α] {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.insertRec.

Equations

• AList.insertRec H0 IH { entries := [], nodupKeys := nodupKeys } = H0
• AList.insertRec H0 IH { entries := c :: l, nodupKeys := h } = Eq.mpr ⋯ (IH c.fst c.snd { entries := l, nodupKeys := ⋯ } ⋯ (AList.insertRec H0 IH { entries := l, nodupKeys := ⋯ }))

@[simp]

theorem AList.insertRec_empty {α : Type u} {β : α → Type v} [DecidableEq α] {C : AList β → Sort u_1} (H0 : C ∅) (IH : (a : α) → (b : β a) → (l : AList β) → a ∉ l → C l → C (AList.insert a b l)) : AList.insertRec H0 IH ∅ = H0

theorem AList.insertRec_insert {α : Type u} {β : α → Type v} [DecidableEq α] {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.insertRec H0 IH (AList.insert c.fst c.snd l) = IH c.fst c.snd l h (AList.insertRec H0 IH l)

theorem AList.insertRec_insert_mk {α : Type u} {β : α → Type v} [DecidableEq α] {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.insertRec H0 IH (AList.insert a b l) = IH a b l h (AList.insertRec H0 IH l)

extract

def AList.extract {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : Option (β a) × AList β

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

Equations

• AList.extract a s = let_fun this := ⋯; match List.kextract a s.entries, this with | (b, l), h => (b, { entries := l, nodupKeys := h })

@[simp]

theorem AList.extract_eq_lookup_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s : AList β) : AList.extract a s = (AList.lookup a s, AList.erase a s)

union

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

• AList.union s₁ s₂ = { entries := List.kunion s₁.entries s₂.entries, nodupKeys := ⋯ }

instance AList.instUnionAList {α : Type u} {β : α → Type v} [DecidableEq α] : Union (AList β)

Equations

• AList.instUnionAList = { union := AList.union }

@[simp]

theorem AList.union_entries {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} : (s₁ ∪ s₂).entries = List.kunion s₁.entries s₂.entries

@[simp]

theorem AList.empty_union {α : Type u} {β : α → Type v} [DecidableEq α] {s : AList β} : ∅ ∪ s = s

@[simp]

theorem AList.union_empty {α : Type u} {β : α → Type v} [DecidableEq α] {s : AList β} : s ∪ ∅ = s

@[simp]

theorem AList.mem_union {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} : a ∈ s₁ ∪ s₂ ↔ a ∈ s₁ ∨ a ∈ s₂

theorem AList.perm_union {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} {s₃ : AList β} {s₄ : AList β} (p₁₂ : List.Perm s₁.entries s₂.entries) (p₃₄ : List.Perm s₃.entries s₄.entries) : List.Perm (s₁ ∪ s₃).entries (s₂ ∪ s₄).entries

theorem AList.union_erase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (s₁ : AList β) (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} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} : a ∈ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₁

@[simp]

theorem AList.lookup_union_right {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s₁ : AList β} {s₂ : AList β} : a ∉ s₁ → AList.lookup a (s₁ ∪ s₂) = AList.lookup a s₂

theorem AList.mem_lookup_union {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} : b ∈ AList.lookup a (s₁ ∪ s₂) ↔ b ∈ AList.lookup a s₁ ∨ a ∉ s₁ ∧ b ∈ AList.lookup a s₂

@[simp]

theorem AList.lookup_union_eq_some {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} : AList.lookup a (s₁ ∪ s₂) = some b ↔ AList.lookup a s₁ = some b ∨ a ∉ s₁ ∧ AList.lookup a s₂ = some b

theorem AList.mem_lookup_union_middle {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} {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} [DecidableEq α] {a : α} {b : β a} {s₁ : AList β} {s₂ : AList β} : AList.insert a b (s₁ ∪ s₂) = AList.insert a b s₁ ∪ s₂

theorem AList.union_assoc {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} {s₃ : AList β} : List.Perm (s₁ ∪ s₂ ∪ s₃).entries (s₁ ∪ (s₂ ∪ s₃)).entries

disjoint

def AList.Disjoint {α : Type u} {β : α → Type v} (s₁ : AList β) (s₂ : AList β) : Prop

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

Equations

• AList.Disjoint s₁ s₂ = ∀ k ∈ AList.keys s₁, k ∉ AList.keys s₂

theorem AList.union_comm_of_disjoint {α : Type u} {β : α → Type v} [DecidableEq α] {s₁ : AList β} {s₂ : AList β} (h : AList.Disjoint s₁ s₂) : List.Perm (s₁ ∪ s₂).entries (s₂ ∪ s₁).entries