mathlib documentation

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*, 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 #

source
def list.keys {α : Type u} {β : α → Type v} :
list (sigma β) → list α

List of keys from a list of key-value pairs

Equations
source
@[simp]
theorem list.keys_nil {α : Type u} {β : α → Type v} :
list.nil.keys = list.nil
source
@[simp]
theorem list.keys_cons {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
(s :: l).keys = s.fst :: l.keys
source
theorem list.mem_keys_of_mem {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
s ∈ l → s.fst ∈ l.keys
source
theorem list.exists_of_mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} (h : a ∈ l.keys) :
∃ (b : β a), ⟨a, b⟩ ∈ l
source
theorem list.mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a ∈ l.keys ↔ ∃ (b : β a), ⟨a, b⟩ ∈ l
source
theorem list.not_mem_keys {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a ∉ l.keys ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
source
theorem list.not_eq_key {α : Type u} {β : α → Type v} {a : α} {l : list (sigma β)} :
a ∉ l.keys ↔ ∀ (s : sigma β), s ∈ l → a ≠ s.fst

nodupkeys #

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

Determines whether the store uses a key several times.

Equations
source
theorem list.nodupkeys_iff_pairwise {α : Type u} {β : α → Type v} {l : list (sigma β)} :
l.nodupkeys ↔ list.pairwise (λ (s s' : sigma β), s.fst ≠ s'.fst) l
source
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
source
@[simp]
theorem list.nodupkeys_nil {α : Type u} {β : α → Type v} :
list.nil.nodupkeys
source
@[simp]
theorem list.nodupkeys_cons {α : Type u} {β : α → Type v} {s : sigma β} {l : list (sigma β)} :
(s :: l).nodupkeys ↔ s.fst ∉ l.keys ∧ l.nodupkeys
source
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'
source
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'
source
theorem list.nodupkeys_singleton {α : Type u} {β : α → Type v} (s : sigma β) :
[s].nodupkeys
source
theorem list.nodupkeys_of_sublist {α : Type u} {β : α → Type v} {l₁ l₂ : list (sigma β)} (h : l₁ <+ l₂) :
l₂.nodupkeys → l₁.nodupkeys
source
theorem list.nodup_of_nodupkeys {α : Type u} {β : α → Type v} {l : list (sigma β)} :
l.nodupkeys → l.nodup
source
theorem list.perm_nodupkeys {α : Type u} {β : α → Type v} {l₁ l₂ : list (sigma β)} (h : l₁ ~ l₂) :
l₁.nodupkeys ↔ l₂.nodupkeys
source
theorem list.nodupkeys_join {α : Type u} {β : α → Type v} {L : list (list (sigma β))} :
L.join.nodupkeys ↔ (∀ (l : list (sigma β)), l ∈ L → l.nodupkeys) ∧ list.pairwise list.disjoint (list.map list.keys L)
source
theorem list.nodup_enum_map_fst {α : Type u} (l : list α) :
(list.map prod.fst l.enum).nodup
source
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 #

source
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
source
@[simp]
theorem list.lookup_nil {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list.lookup a list.nil = none
source
@[simp]
theorem list.lookup_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :
list.lookup a (⟨a, b⟩ :: l) = some b
source
@[simp]
theorem list.lookup_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :
a ≠ s.fst → list.lookup a (s :: l) = list.lookup a l
source
theorem list.lookup_is_some {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
↥((list.lookup a l).is_some) ↔ a ∈ l.keys
source
theorem list.lookup_eq_none {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
list.lookup a l = none ↔ a ∉ l.keys
source
theorem list.of_mem_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b ∈ list.lookup a l → ⟨a, b⟩ ∈ l
source
theorem list.mem_lookup {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : ⟨a, b⟩ ∈ l) :
b ∈ list.lookup a l
source
theorem list.map_lookup_eq_find {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
option.map (sigma.mk a) (list.lookup a l) = list.find (λ (s : sigma β), a = s.fst) l
source
theorem list.mem_lookup_iff {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) :
b ∈ list.lookup a l ↔ ⟨a, b⟩ ∈ l
source
theorem list.perm_lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) :
list.lookup a l₁ = list.lookup a l₂
source
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 ∈ list.lookup x l₀ ↔ y ∈ list.lookup x l₁) :
l₀ ~ l₁

lookup_all #

source
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
source
@[simp]
theorem list.lookup_all_nil {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) :
list.lookup_all a list.nil = list.nil
source
@[simp]
theorem list.lookup_all_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (Σ (a : α), β a)) (a : α) (b : β a) :
list.lookup_all a (⟨a, b⟩ :: l) = b :: list.lookup_all a l
source
@[simp]
theorem list.lookup_all_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) {a : α} (s : sigma β) :
a ≠ s.fst → list.lookup_all a (s :: l) = list.lookup_all a l
source
theorem list.lookup_all_eq_nil {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
list.lookup_all a l = list.nil ↔ ∀ (b : β a), ⟨a, b⟩ ∉ l
source
theorem list.head_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
(list.lookup_all a l).head' = list.lookup a l
source
theorem list.mem_lookup_all {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
b ∈ list.lookup_all a l ↔ ⟨a, b⟩ ∈ l
source
theorem list.lookup_all_sublist {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
list.map (sigma.mk a) (list.lookup_all a l) <+ l
source
theorem list.lookup_all_length_le_one {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
(list.lookup_all a l).length ≤ 1
source
theorem list.lookup_all_eq_lookup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
list.lookup_all a l = (list.lookup a l).to_list
source
theorem list.lookup_all_nodup {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
(list.lookup_all a l).nodup
source
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₂) :
list.lookup_all a l₁ = list.lookup_all a l₂

kreplace #

source
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
source
theorem list.kreplace_of_forall_not {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} (H : ∀ (b : β a), ⟨a, b⟩ ∉ l) :
list.kreplace a b l = l
source
theorem list.kreplace_self {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) (h : ⟨a, b⟩ ∈ l) :
list.kreplace a b l = l
source
theorem list.keys_kreplace {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) (l : list (sigma β)) :
(list.kreplace a b l).keys = l.keys
source
theorem list.kreplace_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} :
(list.kreplace a b l).nodupkeys ↔ l.nodupkeys
source
theorem list.perm.kreplace {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} (nd : l₁.nodupkeys) :
l₁ ~ l₂ → list.kreplace a b l₁ ~ list.kreplace a b l₂

kerase #

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

Remove the first pair with the key a.

Equations
source
@[simp]
theorem list.kerase_nil {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} :
list.kerase a list.nil = list.nil
source
@[simp]
theorem list.kerase_cons_eq {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} (h : a = s.fst) :
list.kerase a (s :: l) = l
source
@[simp]
theorem list.kerase_cons_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {s : sigma β} {l : list (sigma β)} (h : a ≠ s.fst) :
list.kerase a (s :: l) = s :: list.kerase a l
source
@[simp]
theorem list.kerase_of_not_mem_keys {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} (h : a ∉ l.keys) :
list.kerase a l = l
source
theorem list.kerase_sublist {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
list.kerase a l <+ l
source
theorem list.kerase_keys_subset {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
(list.kerase a l).keys ⊆ l.keys
source
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
source
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₂ ∧ list.kerase a l = l₁ ++ l₂
source
@[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
source
theorem list.keys_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l : list (sigma β)} :
(list.kerase a l).keys = l.keys.erase a
source
theorem list.kerase_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} :
list.kerase a (list.kerase a' l) = list.kerase a' (list.kerase a l)
source
theorem list.kerase_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} :
l.nodupkeys → (list.kerase a l).nodupkeys
source
theorem list.perm.kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (nd : l₁.nodupkeys) :
l₁ ~ l₂ → list.kerase a l₁ ~ list.kerase a l₂
source
@[simp]
theorem list.not_mem_keys_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (nd : l.nodupkeys) :
a ∉ (list.kerase a l).keys
source
@[simp]
theorem list.lookup_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) {l : list (sigma β)} (nd : l.nodupkeys) :
list.lookup a (list.kerase a l) = none
source
@[simp]
theorem list.lookup_kerase_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {l : list (sigma β)} (h : a ≠ a') :
list.lookup a (list.kerase a' l) = list.lookup a l
source
theorem list.kerase_append_left {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a ∈ l₁.keys → list.kerase a (l₁ ++ l₂) = list.kerase a l₁ ++ l₂
source
theorem list.kerase_append_right {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
a ∉ l₁.keys → list.kerase a (l₁ ++ l₂) = l₁ ++ list.kerase a l₂
source
theorem list.kerase_comm {α : Type u} {β : α → Type v} [decidable_eq α] (a₁ a₂ : α) (l : list (sigma β)) :
list.kerase a₂ (list.kerase a₁ l) = list.kerase a₁ (list.kerase a₂ l)
source
theorem list.sizeof_kerase {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (x : α) (xs : list (sigma β)) :
sizeof (list.kerase x xs) ≤ sizeof xs

kinsert #

source
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
source
@[simp]
theorem list.kinsert_def {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l : list (sigma β)} :
list.kinsert a b l = ⟨a, b⟩ :: list.kerase a l
source
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
source
theorem list.kinsert_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (b : β a) {l : list (sigma β)} (nd : l.nodupkeys) :
(list.kinsert a b l).nodupkeys
source
theorem list.perm.kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (p : l₁ ~ l₂) :
list.kinsert a b l₁ ~ list.kinsert a b l₂
source
theorem list.lookup_kinsert {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} (l : list (sigma β)) :
list.lookup a (list.kinsert a b l) = some b
source
theorem list.lookup_kinsert_ne {α : Type u} {β : α → Type v} [decidable_eq α] {a a' : α} {b' : β a'} {l : list (sigma β)} (h : a ≠ a') :
list.lookup a (list.kinsert a' b' l) = list.lookup a l

kextract #

source
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
source
@[simp]
theorem list.kextract_eq_lookup_kerase {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
list.kextract a l = (list.lookup a l, list.kerase a l)

erase_dupkeys #

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

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

Equations
source
theorem list.erase_dupkeys_cons {α : Type u} {β : α → Type v} [decidable_eq α] {x : sigma β} (l : list (sigma β)) :
(x :: l).erase_dupkeys = list.kinsert x.fst x.snd l.erase_dupkeys
source
theorem list.nodupkeys_erase_dupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (l : list (sigma β)) :
l.erase_dupkeys.nodupkeys
source
theorem list.lookup_erase_dupkeys {α : Type u} {β : α → Type v} [decidable_eq α] (a : α) (l : list (sigma β)) :
list.lookup a l.erase_dupkeys = list.lookup a l
source
theorem list.sizeof_erase_dupkeys {α : Type u_1} {β : α → Type u_2} [decidable_eq α] [has_sizeof (sigma β)] (xs : list (sigma β)) :
sizeof xs.erase_dupkeys ≤ sizeof xs

kunion #

source
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
source
@[simp]
theorem list.nil_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {l : list (sigma β)} :
list.nil.kunion l = l
source
@[simp]
theorem list.kunion_nil {α : Type u} {β : α → Type v} [decidable_eq α] {l : list (sigma β)} :
l.kunion list.nil = l
source
@[simp]
theorem list.kunion_cons {α : Type u} {β : α → Type v} [decidable_eq α] {s : sigma β} {l₁ l₂ : list (sigma β)} :
(s :: l₁).kunion l₂ = s :: l₁.kunion (list.kerase s.fst l₂)
source
@[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
source
@[simp]
theorem list.kunion_kerase {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
(list.kerase a l₁).kunion (list.kerase a l₂) = list.kerase a (l₁.kunion l₂)
source
theorem list.kunion_nodupkeys {α : Type u} {β : α → Type v} [decidable_eq α] {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) :
(l₁.kunion l₂).nodupkeys
source
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
source
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₂
source
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₄
source
@[simp]
theorem list.lookup_kunion_left {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (h : a ∈ l₁.keys) :
list.lookup a (l₁.kunion l₂) = list.lookup a l₁
source
@[simp]
theorem list.lookup_kunion_right {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} (h : a ∉ l₁.keys) :
list.lookup a (l₁.kunion l₂) = list.lookup a l₂
source
@[simp]
theorem list.mem_lookup_kunion {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ : list (sigma β)} :
b ∈ list.lookup a (l₁.kunion l₂) ↔ b ∈ list.lookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ list.lookup a l₂
source
theorem list.mem_lookup_kunion_middle {α : Type u} {β : α → Type v} [decidable_eq α] {a : α} {b : β a} {l₁ l₂ l₃ : list (sigma β)} (h₁ : b ∈ list.lookup a (l₁.kunion l₃)) (h₂ : a ∉ l₂.keys) :
b ∈ list.lookup a ((l₁.kunion l₂).kunion l₃)