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 (Sigma β) → List α

List of keys from a list of key-value pairs

@[simp]

theorem List.keys_nil {α : Type u} {β : α → Type v} : [].keys = []

@[simp]

theorem List.keys_cons {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)} : (s :: l).keys = s.fst :: l.keys

@[simp]

theorem List.keys_append {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} : (l₁ ++ l₂).keys = l₁.keys ++ 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.notMem_keys {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)} : ¬a ∈ l.keys ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ l

theorem List.ne_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.

theorem List.nodupKeys_iff_pairwise {α : Type u} {β : α → Type v} {l : List (Sigma β)} : l.NodupKeys ↔ Pairwise (fun (s s' : Sigma β) => s.fst ≠ s'.fst) l

theorem List.NodupKeys.pairwise_ne {α : Type u} {β : α → Type v} {l : List (Sigma β)} (h : l.NodupKeys) : Pairwise (fun (s s' : Sigma β) => 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 : Sigma β} {l : List (Sigma β)} : (s :: l).NodupKeys ↔ ¬s.fst ∈ l.keys ∧ l.NodupKeys

theorem List.nodupKeys_middle {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} {s : Sigma β} : (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys

theorem List.notMem_keys_of_nodupKeys_cons {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) : ¬s.fst ∈ l.keys

theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)} (h : (s :: l).NodupKeys) : 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 β) : [s].NodupKeys

theorem List.NodupKeys.sublist {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} (h : l₁.Sublist l₂) : l₂.NodupKeys → l₁.NodupKeys

theorem List.NodupKeys.nodup {α : Type u} {β : α → Type v} {l : List (Sigma β)} : l.NodupKeys → l.Nodup

theorem List.perm_nodupKeys {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} (h : l₁.Perm l₂) : l₁.NodupKeys ↔ l₂.NodupKeys

theorem List.nodupKeys_flatten {α : Type u} {β : α → Type v} {L : List (List (Sigma β))} : L.flatten.NodupKeys ↔ (∀ (l : List (Sigma β)), l ∈ L → l.NodupKeys) ∧ Pairwise Disjoint (map keys L)

theorem List.nodup_zipIdx_map_snd {α : Type u} (l : List α) : (map Prod.snd l.zipIdx).Nodup

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₀.Perm l₁

dlookup

def List.dlookup {α : Type u} {β : α → Type v} [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.

@[simp]

theorem List.dlookup_nil {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : dlookup a [] = none

@[simp]

theorem List.dlookup_cons_eq {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) : dlookup a (⟨a, b⟩ :: l) = some b

@[simp]

theorem List.dlookup_cons_ne {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) : a ≠ s.fst → dlookup a (s :: l) = dlookup a l

theorem List.dlookup_isSome {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} : (dlookup a l).isSome = true ↔ a ∈ l.keys

theorem List.dlookup_eq_none {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} : dlookup a l = none ↔ ¬a ∈ l.keys

theorem List.of_mem_dlookup {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} : b ∈ dlookup a l → ⟨a, b⟩ ∈ l

theorem List.mem_dlookup {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : ⟨a, b⟩ ∈ l) : b ∈ dlookup a l

theorem List.map_dlookup_eq_find {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : Option.map (Sigma.mk a) (dlookup a l) = find? (fun (s : Sigma β) => decide (a = s.fst)) l

theorem List.mem_dlookup_iff {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) : b ∈ dlookup a l ↔ ⟨a, b⟩ ∈ l

theorem List.perm_dlookup {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁.Perm l₂) : dlookup a l₁ = dlookup a l₂

theorem List.lookup_ext {α : Type u} {β : α → Type v} [DecidableEq α] {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys) (h : ∀ (x : α) (y : β x), y ∈ dlookup x l₀ ↔ y ∈ dlookup x l₁) : l₀.Perm l₁

theorem List.dlookup_map {α : Type u} {α' : Type u'} {β : α → Type v} {β' : α' → Type v'} [DecidableEq α] [DecidableEq α'] (l : List (Sigma β)) {f : α → α'} (hf : Function.Injective f) (g : (a : α) → β a → β' (f a)) (a : α) : dlookup (f a) (map (Sigma.map f g) l) = Option.map (g a) (dlookup a l)

theorem List.dlookup_map₁ {α : Type u} {α' : Type u'} [DecidableEq α] [DecidableEq α'] {β : Type v} (l : List ((_ : α) × β)) {f : α → α'} (hf : Function.Injective f) (a : α) : dlookup (f a) (map (Sigma.map f fun (x : α) => id) l) = dlookup a l

theorem List.dlookup_map₂ {α : Type u} [DecidableEq α] {γ : α → Type u_1} {δ : α → Type u_2} {l : List ((a : α) × γ a)} {f : (a : α) → γ a → δ a} (a : α) : dlookup a (map (Sigma.map id f) l) = Option.map (f a) (dlookup a l)

theorem List.NodupKeys.map₁ {α : Type u} {α' : Type u'} {β : Type v} (f : α → α') (hf : Function.Injective f) {l : List ((_ : α) × β)} (nd : l.NodupKeys) : (map (Sigma.map f fun (x : α) => id) l).NodupKeys

theorem List.map₂_keys {α : Type u} {β : α → Type u_1} {β' : α → Type u_2} (f : (a : α) → β a → β' a) (l : List ((a : α) × β a)) : (map (Sigma.map id f) l).keys = l.keys

theorem List.NodupKeys.map₂ {α : Type u} {β : α → Type u_1} {β' : α → Type u_2} (f : (a : α) → β a → β' a) (l : List ((a : α) × β a)) (nd : l.NodupKeys) : (map (Sigma.map id f) l).NodupKeys

@[simp]

theorem List.dlookup_append {α : Type u} {β : α → Type v} [DecidableEq α] (l₁ l₂ : List (Sigma β)) (a : α) : dlookup a (l₁ ++ l₂) = (dlookup a l₁).or (dlookup a l₂)

theorem List.sublist_dlookup {α : Type u} {β : α → Type v} [DecidableEq α] {l₁ l₂ : List (Sigma β)} {a : α} {b : β a} (nd₂ : l₂.NodupKeys) (s : l₁.Sublist l₂) (mem : b ∈ dlookup a l₁) : b ∈ dlookup a l₂

lookupAll

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

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

@[simp]

theorem List.lookupAll_nil {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) : lookupAll a [] = []

@[simp]

theorem List.lookupAll_cons_eq {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) (a : α) (b : β a) : lookupAll a (⟨a, b⟩ :: l) = b :: lookupAll a l

@[simp]

theorem List.lookupAll_cons_ne {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) {a : α} (s : Sigma β) : a ≠ s.fst → lookupAll a (s :: l) = lookupAll a l

theorem List.lookupAll_eq_nil {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} : lookupAll a l = [] ↔ ∀ (b : β a), ¬⟨a, b⟩ ∈ l

theorem List.head?_lookupAll {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : (lookupAll a l).head? = dlookup a l

theorem List.mem_lookupAll {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} : b ∈ lookupAll a l ↔ ⟨a, b⟩ ∈ l

theorem List.lookupAll_sublist {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : (map (Sigma.mk a) (lookupAll a l)).Sublist l

theorem List.lookupAll_length_le_one {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : (lookupAll a l).length ≤ 1

theorem List.lookupAll_eq_dlookup {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : lookupAll a l = (dlookup a l).toList

theorem List.lookupAll_nodup {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : (lookupAll a l).Nodup

theorem List.perm_lookupAll {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁.Perm l₂) : lookupAll a l₁ = lookupAll a l₂

kreplace

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

Replaces the first value with key a by b.

theorem List.kreplace_of_forall_not {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ (b : β a), ¬⟨a, b⟩ ∈ l) : kreplace a b l = l

theorem List.kreplace_self {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} (nd : l.NodupKeys) (h : ⟨a, b⟩ ∈ l) : kreplace a b l = l

theorem List.keys_kreplace {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) (l : List (Sigma β)) : (kreplace a b l).keys = l.keys

theorem List.kreplace_nodupKeys {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} : (kreplace a b l).NodupKeys ↔ l.NodupKeys

theorem List.Perm.kreplace {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (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} [DecidableEq α] (a : α) : List (Sigma β) → List (Sigma β)

Remove the first pair with the key a.

@[simp]

theorem List.kerase_nil {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} : kerase a [] = []

@[simp]

theorem List.kerase_cons_eq {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a = s.fst) : kerase a (s :: l) = l

@[simp]

theorem List.kerase_cons_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {s : Sigma β} {l : List (Sigma β)} (h : a ≠ s.fst) : kerase a (s :: l) = s :: kerase a l

@[simp]

theorem List.kerase_of_notMem_keys {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : ¬a ∈ l.keys) : kerase a l = l

theorem List.kerase_sublist {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : (kerase a l).Sublist l

theorem List.kerase_keys_subset {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : (kerase a l).keys ⊆ l.keys

theorem List.mem_keys_of_mem_keys_kerase {α : Type u} {β : α → Type v} [DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)} : a₁ ∈ (kerase a₂ l).keys → a₁ ∈ l.keys

theorem List.exists_of_kerase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : a ∈ l.keys) : ∃ (b : β a), ∃ (l₁ : List (Sigma β)), ∃ (l₂ : List (Sigma β)), ¬a ∈ l₁.keys ∧ l = l₁ ++ ⟨a, b⟩ :: l₂ ∧ kerase a l = l₁ ++ l₂

@[simp]

theorem List.mem_keys_kerase_of_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)} (h : a₁ ≠ a₂) : a₁ ∈ (kerase a₂ l).keys ↔ a₁ ∈ l.keys

theorem List.keys_kerase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l : List (Sigma β)} : (kerase a l).keys = l.keys.erase a

theorem List.kerase_kerase {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {l : List (Sigma β)} : kerase a (kerase a' l) = kerase a' (kerase a l)

theorem List.NodupKeys.kerase {α : Type u} {β : α → Type v} {l : List (Sigma β)} [DecidableEq α] (a : α) : l.NodupKeys → (List.kerase a l).NodupKeys

theorem List.Perm.kerase {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (nd : l₁.NodupKeys) : l₁.Perm l₂ → (List.kerase a l₁).Perm (List.kerase a l₂)

@[simp]

theorem List.notMem_keys_kerase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) : ¬a ∈ (kerase a l).keys

@[simp]

theorem List.dlookup_kerase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l : List (Sigma β)} (nd : l.NodupKeys) : dlookup a (kerase a l) = none

@[simp]

theorem List.dlookup_kerase_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {l : List (Sigma β)} (h : a ≠ a') : dlookup a (kerase a' l) = dlookup a l

theorem List.kerase_append_left {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} : a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂

theorem List.kerase_append_right {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} : ¬a ∈ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂

theorem List.kerase_comm {α : Type u} {β : α → Type v} [DecidableEq α] (a₁ a₂ : α) (l : List (Sigma β)) : kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)

theorem List.sizeOf_kerase {α : Type u} {β : α → Type v} [DecidableEq α] [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) : sizeOf (kerase x xs) ≤ sizeOf xs

kinsert

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

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

@[simp]

theorem List.kinsert_def {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l : List (Sigma β)} : kinsert a b l = ⟨a, b⟩ :: kerase a l

theorem List.mem_keys_kinsert {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)} : a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys

theorem List.kinsert_nodupKeys {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (nd : l.NodupKeys) : (kinsert a b l).NodupKeys

theorem List.Perm.kinsert {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} (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} [DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)) : dlookup a (kinsert a b l) = some b

theorem List.dlookup_kinsert_ne {α : Type u} {β : α → Type v} [DecidableEq α] {a a' : α} {b' : β a'} {l : List (Sigma β)} (h : a ≠ a') : dlookup a (kinsert a' b' l) = dlookup a l

kextract

def List.kextract {α : Type u} {β : α → Type v} [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.

@[simp]

theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : kextract a l = (dlookup a l, kerase a l)

dedupKeys

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

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

theorem List.dedupKeys_cons {α : Type u} {β : α → Type v} [DecidableEq α] {x : Sigma β} (l : List (Sigma β)) : (x :: l).dedupKeys = kinsert x.fst x.snd l.dedupKeys

theorem List.nodupKeys_dedupKeys {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) : l.dedupKeys.NodupKeys

theorem List.dlookup_dedupKeys {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : dlookup a l.dedupKeys = dlookup a l

theorem List.sizeOf_cons_le_sizeOf_cons {α : Type u_1} [SizeOf α] {l r : List α} (a : α) (h : sizeOf l ≤ sizeOf r) : sizeOf (a :: l) ≤ sizeOf (a :: r)

theorem List.sizeOf_dedupKeys {α : Type u} {β : α → Type v} [DecidableEq α] [SizeOf (Sigma β)] (xs : List (Sigma β)) : sizeOf xs.dedupKeys ≤ sizeOf xs

kunion

def List.kunion {α : Type u} {β : α → Type v} [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.

@[simp]

theorem List.nil_kunion {α : Type u} {β : α → Type v} [DecidableEq α] {l : List (Sigma β)} : [].kunion l = l

@[simp]

theorem List.kunion_nil {α : Type u} {β : α → Type v} [DecidableEq α] {l : List (Sigma β)} : l.kunion [] = l

@[simp]

theorem List.kunion_cons {α : Type u} {β : α → Type v} [DecidableEq α] {s : Sigma β} {l₁ l₂ : List (Sigma β)} : (s :: l₁).kunion l₂ = s :: l₁.kunion (kerase s.fst l₂)

@[simp]

theorem List.mem_keys_kunion {α : Type u} {β : α → Type v} [DecidableEq α] {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} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} : (kerase a l₁).kunion (kerase a l₂) = kerase a (l₁.kunion l₂)

theorem List.NodupKeys.kunion {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)} [DecidableEq α] (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) : (l₁.kunion l₂).NodupKeys

theorem List.Perm.kunion_right {α : Type u} {β : α → Type v} [DecidableEq α] {l₁ l₂ : List (Sigma β)} (p : l₁.Perm l₂) (l : List (Sigma β)) : (l₁.kunion l).Perm (l₂.kunion l)

theorem List.Perm.kunion_left {α : Type u} {β : α → Type v} [DecidableEq α] (l : List (Sigma β)) {l₁ l₂ : List (Sigma β)} : l₁.NodupKeys → l₁.Perm l₂ → (l.kunion l₁).Perm (l.kunion l₂)

theorem List.Perm.kunion {α : Type u} {β : α → Type v} [DecidableEq α] {l₁ l₂ l₃ l₄ : List (Sigma β)} (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} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (h : a ∈ l₁.keys) : dlookup a (l₁.kunion l₂) = dlookup a l₁

@[simp]

theorem List.dlookup_kunion_right {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {l₁ l₂ : List (Sigma β)} (h : ¬a ∈ l₁.keys) : dlookup a (l₁.kunion l₂) = dlookup a l₂

theorem List.mem_dlookup_kunion {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} : b ∈ dlookup a (l₁.kunion l₂) ↔ b ∈ dlookup a l₁ ∨ ¬a ∈ l₁.keys ∧ b ∈ dlookup a l₂

@[simp]

theorem List.dlookup_kunion_eq_some {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ : List (Sigma β)} : dlookup a (l₁.kunion l₂) = some b ↔ dlookup a l₁ = some b ∨ ¬a ∈ l₁.keys ∧ dlookup a l₂ = some b

theorem List.mem_dlookup_kunion_middle {α : Type u} {β : α → Type v} [DecidableEq α] {a : α} {b : β a} {l₁ l₂ l₃ : List (Sigma β)} (h₁ : b ∈ dlookup a (l₁.kunion l₃)) (h₂ : ¬a ∈ l₂.keys) : b ∈ dlookup a ((l₁.kunion l₂).kunion l₃)