# 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*, 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
Instances For
@[simp]
theorem List.keys_nil {α : Type u} {β : αType v} :
[].keys = []
@[simp]
theorem List.keys_cons {α : Type u} {β : αType v} {s : } {l : List ()} :
(s :: l).keys = s.fst :: l.keys
theorem List.mem_keys_of_mem {α : Type u} {β : αType v} {s : } {l : List ()} :
s ls.fst l.keys
theorem List.exists_of_mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} (h : a l.keys) :
∃ (b : β a), a, b l
theorem List.mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} :
a l.keys ∃ (b : β a), a, b l
theorem List.not_mem_keys {α : Type u} {β : αType v} {a : α} {l : List ()} :
al.keys ∀ (b : β a), a, bl
theorem List.not_eq_key {α : Type u} {β : αType v} {a : α} {l : List ()} :
al.keys sl, a s.fst

### NodupKeys#

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

Determines whether the store uses a key several times.

Equations
• l.NodupKeys = l.keys.Nodup
Instances For
theorem List.nodupKeys_iff_pairwise {α : Type u} {β : αType v} {l : List ()} :
l.NodupKeys List.Pairwise (fun (s s' : ) => s.fst s'.fst) l
theorem List.NodupKeys.pairwise_ne {α : Type u} {β : αType v} {l : List ()} (h : l.NodupKeys) :
List.Pairwise (fun (s s' : ) => s.fst s'.fst) l
@[simp]
theorem List.nodupKeys_nil {α : Type u} {β : αType v} :
[].NodupKeys
@[simp]
theorem List.nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} :
(s :: l).NodupKeys s.fstl.keys l.NodupKeys
theorem List.not_mem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} (h : (s :: l).NodupKeys) :
s.fstl.keys
theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : } {l : List ()} (h : (s :: l).NodupKeys) :
l.NodupKeys
theorem List.NodupKeys.eq_of_fst_eq {α : Type u} {β : αType v} {l : List ()} (nd : l.NodupKeys) {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 : l.NodupKeys) (h : a, b l) (h' : a, b' l) :
b = b'
theorem List.nodupKeys_singleton {α : Type u} {β : αType v} (s : ) :
[s].NodupKeys
theorem List.NodupKeys.sublist {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} (h : l₁.Sublist l₂) :
l₂.NodupKeysl₁.NodupKeys
theorem List.NodupKeys.nodup {α : Type u} {β : αType v} {l : List ()} :
l.NodupKeysl.Nodup
theorem List.perm_nodupKeys {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} (h : l₁.Perm l₂) :
l₁.NodupKeys l₂.NodupKeys
theorem List.nodupKeys_join {α : Type u} {β : αType v} {L : List (List ())} :
L.join.NodupKeys (lL, l.NodupKeys) List.Pairwise List.Disjoint (List.map List.keys L)
theorem List.nodup_enum_map_fst {α : Type u} (l : List α) :
(List.map Prod.fst l.enum).Nodup
theorem List.mem_ext {α : Type u} {β : αType v} {l₀ : List ()} {l₁ : List ()} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup) (h : ∀ (x : ), x l₀ x l₁) :
l₀.Perm l₁

### dlookup#

def List.dlookup {α : Type u} {β : αType v} [] (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
Instances For
@[simp]
theorem List.dlookup_nil {α : Type u} {β : αType v} [] (a : α) :
List.dlookup a [] = none
@[simp]
theorem List.dlookup_cons_eq {α : Type u} {β : αType v} [] (l : List ()) (a : α) (b : β a) :
List.dlookup a (a, b :: l) = some b
@[simp]
theorem List.dlookup_cons_ne {α : Type u} {β : αType v} [] (l : List ()) {a : α} (s : ) :
a s.fstList.dlookup a (s :: l) =
theorem List.dlookup_isSome {α : Type u} {β : αType v} [] {a : α} {l : List ()} :
().isSome = true a l.keys
theorem List.dlookup_eq_none {α : Type u} {β : αType v} [] {a : α} {l : List ()} :
= none al.keys
theorem List.of_mem_dlookup {α : Type u} {β : αType v} [] {a : α} {b : β a} {l : List ()} :
b a, b l
theorem List.mem_dlookup {α : Type u} {β : αType v} [] {a : α} {b : β a} {l : List ()} (nd : l.NodupKeys) (h : a, b l) :
b
theorem List.map_dlookup_eq_find {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
Option.map () () = List.find? (fun (s : ) => decide (a = s.fst)) l
theorem List.mem_dlookup_iff {α : Type u} {β : αType v} [] {a : α} {b : β a} {l : List ()} (nd : l.NodupKeys) :
b a, b l
theorem List.perm_dlookup {α : Type u} {β : αType v} [] (a : α) {l₁ : List ()} {l₂ : List ()} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :
theorem List.lookup_ext {α : Type u} {β : αType v} [] {l₀ : List ()} {l₁ : List ()} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys) (h : ∀ (x : α) (y : β x), y List.dlookup x l₀ y List.dlookup x l₁) :
l₀.Perm l₁

### lookupAll#

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

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

Equations
Instances For
@[simp]
theorem List.lookupAll_nil {α : Type u} {β : αType v} [] (a : α) :
= []
@[simp]
theorem List.lookupAll_cons_eq {α : Type u} {β : αType v} [] (l : List ()) (a : α) (b : β a) :
List.lookupAll a (a, b :: l) = b ::
@[simp]
theorem List.lookupAll_cons_ne {α : Type u} {β : αType v} [] (l : List ()) {a : α} (s : ) :
a s.fstList.lookupAll a (s :: l) =
theorem List.lookupAll_eq_nil {α : Type u} {β : αType v} [] {a : α} {l : List ()} :
= [] ∀ (b : β a), a, bl
theorem List.head?_lookupAll {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
theorem List.mem_lookupAll {α : Type u} {β : αType v} [] {a : α} {b : β a} {l : List ()} :
b a, b l
theorem List.lookupAll_sublist {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
(List.map () ()).Sublist l
theorem List.lookupAll_length_le_one {α : Type u} {β : αType v} [] (a : α) {l : List ()} (h : l.NodupKeys) :
().length 1
theorem List.lookupAll_eq_dlookup {α : Type u} {β : αType v} [] (a : α) {l : List ()} (h : l.NodupKeys) :
= ().toList
theorem List.lookupAll_nodup {α : Type u} {β : αType v} [] (a : α) {l : List ()} (h : l.NodupKeys) :
().Nodup
theorem List.perm_lookupAll {α : Type u} {β : αType v} [] (a : α) {l₁ : List ()} {l₂ : List ()} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) :
=

### kreplace#

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

Replaces the first value with key a by b.

Equations
Instances For
theorem List.kreplace_of_forall_not {α : Type u} {β : αType v} [] (a : α) (b : β a) {l : List ()} (H : ∀ (b : β a), a, bl) :
= l
theorem List.kreplace_self {α : Type u} {β : αType v} [] {a : α} {b : β a} {l : List ()} (nd : l.NodupKeys) (h : a, b l) :
= l
theorem List.keys_kreplace {α : Type u} {β : αType v} [] (a : α) (b : β a) (l : List ()) :
().keys = l.keys
theorem List.kreplace_nodupKeys {α : Type u} {β : αType v} [] (a : α) (b : β a) {l : List ()} :
().NodupKeys l.NodupKeys
theorem List.Perm.kreplace {α : Type u} {β : αType v} [] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} (nd : l₁.NodupKeys) :
l₁.Perm l₂(List.kreplace a b l₁).Perm (List.kreplace a b l₂)

### kerase#

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

Remove the first pair with the key a.

Equations
Instances For
theorem List.kerase_nil {α : Type u} {β : αType v} [] {a : α} :
List.kerase a [] = []
@[simp]
theorem List.kerase_cons_eq {α : Type u} {β : αType v} [] {a : α} {s : } {l : List ()} (h : a = s.fst) :
List.kerase a (s :: l) = l
@[simp]
theorem List.kerase_cons_ne {α : Type u} {β : αType v} [] {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} [] {a : α} {l : List ()} (h : al.keys) :
= l
theorem List.kerase_sublist {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
().Sublist l
theorem List.kerase_keys_subset {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
().keys l.keys
theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : αType v} [] {a₁ : α} {a₂ : α} {l : List ()} :
a₁ (List.kerase a₂ l).keysa₁ l.keys
theorem List.exists_of_kerase {α : Type u} {β : αType v} [] {a : α} {l : List ()} (h : a l.keys) :
∃ (b : β a) (l₁ : List ()) (l₂ : List ()), al₁.keys l = l₁ ++ a, b :: l₂ = l₁ ++ l₂
@[simp]
theorem List.mem_keys_kerase_of_ne {α : Type u} {β : αType v} [] {a₁ : α} {a₂ : α} {l : List ()} (h : a₁ a₂) :
a₁ (List.kerase a₂ l).keys a₁ l.keys
theorem List.keys_kerase {α : Type u} {β : αType v} [] {a : α} {l : List ()} :
().keys = l.keys.erase a
theorem List.kerase_kerase {α : Type u} {β : αType v} [] {a : α} {a' : α} {l : List ()} :
theorem List.NodupKeys.kerase {α : Type u} {β : αType v} {l : List ()} [] (a : α) :
l.NodupKeys().NodupKeys
theorem List.Perm.kerase {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} (nd : l₁.NodupKeys) :
l₁.Perm l₂(List.kerase a l₁).Perm (List.kerase a l₂)
@[simp]
theorem List.not_mem_keys_kerase {α : Type u} {β : αType v} [] (a : α) {l : List ()} (nd : l.NodupKeys) :
a().keys
@[simp]
theorem List.dlookup_kerase {α : Type u} {β : αType v} [] (a : α) {l : List ()} (nd : l.NodupKeys) :
List.dlookup a () = none
@[simp]
theorem List.dlookup_kerase_ne {α : Type u} {β : αType v} [] {a : α} {a' : α} {l : List ()} (h : a a') :
theorem List.kerase_append_left {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} :
a l₁.keysList.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
theorem List.kerase_append_right {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} :
al₁.keysList.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
theorem List.kerase_comm {α : Type u} {β : αType v} [] (a₁ : α) (a₂ : α) (l : List ()) :
List.kerase a₂ (List.kerase a₁ l) = List.kerase a₁ (List.kerase a₂ l)
theorem List.sizeOf_kerase {α : Type u_2} {β : αType u_1} [] [SizeOf ()] (x : α) (xs : List ()) :

### kinsert#

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

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

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

### kextract#

def List.kextract {α : Type u} {β : αType v} [] (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
Instances For
@[simp]
theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : αType v} [] (a : α) (l : List ()) :
= (, )

### dedupKeys#

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

Remove entries with duplicate keys from l : List (Sigma β).

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

### kunion#

def List.kunion {α : Type u} {β : αType v} [] :
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
Instances For
@[simp]
theorem List.nil_kunion {α : Type u} {β : αType v} [] {l : List ()} :
[].kunion l = l
@[simp]
theorem List.kunion_nil {α : Type u} {β : αType v} [] {l : List ()} :
l.kunion [] = l
@[simp]
theorem List.kunion_cons {α : Type u} {β : αType v} [] {s : } {l₁ : List ()} {l₂ : List ()} :
(s :: l₁).kunion l₂ = s :: l₁.kunion (List.kerase s.fst l₂)
@[simp]
theorem List.mem_keys_kunion {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} :
a (l₁.kunion l₂).keys a l₁.keys a l₂.keys
@[simp]
theorem List.kunion_kerase {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} :
(List.kerase a l₁).kunion (List.kerase a l₂) = List.kerase a (l₁.kunion l₂)
theorem List.NodupKeys.kunion {α : Type u} {β : αType v} {l₁ : List ()} {l₂ : List ()} [] (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) :
(l₁.kunion l₂).NodupKeys
theorem List.Perm.kunion_right {α : Type u} {β : αType v} [] {l₁ : List ()} {l₂ : List ()} (p : l₁.Perm l₂) (l : List ()) :
(l₁.kunion l).Perm (l₂.kunion l)
theorem List.Perm.kunion_left {α : Type u} {β : αType v} [] (l : List ()) {l₁ : List ()} {l₂ : List ()} :
l₁.NodupKeysl₁.Perm l₂(l.kunion l₁).Perm (l.kunion l₂)
theorem List.Perm.kunion {α : Type u} {β : αType v} [] {l₁ : List ()} {l₂ : List ()} {l₃ : List ()} {l₄ : List ()} (nd₃ : l₃.NodupKeys) (p₁₂ : l₁.Perm l₂) (p₃₄ : l₃.Perm l₄) :
(l₁.kunion l₃).Perm (l₂.kunion l₄)
@[simp]
theorem List.dlookup_kunion_left {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} (h : a l₁.keys) :
List.dlookup a (l₁.kunion l₂) = List.dlookup a l₁
@[simp]
theorem List.dlookup_kunion_right {α : Type u} {β : αType v} [] {a : α} {l₁ : List ()} {l₂ : List ()} (h : al₁.keys) :
List.dlookup a (l₁.kunion l₂) = List.dlookup a l₂
theorem List.mem_dlookup_kunion {α : Type u} {β : αType v} [] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} :
b List.dlookup a (l₁.kunion l₂) b List.dlookup a l₁ al₁.keys b List.dlookup a l₂
@[simp]
theorem List.dlookup_kunion_eq_some {α : Type u} {β : αType v} [] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} :
List.dlookup a (l₁.kunion l₂) = some b List.dlookup a l₁ = some b al₁.keys List.dlookup a l₂ = some b
theorem List.mem_dlookup_kunion_middle {α : Type u} {β : αType v} [] {a : α} {b : β a} {l₁ : List ()} {l₂ : List ()} {l₃ : List ()} (h₁ : b List.dlookup a (l₁.kunion l₃)) (h₂ : al₂.keys) :
b List.dlookup a ((l₁.kunion l₂).kunion l₃)