# Documentation

Mathlib.Data.List.Sigma

# Utilities for lists of sigmas #

This file includes several ways of interacting with List (Sigma β), treated as a key-value store.

If α : Type _ and β : α → Type _→ Type _, then we regard s : Sigma β as having key s.1 : α and value s.2 : β s.1. Hence, list (sigma β) behaves like a key-value store.

## Main Definitions #

• List.keys extracts the list of keys.
• List.NodupKeys determines if the store has duplicate keys.
• List.lookup/lookup_all accesses the value(s) of a particular key.
• List.kreplace replaces the first value with a given key by a given value.
• List.kerase removes a value.
• List.kinsert inserts a value.
• List.kunion computes the union of two stores.
• List.kextract returns a value with a given key and the rest of the values.

### keys#

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

List of keys from a list of key-value pairs

Equations
@[simp]
theorem List.keys_nil {α : Type u} {β : αType v} :
= []
@[simp]
theorem List.keys_cons {α : Type u} {β : αType v} {s : } {l : List ()} :
List.keys (s :: l) = s.fst ::
theorem List.mem_keys_of_mem {α : Type u} {β : αType v} {s : } {l : List ()} :
s ls.fst
theorem List.exists_of_mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} (h : a ) :
b, { fst := a, snd := b } l
theorem List.mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} :
a b, { fst := a, snd := b } l
theorem List.not_mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} :
¬a ∀ (b : β a), ¬{ fst := a, snd := b } l
theorem List.not_eq_key {α : Type u} {β : αType v} {a : α} {l : List ()} :
¬a ∀ (s : ), s la s.fst

### NodupKeys#

def List.NodupKeys {α : Type u} {β : αType v} (l : List ()) :

Determines whether the store uses a key several times.

Equations
theorem List.nodupKeys_iff_pairwise {α : Type u} {β : αType v} {l : List ()} :
List.Pairwise (fun s s' => s.fst s'.fst) l
theorem List.NodupKeys.pairwise_ne {α : Type u} {β : αType v} {l : List ()} (h : ) :
List.Pairwise (fun s s' => s.fst s'.fst) l
@[simp]
theorem List.nodupKeys_nil {α : Type u} {β : αType v} :
@[simp]
theorem List.nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} :
theorem List.not_mem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} (h : List.NodupKeys (s :: l)) :
¬s.fst
theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} (h : List.NodupKeys (s :: l)) :
theorem List.NodupKeys.eq_of_fst_eq {α : Type u} {β : αType v} {l : List ()} (nd : ) {s : } {s' : } (h : s l) (h' : s' l) :
s.fst = s'.fsts = s'
theorem List.NodupKeys.eq_of_mk_mem {α : Type u} {β : αType v} {a : α} {b : β a} {b' : β a} {l : List ()} (nd : ) (h : { fst := a, snd := b } l) (h' : { fst := a, snd := b' } l) :
b = b'
theorem List.nodupKeys_singleton {α : Type u} {β : αType v} (s : ) :
theorem List.NodupKeys.sublist {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} (h : List.Sublist l₁ l₂) :
theorem List.NodupKeys.nodup {α : Type u} {β : αType v} {l : List ()} :
theorem List.perm_nodupKeys {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} (h : l₁ ~ l₂) :
theorem List.nodupKeys_join {α : Type u} {β : αType v} {L : List (List ())} :
(∀ (l : List ()), l L) List.Pairwise List.Disjoint (List.map List.keys L)
theorem List.nodup_enum_map_fst {α : Type u} (l : List α) :
List.Nodup (List.map Prod.fst ())
theorem List.mem_ext {α : Type u} {β : αType v} {l₀ : List ()} {l₁ : List ()} (nd₀ : ) (nd₁ : ) (h : ∀ (x : ), x l₀ x l₁) :
l₀ ~ l₁

### dlookup#

def List.dlookup {α : Type u} {β : αType v} [inst : ] (a : α) :
List ()Option (β a)

dlookup a l is the first value in l corresponding to the key a, or none if no such element exists.

Equations
@[simp]
theorem List.dlookup_nil {α : Type u} {β : αType v} [inst : ] (a : α) :
List.dlookup a [] = none
@[simp]
theorem List.dlookup_cons_eq {α : Type u} {β : αType v} [inst : ] (l : List ()) (a : α) (b : β a) :
List.dlookup a ({ fst := a, snd := b } :: l) = some b
@[simp]
theorem List.dlookup_cons_ne {α : Type u} {β : αType v} [inst : ] (l : List ()) {a : α} (s : ) :
a s.fstList.dlookup a (s :: l) =
theorem List.dlookup_isSome {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} :
a
theorem List.dlookup_eq_none {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} :
= none ¬a
theorem List.of_mem_dlookup {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} :
b { fst := a, snd := b } l
theorem List.mem_dlookup {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} (nd : ) (h : { fst := a, snd := b } l) :
b
theorem List.map_dlookup_eq_find {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
Option.map () () = List.find? (fun s => decide (a = s.fst)) l
theorem List.mem_dlookup_iff {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} (nd : ) :
b { fst := a, snd := b } l
theorem List.perm_dlookup {α : Type u} {β : αType v} [inst : ] (a : α) {l₁ : List ()} {l₂ : List ()} (nd₁ : ) (nd₂ : ) (p : l₁ ~ l₂) :
theorem List.lookup_ext {α : Type u} {β : αType v} [inst : ] {l₀ : List ()} {l₁ : List ()} (nd₀ : ) (nd₁ : ) (h : ∀ (x : α) (y : β x), y List.dlookup x l₀ y List.dlookup x l₁) :
l₀ ~ l₁

### lookup_all#

def List.lookupAll {α : Type u} {β : αType v} [inst : ] (a : α) :
List ()List (β a)

lookup_all a l is the list of all values in l corresponding to the key a.

Equations
@[simp]
theorem List.lookupAll_nil {α : Type u} {β : αType v} [inst : ] (a : α) :
= []
@[simp]
theorem List.lookupAll_cons_eq {α : Type u} {β : αType v} [inst : ] (l : List ()) (a : α) (b : β a) :
List.lookupAll a ({ fst := a, snd := b } :: l) = b ::
@[simp]
theorem List.lookupAll_cons_ne {α : Type u} {β : αType v} [inst : ] (l : List ()) {a : α} (s : ) :
a s.fstList.lookupAll a (s :: l) =
theorem List.lookupAll_eq_nil {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} :
= [] ∀ (b : β a), ¬{ fst := a, snd := b } l
theorem List.head?_lookupAll {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
theorem List.mem_lookupAll {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} :
b { fst := a, snd := b } l
theorem List.lookupAll_sublist {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
theorem List.lookupAll_length_le_one {α : Type u} {β : αType v} [inst : ] (a : α) {l : List ()} (h : ) :
1
theorem List.lookupAll_eq_dlookup {α : Type u} {β : αType v} [inst : ] (a : α) {l : List ()} (h : ) :
=
theorem List.lookupAll_nodup {α : Type u} {β : αType v} [inst : ] (a : α) {l : List ()} (h : ) :
theorem List.perm_lookupAll {α : Type u} {β : αType v} [inst : ] (a : α) {l₁ : List ()} {l₂ : List ()} (nd₁ : ) (nd₂ : ) (p : l₁ ~ l₂) :
=

### kreplace#

def List.kreplace {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) :
List ()List ()

Replaces the first value with key a by b.

Equations
theorem List.kreplace_of_forall_not {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) {l : List ()} (H : ∀ (b : β a), ¬{ fst := a, snd := b } l) :
= l
theorem List.kreplace_self {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} (nd : ) (h : { fst := a, snd := b } l) :
= l
theorem List.keys_kreplace {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) (l : List ()) :
theorem List.kreplace_nodupKeys {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) {l : List ()} :
theorem List.Perm.kreplace {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} (nd : ) :
l₁ ~ l₂List.kreplace a b l₁ ~ List.kreplace a b l₂

### kerase#

def List.kerase {α : Type u} {β : αType v} [inst : ] (a : α) :
List ()List ()

Remove the first pair with the key a.

Equations
theorem List.kerase_nil {α : Type u} {β : αType v} [inst : ] {a : α} :
List.kerase a [] = []
@[simp]
theorem List.kerase_cons_eq {α : Type u} {β : αType v} [inst : ] {a : α} {s : } {l : List ()} (h : a = s.fst) :
List.kerase a (s :: l) = l
@[simp]
theorem List.kerase_cons_ne {α : Type u} {β : αType v} [inst : ] {a : α} {s : } {l : List ()} (h : a s.fst) :
List.kerase a (s :: l) = s ::
@[simp]
theorem List.kerase_of_not_mem_keys {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} (h : ¬a ) :
= l
theorem List.kerase_sublist {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
theorem List.kerase_keys_subset {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : αType v} [inst : ] {a₁ : α} {a₂ : α} {l : List ()} :
a₁ List.keys (List.kerase a₂ l)a₁
theorem List.exists_of_kerase {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} (h : a ) :
b l₁ l₂, ¬a l = l₁ ++ { fst := a, snd := b } :: l₂ = l₁ ++ l₂
@[simp]
theorem List.mem_keys_kerase_of_ne {α : Type u} {β : αType v} [inst : ] {a₁ : α} {a₂ : α} {l : List ()} (h : a₁ a₂) :
a₁ List.keys (List.kerase a₂ l) a₁
theorem List.keys_kerase {α : Type u} {β : αType v} [inst : ] {a : α} {l : List ()} :
theorem List.kerase_kerase {α : Type u} {β : αType v} [inst : ] {a : α} {a' : α} {l : List ()} :
theorem List.NodupKeys.kerase {α : Type u} {β : αType v} {l : List ()} [inst : ] (a : α) :
theorem List.Perm.kerase {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} (nd : ) :
l₁ ~ l₂List.kerase a l₁ ~ List.kerase a l₂
@[simp]
theorem List.not_mem_keys_kerase {α : Type u} {β : αType v} [inst : ] (a : α) {l : List ()} (nd : ) :
@[simp]
theorem List.dlookup_kerase {α : Type u} {β : αType v} [inst : ] (a : α) {l : List ()} (nd : ) :
List.dlookup a () = none
@[simp]
theorem List.dlookup_kerase_ne {α : Type u} {β : αType v} [inst : ] {a : α} {a' : α} {l : List ()} (h : a a') :
theorem List.kerase_append_left {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} :
a List.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
theorem List.kerase_append_right {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} :
¬a List.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
theorem List.kerase_comm {α : Type u} {β : αType v} [inst : ] (a₁ : α) (a₂ : α) (l : List ()) :
List.kerase a₂ (List.kerase a₁ l) = List.kerase a₁ (List.kerase a₂ l)
theorem List.sizeOf_kerase {α : Type u_1} {β : αType u_2} [inst : ] [inst : SizeOf ()] (x : α) (xs : List ()) :

### kinsert#

def List.kinsert {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) (l : List ()) :
List ()

Insert the pair ⟨a, b⟩ and erase the first pair with the key a.

Equations
@[simp]
theorem List.kinsert_def {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l : List ()} :
List.kinsert a b l = { fst := a, snd := b } ::
theorem List.mem_keys_kinsert {α : Type u} {β : αType v} [inst : ] {a : α} {a' : α} {b' : β a'} {l : List ()} :
a List.keys (List.kinsert a' b' l) a = a' a
theorem List.kinsert_nodupKeys {α : Type u} {β : αType v} [inst : ] (a : α) (b : β a) {l : List ()} (nd : ) :
theorem List.Perm.kinsert {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} (nd₁ : ) (p : l₁ ~ l₂) :
List.kinsert a b l₁ ~ List.kinsert a b l₂
theorem List.dlookup_kinsert {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} (l : List ()) :
theorem List.dlookup_kinsert_ne {α : Type u} {β : αType v} [inst : ] {a : α} {a' : α} {b' : β a'} {l : List ()} (h : a a') :

### kextract#

def List.kextract {α : Type u} {β : αType v} [inst : ] (a : α) :
List ()Option (β a) × List ()

Finds the first entry with a given key a and returns its value (as an option because there might be no entry with key a) alongside with the rest of the entries.

Equations
@[simp]
theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
= (, )

### dedupKeys#

def List.dedupKeys {α : Type u} {β : αType v} [inst : ] :
List ()List ()

Remove entries with duplicate keys from l : list (sigma β).

Equations
theorem List.dedupKeys_cons {α : Type u} {β : αType v} [inst : ] {x : } (l : List ()) :
List.dedupKeys (x :: l) = List.kinsert x.fst x.snd ()
theorem List.nodupKeys_dedupKeys {α : Type u} {β : αType v} [inst : ] (l : List ()) :
theorem List.dlookup_dedupKeys {α : Type u} {β : αType v} [inst : ] (a : α) (l : List ()) :
=
theorem List.sizeOf_dedupKeys {α : Type u_1} {β : αType u_2} [inst : ] [inst : SizeOf ()] (xs : List ()) :

### kunion#

def List.kunion {α : Type u} {β : αType v} [inst : ] :
List ()List ()List ()

kunion l₁ l₂ is the append to l₁ of l₂ after, for each key in l₁, the first matching pair in l₂ is erased.

Equations
@[simp]
theorem List.nil_kunion {α : Type u} {β : αType v} [inst : ] {l : List ()} :
List.kunion [] l = l
@[simp]
theorem List.kunion_nil {α : Type u} {β : αType v} [inst : ] {l : List ()} :
List.kunion l [] = l
@[simp]
theorem List.kunion_cons {α : Type u} {β : αType v} [inst : ] {s : } {l₁ : List ()} {l₂ : List ()} :
List.kunion (s :: l₁) l₂ = s :: List.kunion l₁ (List.kerase s.fst l₂)
@[simp]
theorem List.mem_keys_kunion {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} :
a List.keys (List.kunion l₁ l₂) a a
@[simp]
theorem List.kunion_kerase {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} :
theorem List.NodupKeys.kunion {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} [inst : ] (nd₁ : ) (nd₂ : ) :
theorem List.Perm.kunion_right {α : Type u} {β : αType v} [inst : ] {l₁ : List ()} {l₂ : List ()} (p : l₁ ~ l₂) (l : List ()) :
List.kunion l₁ l ~ List.kunion l₂ l
theorem List.Perm.kunion_left {α : Type u} {β : αType v} [inst : ] (l : List ()) {l₁ : List ()} {l₂ : List ()} :
l₁ ~ l₂List.kunion l l₁ ~ List.kunion l l₂
theorem List.Perm.kunion {α : Type u} {β : αType v} [inst : ] {l₁ : List ()} {l₂ : List ()} {l₃ : List ()} {l₄ : List ()} (nd₃ : ) (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) :
List.kunion l₁ l₃ ~ List.kunion l₂ l₄
@[simp]
theorem List.dlookup_kunion_left {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} (h : a ) :
List.dlookup a (List.kunion l₁ l₂) = List.dlookup a l₁
@[simp]
theorem List.dlookup_kunion_right {α : Type u} {β : αType v} [inst : ] {a : α} {l₁ : List ()} {l₂ : List ()} (h : ¬a ) :
List.dlookup a (List.kunion l₁ l₂) = List.dlookup a l₂
theorem List.mem_dlookup_kunion {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} :
@[simp]
theorem List.dlookup_kunion_eq_some {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} :
theorem List.mem_dlookup_kunion_middle {α : Type u} {β : αType v} [inst : ] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} {l₃ : List ()} (h₁ : b List.dlookup a (List.kunion l₁ l₃)) (h₂ : ¬a ) :
b List.dlookup a (List.kunion (List.kunion l₁ l₂) l₃)