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 #

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} :
List.keys [] = []
@[simp]
theorem List.keys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
List.keys (s :: l) = s.fst :: List.keys l
theorem List.mem_keys_of_mem {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} :
s ls.fst List.keys l
theorem List.exists_of_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} (h : a List.keys l) :
b, { fst := a, snd := b } l
theorem List.mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
a List.keys l b, { fst := a, snd := b } l
theorem List.not_mem_keys {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a List.keys l ∀ (b : β a), ¬{ fst := a, snd := b } l
theorem List.not_eq_key {α : Type u} {β : αType v} {a : α} {l : List (Sigma β)} :
¬a List.keys l ∀ (s : Sigma β), s la s.fst

NodupKeys #

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

Determines whether the store uses a key several times.

Equations
theorem List.nodupKeys_iff_pairwise {α : Type u} {β : αType v} {l : List (Sigma β)} :
List.NodupKeys l List.Pairwise (fun s s' => s.fst s'.fst) l
theorem List.NodupKeys.pairwise_ne {α : Type u} {β : αType v} {l : List (Sigma β)} (h : List.NodupKeys l) :
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 : Sigma β} {l : List (Sigma β)} :
theorem List.not_mem_keys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : List.NodupKeys (s :: l)) :
theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : αType v} {s : Sigma β} {l : List (Sigma β)} (h : List.NodupKeys (s :: l)) :
theorem List.NodupKeys.eq_of_fst_eq {α : Type u} {β : αType v} {l : List (Sigma β)} (nd : List.NodupKeys l) {s : Sigma β} {s' : Sigma β} (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 (Sigma β)} (nd : List.NodupKeys l) (h : { fst := a, snd := b } l) (h' : { fst := a, snd := b' } l) :
b = b'
theorem List.nodupKeys_singleton {α : Type u} {β : αType v} (s : Sigma β) :
theorem List.NodupKeys.sublist {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : List.Sublist l₁ l₂) :
theorem List.NodupKeys.nodup {α : Type u} {β : αType v} {l : List (Sigma β)} :
theorem List.perm_nodupKeys {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : l₁ ~ l₂) :
theorem List.nodupKeys_join {α : Type u} {β : αType v} {L : List (List (Sigma β))} :
List.NodupKeys (List.join L) (∀ (l : List (Sigma β)), l LList.NodupKeys l) List.Pairwise List.Disjoint (List.map List.keys L)
theorem List.nodup_enum_map_fst {α : Type u} (l : List α) :
theorem List.mem_ext {α : Type u} {β : αType v} {l₀ : List (Sigma β)} {l₁ : List (Sigma β)} (nd₀ : List.Nodup l₀) (nd₁ : List.Nodup l₁) (h : ∀ (x : Sigma β), x l₀ x l₁) :
l₀ ~ l₁

dlookup #

def List.dlookup {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) :
List (Sigma β)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 : DecidableEq α] (a : α) :
List.dlookup a [] = none
@[simp]
theorem List.dlookup_cons_eq {α : Type u} {β : αType v} [inst : DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
List.dlookup a ({ fst := a, snd := b } :: l) = some b
@[simp]
theorem List.dlookup_cons_ne {α : Type u} {β : αType v} [inst : DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
a s.fstList.dlookup a (s :: l) = List.dlookup a l
theorem List.dlookup_isSome {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} :
theorem List.dlookup_eq_none {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} :
theorem List.of_mem_dlookup {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
b List.dlookup a l{ fst := a, snd := b } l
theorem List.mem_dlookup {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : List.NodupKeys l) (h : { fst := a, snd := b } l) :
theorem List.map_dlookup_eq_find {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :
Option.map (Sigma.mk a) (List.dlookup a l) = List.find? (fun s => decide (a = s.fst)) l
theorem List.mem_dlookup_iff {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : List.NodupKeys l) :
b List.dlookup a l { fst := a, snd := b } l
theorem List.perm_dlookup {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : List.NodupKeys l₁) (nd₂ : List.NodupKeys l₂) (p : l₁ ~ l₂) :
theorem List.lookup_ext {α : Type u} {β : αType v} [inst : DecidableEq α] {l₀ : List (Sigma β)} {l₁ : List (Sigma β)} (nd₀ : List.NodupKeys l₀) (nd₁ : List.NodupKeys l₁) (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 : DecidableEq α] (a : α) :
List (Sigma β)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 : DecidableEq α] (a : α) :
@[simp]
theorem List.lookupAll_cons_eq {α : Type u} {β : αType v} [inst : DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) :
List.lookupAll a ({ fst := a, snd := b } :: l) = b :: List.lookupAll a l
@[simp]
theorem List.lookupAll_cons_ne {α : Type u} {β : αType v} [inst : DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) :
a s.fstList.lookupAll a (s :: l) = List.lookupAll a l
theorem List.lookupAll_eq_nil {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} :
List.lookupAll a l = [] ∀ (b : β a), ¬{ fst := a, snd := b } l
theorem List.head?_lookupAll {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.mem_lookupAll {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
b List.lookupAll a l { fst := a, snd := b } l
theorem List.lookupAll_sublist {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.lookupAll_length_le_one {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)} (h : List.NodupKeys l) :
theorem List.lookupAll_eq_dlookup {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)} (h : List.NodupKeys l) :
theorem List.lookupAll_nodup {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)} (h : List.NodupKeys l) :
theorem List.perm_lookupAll {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : List.NodupKeys l₁) (nd₂ : List.NodupKeys l₂) (p : l₁ ~ l₂) :

kreplace #

def List.kreplace {α : Type u} {β : αType v} [inst : DecidableEq α] (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} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ (b : β a), ¬{ fst := a, snd := b } l) :
theorem List.kreplace_self {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : List.NodupKeys l) (h : { fst := a, snd := b } l) :
theorem List.keys_kreplace {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) :
theorem List.kreplace_nodupKeys {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} :
theorem List.Perm.kreplace {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd : List.NodupKeys l₁) :
l₁ ~ l₂List.kreplace a b l₁ ~ List.kreplace a b l₂

kerase #

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

Remove the first pair with the key a.

Equations
theorem List.kerase_nil {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} :
List.kerase a [] = []
@[simp]
theorem List.kerase_cons_eq {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a = s.fst) :
List.kerase a (s :: l) = l
@[simp]
theorem List.kerase_cons_ne {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a s.fst) :
List.kerase a (s :: l) = s :: List.kerase a l
@[simp]
theorem List.kerase_of_not_mem_keys {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} (h : ¬a List.keys l) :
theorem List.kerase_sublist {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.kerase_keys_subset {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :
theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a₁ : α} {a₂ : α} {l : List (Sigma β)} :
a₁ List.keys (List.kerase a₂ l)a₁ List.keys l
theorem List.exists_of_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} (h : a List.keys l) :
b l₁ l₂, ¬a List.keys l₁ l = l₁ ++ { fst := a, snd := b } :: l₂ List.kerase a l = l₁ ++ l₂
@[simp]
theorem List.mem_keys_kerase_of_ne {α : Type u} {β : αType v} [inst : DecidableEq α] {a₁ : α} {a₂ : α} {l : List (Sigma β)} (h : a₁ a₂) :
a₁ List.keys (List.kerase a₂ l) a₁ List.keys l
theorem List.keys_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l : List (Sigma β)} :
theorem List.kerase_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {a' : α} {l : List (Sigma β)} :
theorem List.NodupKeys.kerase {α : Type u} {β : αType v} {l : List (Sigma β)} [inst : DecidableEq α] (a : α) :
theorem List.Perm.kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd : List.NodupKeys l₁) :
l₁ ~ l₂List.kerase a l₁ ~ List.kerase a l₂
@[simp]
theorem List.not_mem_keys_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)} (nd : List.NodupKeys l) :
@[simp]
theorem List.dlookup_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) {l : List (Sigma β)} (nd : List.NodupKeys l) :
@[simp]
theorem List.dlookup_kerase_ne {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {a' : α} {l : List (Sigma β)} (h : a a') :
theorem List.kerase_append_left {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
a List.keys l₁List.kerase a (l₁ ++ l₂) = List.kerase a l₁ ++ l₂
theorem List.kerase_append_right {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
¬a List.keys l₁List.kerase a (l₁ ++ l₂) = l₁ ++ List.kerase a l₂
theorem List.kerase_comm {α : Type u} {β : αType v} [inst : DecidableEq α] (a₁ : α) (a₂ : α) (l : List (Sigma β)) :
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 : DecidableEq α] [inst : SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) :

kinsert #

def List.kinsert {α : Type u} {β : αType v} [inst : DecidableEq α] (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} [inst : DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} :
List.kinsert a b l = { fst := a, snd := b } :: List.kerase a l
theorem List.mem_keys_kinsert {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {a' : α} {b' : β a'} {l : List (Sigma β)} :
theorem List.kinsert_nodupKeys {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (nd : List.NodupKeys l) :
theorem List.Perm.kinsert {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : List.NodupKeys l₁) (p : l₁ ~ l₂) :
List.kinsert a b l₁ ~ List.kinsert a b l₂
theorem List.dlookup_kinsert {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)) :
theorem List.dlookup_kinsert_ne {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {a' : α} {b' : β a'} {l : List (Sigma β)} (h : a a') :

kextract #

def List.kextract {α : Type u} {β : αType v} [inst : DecidableEq α] (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_dlookup_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] (a : α) (l : List (Sigma β)) :

dedupKeys #

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

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

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

kunion #

def List.kunion {α : Type u} {β : αType v} [inst : DecidableEq α] :
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} [inst : DecidableEq α] {l : List (Sigma β)} :
List.kunion [] l = l
@[simp]
theorem List.kunion_nil {α : Type u} {β : αType v} [inst : DecidableEq α] {l : List (Sigma β)} :
List.kunion l [] = l
@[simp]
theorem List.kunion_cons {α : Type u} {β : αType v} [inst : DecidableEq α] {s : Sigma β} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
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 : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
a List.keys (List.kunion l₁ l₂) a List.keys l₁ a List.keys l₂
@[simp]
theorem List.kunion_kerase {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
theorem List.NodupKeys.kunion {α : Type u} {β : αType v} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} [inst : DecidableEq α] (nd₁ : List.NodupKeys l₁) (nd₂ : List.NodupKeys l₂) :
theorem List.Perm.kunion_right {α : Type u} {β : αType v} [inst : DecidableEq α] {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (p : l₁ ~ l₂) (l : List (Sigma β)) :
List.kunion l₁ l ~ List.kunion l₂ l
theorem List.Perm.kunion_left {α : Type u} {β : αType v} [inst : DecidableEq α] (l : List (Sigma β)) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
List.NodupKeys l₁l₁ ~ l₂List.kunion l l₁ ~ List.kunion l l₂
theorem List.Perm.kunion {α : Type u} {β : αType v} [inst : DecidableEq α] {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} {l₃ : List (Sigma β)} {l₄ : List (Sigma β)} (nd₃ : List.NodupKeys l₃) (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 : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : a List.keys l₁) :
List.dlookup a (List.kunion l₁ l₂) = List.dlookup a l₁
@[simp]
theorem List.dlookup_kunion_right {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : ¬a List.keys l₁) :
List.dlookup a (List.kunion l₁ l₂) = List.dlookup a l₂
theorem List.mem_dlookup_kunion {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
@[simp]
theorem List.dlookup_kunion_eq_some {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} :
theorem List.mem_dlookup_kunion_middle {α : Type u} {β : αType v} [inst : DecidableEq α] {a : α} {b : β a} {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} {l₃ : List (Sigma β)} (h₁ : b List.dlookup a (List.kunion l₁ l₃)) (h₂ : ¬a List.keys l₂) :
b List.dlookup a (List.kunion (List.kunion l₁ l₂) l₃)