data.list.sigma

# Utilities for lists of sigmas #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

### keys#

def list.keys {α : Type u} {β : α Type v} :
list (sigma β) 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 : sigma β} {l : list (sigma β)} :
(s :: l).keys = s.fst :: l.keys
theorem list.mem_keys_of_mem {α : Type u} {β : α Type v} {s : sigma β} {l : list (sigma β)} :
s l s.fst l.keys
theorem list.exists_of_mem_keys {α : Type u} {β : α Type v} {a : α} {l : list (sigma β)} (h : a l.keys) :
(b : β a), a, b⟩ l
theorem list.mem_keys {α : Type u} {β : α Type v} {a : α} {l : list (sigma β)} :
a l.keys (b : β a), a, b⟩ l
theorem list.not_mem_keys {α : Type u} {β : α Type v} {a : α} {l : list (sigma β)} :
a l.keys (b : β a), a, b⟩ l
theorem list.not_eq_key {α : Type u} {β : α Type v} {a : α} {l : list (sigma β)} :
a l.keys (s : sigma β), s l a s.fst

### nodupkeys#

def list.nodupkeys {α : Type u} {β : α Type v} (l : list (sigma β)) :
Prop

Determines whether the store uses a key several times.

Equations
theorem list.nodupkeys_iff_pairwise {α : Type u} {β : α Type v} {l : list (sigma β)} :
l.nodupkeys list.pairwise (λ (s s' : sigma β), s.fst s'.fst) l
theorem list.nodupkeys.pairwise_ne {α : Type u} {β : α Type v} {l : list (sigma β)} (h : l.nodupkeys) :
list.pairwise (λ (s s' : sigma β), s.fst s'.fst) l
@[simp]
theorem list.nodupkeys_nil {α : Type u} {β : α Type v} :
@[simp]
theorem list.nodupkeys_cons {α : Type u} {β : α Type v} {s : sigma β} {l : list (sigma β)} :
theorem list.not_mem_keys_of_nodupkeys_cons {α : Type u} {β : α Type v} {s : sigma β} {l : list (sigma β)} (h : (s :: l).nodupkeys) :
theorem list.nodupkeys_of_nodupkeys_cons {α : Type u} {β : α Type v} {s : sigma β} {l : list (sigma β)} (h : (s :: l).nodupkeys) :
theorem list.nodupkeys.eq_of_fst_eq {α : Type u} {β : α Type v} {l : list (sigma β)} (nd : l.nodupkeys) {s s' : sigma β} (h : s l) (h' : s' l) :
s.fst = s'.fst s = s'
theorem list.nodupkeys.eq_of_mk_mem {α : Type u} {β : α Type v} {a : α} {b b' : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : a, b⟩ l) (h' : a, b'⟩ l) :
b = b'
theorem list.nodupkeys_singleton {α : Type u} {β : α Type v} (s : sigma β) :
theorem list.nodupkeys.sublist {α : Type u} {β : α Type v} {l₁ l₂ : list (sigma β)} (h : l₁ <+ l₂) :
@[protected]
theorem list.nodupkeys.nodup {α : Type u} {β : α Type v} {l : list (sigma β)} :
theorem list.perm_nodupkeys {α : Type u} {β : α Type v} {l₁ l₂ : list (sigma β)} (h : l₁ ~ l₂) :
theorem list.nodupkeys_join {α : Type u} {β : α Type v} {L : list (list (sigma β))} :
L.join.nodupkeys ( (l : list (sigma β)), l L l.nodupkeys)
theorem list.nodup_enum_map_fst {α : Type u} (l : list α) :
theorem list.mem_ext {α : Type u} {β : α Type v} {l₀ l₁ : list (sigma β)} (nd₀ : l₀.nodup) (nd₁ : l₁.nodup) (h : (x : sigma β), x l₀ x l₁) :
l₀ ~ l₁

### lookup#

def list.lookup {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
list (sigma β) option (β a)

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

Equations
@[simp]
theorem list.lookup_nil {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
@[simp]
theorem list.lookup_cons_eq {α : Type u} {β : α Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :
(a, b⟩ :: l) =
@[simp]
theorem list.lookup_cons_ne {α : Type u} {β : α Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :
a s.fst (s :: l) = l
theorem list.lookup_is_some {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
theorem list.lookup_eq_none {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
a l.keys
theorem list.of_mem_lookup {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b l a, b⟩ l
theorem list.mem_lookup {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : a, b⟩ l) :
b l
theorem list.map_lookup_eq_find {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
l) = list.find (λ (s : sigma β), a = s.fst) l
theorem list.mem_lookup_iff {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) :
b l a, b⟩ l
theorem list.perm_lookup {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) :
l₁ = l₂
theorem list.lookup_ext {α : Type u} {β : α Type v} [decidable_eq α] {l₀ l₁ : list (sigma β)} (nd₀ : l₀.nodupkeys) (nd₁ : l₁.nodupkeys) (h : (x : α) (y : β x), y l₀ y l₁) :
l₀ ~ l₁

### lookup_all#

def list.lookup_all {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
list (sigma β) list (β a)

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

Equations
• (a', b⟩ :: l) = dite (a' = a) (λ (h : a' = a), h.rec_on b :: l) (λ (h : ¬a' = a), l)
@[simp]
theorem list.lookup_all_nil {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
@[simp]
theorem list.lookup_all_cons_eq {α : Type u} {β : α Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :
(a, b⟩ :: l) = b ::
@[simp]
theorem list.lookup_all_cons_ne {α : Type u} {β : α Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :
a s.fst (s :: l) =
theorem list.lookup_all_eq_nil {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
(b : β a), a, b⟩ l
theorem list.head_lookup_all {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
theorem list.mem_lookup_all {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b a, b⟩ l
theorem list.lookup_all_sublist {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
theorem list.lookup_all_length_le_one {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
l).length 1
theorem list.lookup_all_eq_lookup {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
theorem list.lookup_all_nodup {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
l).nodup
theorem list.perm_lookup_all {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) :
l₁ = l₂

### kreplace#

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

Replaces the first value with key a by b.

Equations
theorem list.kreplace_of_forall_not {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} (H : (b : β a), a, b⟩ l) :
l = l
theorem list.kreplace_self {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : a, b⟩ l) :
l = l
theorem list.keys_kreplace {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) (l : list (sigma β)) :
b l).keys = l.keys
theorem list.kreplace_nodupkeys {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} :
theorem list.perm.kreplace {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} (nd : l₁.nodupkeys) :
l₁ ~ l₂ l₁ ~ l₂

### kerase#

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

Remove the first pair with the key a.

Equations
@[simp]
theorem list.kerase_nil {α : Type u} {β : α Type v} [decidable_eq α] {a : α} :
@[simp]
theorem list.kerase_cons_eq {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} (h : a = s.fst) :
(s :: l) = l
@[simp]
theorem list.kerase_cons_ne {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} (h : a s.fst) :
(s :: l) = s :: l
@[simp]
theorem list.kerase_of_not_mem_keys {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} (h : a l.keys) :
l = l
theorem list.kerase_sublist {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
l <+ l
theorem list.kerase_keys_subset {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
l).keys l.keys
theorem list.mem_keys_of_mem_keys_kerase {α : Type u} {β : α Type v} [decidable_eq α] {a₁ a₂ : α} {l : list (sigma β)} :
a₁ (list.kerase a₂ l).keys a₁ l.keys
theorem list.exists_of_kerase {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} (h : a l.keys) :
(b : β a) (l₁ l₂ : list (sigma β)), a l₁.keys l = l₁ ++ a, b⟩ :: l₂ l = l₁ ++ l₂
@[simp]
theorem list.mem_keys_kerase_of_ne {α : Type u} {β : α Type v} [decidable_eq α] {a₁ a₂ : α} {l : list (sigma β)} (h : a₁ a₂) :
a₁ (list.kerase a₂ l).keys a₁ l.keys
theorem list.keys_kerase {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
l).keys = l.keys.erase a
theorem list.kerase_kerase {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} :
(list.kerase a' l) = l)
theorem list.nodupkeys.kerase {α : Type u} {β : α Type v} {l : list (sigma β)} [decidable_eq α] (a : α) :
theorem list.perm.kerase {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (nd : l₁.nodupkeys) :
l₁ ~ l₂ l₁ ~ l₂
@[simp]
theorem list.not_mem_keys_kerase {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (nd : l.nodupkeys) :
a l).keys
@[simp]
theorem list.lookup_kerase {α : Type u} {β : α Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (nd : l.nodupkeys) :
@[simp]
theorem list.lookup_kerase_ne {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} (h : a a') :
(list.kerase a' l) = l
theorem list.kerase_append_left {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keys (l₁ ++ l₂) = l₁ ++ l₂
theorem list.kerase_append_right {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a l₁.keys (l₁ ++ l₂) = l₁ ++ l₂
theorem list.kerase_comm {α : Type u} {β : α Type v} [decidable_eq α] (a₁ a₂ : α) (l : list (sigma β)) :
(list.kerase a₁ l) = (list.kerase a₂ l)
theorem list.sizeof_kerase {α : Type u_1} {β : α Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (x : α) (xs : list (sigma β)) :

### kinsert#

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

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

Equations
@[simp]
theorem list.kinsert_def {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b l = a, b⟩ :: l
theorem list.mem_keys_kinsert {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b' : β a'} {l : list (sigma β)} :
a (list.kinsert a' b' l).keys a = a' a l.keys
theorem list.kinsert_nodupkeys {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} (nd : l.nodupkeys) :
b l).nodupkeys
theorem list.perm.kinsert {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (p : l₁ ~ l₂) :
b l₁ ~ b l₂
theorem list.lookup_kinsert {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} (l : list (sigma β)) :
b l) =
theorem list.lookup_kinsert_ne {α : Type u} {β : α Type v} [decidable_eq α] {a a' : α} {b' : β a'} {l : list (sigma β)} (h : a a') :
(list.kinsert a' b' l) = l

### kextract#

def list.kextract {α : Type u} {β : α Type v} [decidable_eq α] (a : α) :
list (sigma β) option (β a) × list (sigma β)

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_lookup_kerase {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
= l, l)

### dedupkeys#

def list.dedupkeys {α : Type u} {β : α Type v} [decidable_eq α] :
list (sigma β) list (sigma β)

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

Equations
theorem list.dedupkeys_cons {α : Type u} {β : α Type v} [decidable_eq α] {x : sigma β} (l : list (sigma β)) :
theorem list.nodupkeys_dedupkeys {α : Type u} {β : α Type v} [decidable_eq α] (l : list (sigma β)) :
theorem list.lookup_dedupkeys {α : Type u} {β : α Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
= l
theorem list.sizeof_dedupkeys {α : Type u_1} {β : α Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (xs : list (sigma β)) :

### kunion#

def list.kunion {α : Type u} {β : α Type v} [decidable_eq α] :
list (sigma β) list (sigma β) list (sigma β)

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} [decidable_eq α] {l : list (sigma β)} :
= l
@[simp]
theorem list.kunion_nil {α : Type u} {β : α Type v} [decidable_eq α] {l : list (sigma β)} :
= l
@[simp]
theorem list.kunion_cons {α : Type u} {β : α Type v} [decidable_eq α] {s : sigma β} {l₁ l₂ : list (sigma β)} :
(s :: l₁).kunion l₂ = s :: l₁.kunion l₂)
@[simp]
theorem list.mem_keys_kunion {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a (l₁.kunion l₂).keys a l₁.keys a l₂.keys
@[simp]
theorem list.kunion_kerase {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
l₁).kunion l₂) = (l₁.kunion l₂)
theorem list.nodupkeys.kunion {α : Type u} {β : α Type v} {l₁ l₂ : list (sigma β)} [decidable_eq α] (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) :
(l₁.kunion l₂).nodupkeys
theorem list.perm.kunion_right {α : Type u} {β : α Type v} [decidable_eq α] {l₁ l₂ : list (sigma β)} (p : l₁ ~ l₂) (l : list (sigma β)) :
l₁.kunion l ~ l₂.kunion l
theorem list.perm.kunion_left {α : Type u} {β : α Type v} [decidable_eq α] (l : list (sigma β)) {l₁ l₂ : list (sigma β)} :
l₁.nodupkeys l₁ ~ l₂ l.kunion l₁ ~ l.kunion l₂
theorem list.perm.kunion {α : Type u} {β : α Type v} [decidable_eq α] {l₁ l₂ l₃ l₄ : list (sigma β)} (nd₃ : l₃.nodupkeys) (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) :
l₁.kunion l₃ ~ l₂.kunion l₄
@[simp]
theorem list.lookup_kunion_left {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (h : a l₁.keys) :
(l₁.kunion l₂) = l₁
@[simp]
theorem list.lookup_kunion_right {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (h : a l₁.keys) :
(l₁.kunion l₂) = l₂
@[simp]
theorem list.mem_lookup_kunion {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} :
b (l₁.kunion l₂) b l₁ a l₁.keys b l₂
theorem list.mem_lookup_kunion_middle {α : Type u} {β : α Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ l₃ : list (sigma β)} (h₁ : b (l₁.kunion l₃)) (h₂ : a l₂.keys) :
b ((l₁.kunion l₂).kunion l₃)