# 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 : List.NodupKeys self.entries

There are no duplicate keys in entries

Instances For
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
• = { entries := , 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.instDecidableEqAList {α : Type u} {β : αType v} [] [(a : α) → DecidableEq (β a)] :
Equations

### keys #

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

The list of keys of an association list.

Equations
Instances For
theorem AList.keys_nodup {α : Type u} {β : αType v} (s : ) :

### mem #

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

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

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

### empty #

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

The empty association list.

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

### singleton #

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

The singleton association list.

Equations
• = { entries := [{ fst := a, snd := b }], nodupKeys := }
Instances For
@[simp]
theorem AList.singleton_entries {α : Type u} {β : αType v} (a : α) (b : β a) :
().entries = [{ fst := a, snd := b }]
@[simp]
theorem AList.keys_singleton {α : Type u} {β : αType v} (a : α) (b : β a) :
= [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 : } :
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 { fst := a, snd := b } s.entries
theorem AList.perm_lookup {α : Type u} {β : αType v} [] {a : α} {s₁ : } {s₂ : } (p : List.Perm s₁.entries s₂.entries) :
instance AList.instDecidableMemAListInstMembershipAList {α : 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) :

### 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 : ) :
@[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₂ : } :
List.Perm s₁.entries s₂.entriesList.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 : ) :
δ

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 : ) :
@[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₂ : } :
List.Perm s₁.entries s₂.entriesList.Perm (AList.erase a s₁).entries (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 = { fst := a, snd := 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 = { fst := a, snd := b } :: s.entries
theorem AList.insert_of_neg {α : Type u} {β : αType v} [] {a : α} {b : β a} {s : } (h : as) :
AList.insert a b s = { entries := { fst := a, snd := 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 : ) :
theorem AList.perm_insert {α : Type u} {β : αType v} [] {a : α} {b : β a} {s₁ : } {s₂ : } (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} [] {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 ()) :
=
@[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') :
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} [] {a : α} {b : β a} {b' : β a} :
AList.insert a b () =
@[simp]
theorem AList.entries_toAList {α : Type u} {β : αType v} [] (xs : List ()) :
().entries =
theorem AList.toAList_cons {α : Type u} {β : αType v} [] (a : α) (b : β a) (xs : List ()) :
List.toAList ({ fst := a, snd := b } :: xs) = AList.insert a b ()
theorem AList.mk_cons_eq_insert {α : Type u} {β : αType v} [] (c : ) (l : List ()) (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} [] {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 using AList.insertRec.

Equations
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
Instances For
instance AList.instUnionAList {α : Type u} {β : αType v} [] :
Equations
• AList.instUnionAList = { union := AList.union }
@[simp]
theorem AList.union_entries {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } :
(s₁ s₂).entries = List.kunion s₁.entries 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₁₂ : 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} [] (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₃ : } :
List.Perm (s₁ s₂ s₃).entries (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
Instances For
theorem AList.union_comm_of_disjoint {α : Type u} {β : αType v} [] {s₁ : } {s₂ : } (h : AList.Disjoint s₁ s₂) :
List.Perm (s₁ s₂).entries (s₂ s₁).entries