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

Equations

• List.keys = List.map Sigma.fst

@[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

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 ∈ 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

• l.NodupKeys = l.keys.Nodup

theorem List.nodupKeys_iff_pairwise {α : Type u} {β : α → Type v} {l : List (Sigma β)} : l.NodupKeys ↔ List.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) : List.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.not_mem_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 : Sigma β} {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 : β a} {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₁ : List (Sigma β)} {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₁ : List (Sigma β)} {l₂ : List (Sigma β)} (h : l₁.Perm l₂) : l₁.NodupKeys ↔ l₂.NodupKeys

theorem List.nodupKeys_join {α : Type u} {β : α → Type v} {L : List (List (Sigma β))} : L.join.NodupKeys ↔ (∀ l ∈ L, 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 (Sigma β)} {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.

Equations

• List.dlookup a [] = none
• List.dlookup a (⟨a', b⟩ :: l) = if h : a' = a then some (Eq.recOn h b) else List.dlookup a l

@[simp]

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

@[simp]

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

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

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

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

theorem List.map_dlookup_eq_find {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : Option.map (Sigma.mk a) (List.dlookup a l) = List.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 ∈ List.dlookup a l ↔ ⟨a, b⟩ ∈ l

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

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

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

Equations

• List.lookupAll a [] = []
• List.lookupAll a (⟨a', b⟩ :: l) = if h : a' = a then Eq.recOn h b :: List.lookupAll a l else List.lookupAll a l

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

theorem List.perm_lookupAll {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) {l₁ : List (Sigma β)} {l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (nd₂ : l₂.NodupKeys) (p : l₁.Perm l₂) : List.lookupAll a l₁ = List.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.

Equations

• List.kreplace a b = List.lookmap fun (s : Sigma β) => if a = s.fst then some ⟨a, b⟩ else none

theorem List.kreplace_of_forall_not {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (H : ∀ (b : β a), ⟨a, b⟩ ∉ l) : List.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) : List.kreplace a b l = l

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

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

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

Equations

• List.kerase a = List.eraseP fun (s : Sigma β) => decide (a = s.fst)

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

@[simp]

theorem List.kerase_cons_eq {α : Type u} {β : α → Type v} [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} [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} [DecidableEq α] {a : α} {l : List (Sigma β)} (h : a ∉ l.keys) : List.kerase a l = l

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

theorem List.kerase_keys_subset {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : (List.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₁ ∈ (List.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₂ ∧ List.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₁ ∈ (List.kerase a₂ l).keys ↔ a₁ ∈ l.keys

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

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

@[simp]

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

@[simp]

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

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

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

theorem List.kerase_comm {α : Type u} {β : α → Type v} [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} {β : α → Type v} [DecidableEq α] [SizeOf (Sigma β)] (x : α) (xs : List (Sigma β)) : sizeOf (List.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.

Equations

• List.kinsert a b l = ⟨a, b⟩ :: List.kerase a l

@[simp]

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

theorem List.mem_keys_kinsert {α : Type u} {β : α → Type v} [DecidableEq α] {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} [DecidableEq α] (a : α) (b : β a) {l : List (Sigma β)} (nd : l.NodupKeys) : (List.kinsert a b l).NodupKeys

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

Equations

• List.kextract a [] = (none, [])
• List.kextract a (s :: l) = if h : s.fst = a then (some (Eq.recOn h s.snd), l) else match List.kextract a l with | (b', l') => (b', s :: l')

@[simp]

theorem List.kextract_eq_dlookup_kerase {α : Type u} {β : α → Type v} [DecidableEq α] (a : α) (l : List (Sigma β)) : List.kextract a l = (List.dlookup a l, List.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 β).

Equations

• List.dedupKeys = List.foldr (fun (x : Sigma β) => List.kinsert x.fst x.snd) []

theorem List.dedupKeys_cons {α : Type u} {β : α → Type v} [DecidableEq α] {x : Sigma β} (l : List (Sigma β)) : (x :: l).dedupKeys = List.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 β)) : List.dlookup a l.dedupKeys = List.dlookup a l

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.

Equations

• [].kunion x = x
• (s :: l₁).kunion x = s :: l₁.kunion (List.kerase s.fst x)

@[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₁ : List (Sigma β)} {l₂ : List (Sigma β)} : (s :: l₁).kunion l₂ = s :: l₁.kunion (List.kerase s.fst l₂)

@[simp]

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

@[simp]

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

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

@[simp]

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

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