# 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 ()

The underlying List of an AList

• nodupKeys : self.entries.NodupKeys

There are no duplicate keys in entries

Instances For
theorem AList.nodupKeys {α : Type u} {β : αType v} (self : ) :
self.entries.NodupKeys

There are no duplicate keys in entries

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

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

Equations
• l.toAList = { entries := l.dedupKeys, nodupKeys := }
Instances For
theorem AList.ext {α : Type u} {β : αType v} {s : } {t : } :
s.entries = t.entriess = t
theorem AList.ext_iff {α : Type u} {β : αType v} {s : } {t : } :
s = t s.entries = t.entries
instance AList.instDecidableEq {α : Type u} {β : αType v} [] [(a : α) → DecidableEq (β a)] :
Equations
• xs.instDecidableEq ys = .mpr inferInstance

### keys #

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

The list of keys of an association list.

Equations
• s.keys = s.entries.keys
Instances For
theorem AList.keys_nodup {α : Type u} {β : αType v} (s : ) :
s.keys.Nodup

### mem #

instance AList.instMembership {α : Type u} {β : αType v} :

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

Equations
• AList.instMembership = { mem := fun (a : α) (s : ) => a s.keys }
theorem AList.mem_keys {α : Type u} {β : αType v} {a : α} {s : } :
a s a s.keys
theorem AList.mem_of_perm {α : Type u} {β : αType v} {a : α} {s₁ : } {s₂ : } (p : s₁.entries.Perm s₂.entries) :
a s₁ a s₂

### empty #

instance AList.instEmptyCollection {α : Type u} {β : αType v} :

The empty association list.

Equations
• AList.instEmptyCollection = { emptyCollection := { entries := [], nodupKeys := } }
instance AList.instInhabited {α : Type u} {β : αType v} :
Equations
• AList.instInhabited = { 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} :
.keys = []

### singleton #

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

The singleton association list.

Equations
• = { entries := [a, b], nodupKeys := }
Instances For
@[simp]
theorem AList.singleton_entries {α : Type u} {β : αType v} (a : α) (b : β a) :
().entries = [a, b]
@[simp]
theorem AList.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
().keys = [a]

### lookup #

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

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

Equations
Instances For
@[simp]
theorem AList.lookup_empty {α : Type u} {β : αType v} [] (a : α) :
= none
theorem AList.lookup_isSome {α : Type u} {β : αType v} [] {a : α} {s : } :
().isSome = true a s
theorem AList.lookup_eq_none {α : Type u} {β : αType v} [] {a : α} {s : } :
= none as
theorem AList.mem_lookup_iff {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } :
b a, b s.entries
theorem AList.perm_lookup {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } (p : s₁.entries.Perm s₂.entries) :
instance AList.instDecidableMem {α : Type u} {β : αType v} [] (a : α) (s : ) :
Equations
theorem AList.keys_subset_keys_of_entries_subset_entries {α : Type u} {β : αType v} {s₁ : } {s₂ : } (h : s₁.entries s₂.entries) :
s₁.keys s₂.keys

### replace #

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

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

Equations
Instances For
@[simp]
theorem AList.keys_replace {α : Type u} {β : αType v} [] (a : α) (b : β a) (s : ) :
().keys = s.keys
@[simp]
theorem AList.mem_replace {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {s : } :
a' a' s
theorem AList.perm_replace {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
s₁.entries.Perm s₂.entries(AList.replace a b s₁).entries.Perm (AList.replace a b s₂).entries
def AList.foldl {α : Type u} {β : αType v} {δ : Type w} (f : δ(a : α) → β aδ) (d : δ) (m : ) :
δ

Fold a function over the key-value pairs in the map.

Equations
Instances For

### erase #

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

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

Equations
Instances For
@[simp]
theorem AList.keys_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
().keys = s.keys.erase a
@[simp]
theorem AList.mem_erase {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } :
a' a' a a' s
theorem AList.perm_erase {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
s₁.entries.Perm s₂.entries(AList.erase a s₁).entries.Perm (AList.erase a s₂).entries
@[simp]
theorem AList.lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
AList.lookup a () = none
@[simp]
theorem AList.lookup_erase_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {s : } (h : a a') :
theorem AList.erase_erase {α : Type u} {β : αType v} [] (a : α) (a' : α) (s : ) :

### insert #

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

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

Equations
Instances For
@[simp]
theorem AList.insert_entries {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } :
(AList.insert a b s).entries = a, b :: List.kerase a s.entries
theorem AList.insert_entries_of_neg {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } (h : as) :
(AList.insert a b s).entries = a, b :: s.entries
theorem AList.insert_of_neg {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } (h : as) :
AList.insert a b s = { entries := a, b :: s.entries, nodupKeys := }
@[simp]
theorem AList.insert_empty {α : Type u} {β : αType v} [] (a : α) (b : β a) :
=
@[simp]
theorem AList.mem_insert {α : Type u} {β : αType v} [] {a : α} {a' : α} {b' : β a'} (s : ) :
a AList.insert a' b' s a = a' a s
@[simp]
theorem AList.keys_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} (s : ) :
(AList.insert a b s).keys = a :: s.keys.erase a
theorem AList.perm_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } (p : s₁.entries.Perm s₂.entries) :
(AList.insert a b s₁).entries.Perm (AList.insert a b s₂).entries
@[simp]
theorem AList.lookup_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} (s : ) :
@[simp]
theorem AList.lookup_insert_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b' : β a'} {s : } (h : a a') :
@[simp]
theorem AList.lookup_insert_eq_none {α : Type u} {β : αType v} [] {l : } {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} [] {a : α} (s : List ()) :
AList.lookup a s.toAList =
@[simp]
theorem AList.insert_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} (s : ) :
theorem AList.insert_insert_of_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {b : β a} {b' : β a'} (s : ) (h : a a') :
(AList.insert a' b' (AList.insert a b s)).entries.Perm (AList.insert a b (AList.insert a' b' s)).entries
@[simp]
theorem AList.insert_singleton_eq {α : Type u} {β : αType v} [] {a : α} {b : β a} {b' : β a} :
AList.insert a b () =
@[simp]
theorem AList.entries_toAList {α : Type u} {β : αType v} [] (xs : List ()) :
xs.toAList.entries = xs.dedupKeys
theorem AList.toAList_cons {α : Type u} {β : αType v} [] (a : α) (b : β a) (xs : List ()) :
(a, b :: xs).toAList = AList.insert a b xs.toAList
theorem AList.mk_cons_eq_insert {α : Type u} {β : αType v} [] (c : ) (l : List ()) (h : (c :: l).NodupKeys) :
{ entries := c :: l, nodupKeys := h } = AList.insert c.fst c.snd { entries := l, nodupKeys := }
@[irreducible]
def AList.insertRec {α : Type u} {β : αType v} [] {C : Sort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : ) → alC lC (AList.insert a b l)) (l : ) :
C l

Recursion on an AList, using insert. Use as induction l.

Equations
• AList.insertRec H0 IH { entries := [], nodupKeys := nodupKeys } = H0
• AList.insertRec H0 IH { entries := c :: l, nodupKeys := h } = .mpr (IH c.fst c.snd { entries := l, nodupKeys := } (AList.insertRec H0 IH { entries := l, nodupKeys := }))
Instances For
@[simp]
theorem AList.insertRec_empty {α : Type u} {β : αType v} [] {C : Sort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : ) → alC lC (AList.insert a b l)) :
theorem AList.insertRec_insert {α : Type u} {β : αType v} [] {C : Sort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : ) → alC lC (AList.insert a b l)) {c : } {l : } (h : c.fstl) :
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} [] {C : Sort u_1} (H0 : C ) (IH : (a : α) → (b : β a) → (l : ) → alC lC (AList.insert a b l)) {a : α} (b : β a) {l : } (h : al) :
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} [] (a : α) (s : ) :
Option (β a) ×

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

Equations
• = let_fun this := ; match List.kextract a s.entries, this with | (b, l), h => (b, { entries := l, nodupKeys := h })
Instances For
@[simp]
theorem AList.extract_eq_lookup_erase {α : Type u} {β : αType v} [] (a : α) (s : ) :
= (, )

### union #

def AList.union {α : Type u} {β : αType v} [] (s₁ : ) (s₂ : ) :

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 := }
Instances For
instance AList.instUnion {α : Type u} {β : αType v} [] :
Equations
• AList.instUnion = { union := AList.union }
@[simp]
theorem AList.union_entries {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
(s₁ s₂).entries = s₁.entries.kunion s₂.entries
@[simp]
theorem AList.empty_union {α : Type u} {β : αType v} [] {s : } :
s = s
@[simp]
theorem AList.union_empty {α : Type u} {β : αType v} [] {s : } :
s = s
@[simp]
theorem AList.mem_union {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁ s₂ a s₁ a s₂
theorem AList.perm_union {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } {s₃ : } {s₄ : } (p₁₂ : s₁.entries.Perm s₂.entries) (p₃₄ : s₃.entries.Perm s₄.entries) :
(s₁ s₃).entries.Perm (s₂ s₄).entries
theorem AList.union_erase {α : Type u} {β : αType v} [] (a : α) (s₁ : ) (s₂ : ) :
AList.erase a (s₁ s₂) = AList.erase a s₁ AList.erase a s₂
@[simp]
theorem AList.lookup_union_left {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
a s₁AList.lookup a (s₁ s₂) = AList.lookup a s₁
@[simp]
theorem AList.lookup_union_right {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } :
as₁AList.lookup a (s₁ s₂) = AList.lookup a s₂
theorem AList.mem_lookup_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
b AList.lookup a (s₁ s₂) b AList.lookup a s₁ as₁ b AList.lookup a s₂
@[simp]
theorem AList.lookup_union_eq_some {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
AList.lookup a (s₁ s₂) = some b AList.lookup a s₁ = some b as₁ AList.lookup a s₂ = some b
theorem AList.mem_lookup_union_middle {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } {s₃ : } :
b AList.lookup a (s₁ s₃)as₂b AList.lookup a (s₁ s₂ s₃)
theorem AList.insert_union {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } :
AList.insert a b (s₁ s₂) = AList.insert a b s₁ s₂
theorem AList.union_assoc {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } {s₃ : } :
(s₁ s₂ s₃).entries.Perm (s₁ (s₂ s₃)).entries

### disjoint #

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

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

Equations
• s₁.Disjoint s₂ = ks₁.keys, ks₂.keys
Instances For
theorem AList.union_comm_of_disjoint {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } (h : s₁.Disjoint s₂) :
(s₁ s₂).entries.Perm (s₂ s₁).entries