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

• 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

ink

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

theorem List.mem_keys {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)} : a ∈ List.keys l ↔ ∃ b, { fst := a, snd := b } ∈ l

ink

theorem List.not_mem_keys {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)} : ¬a ∈ List.keys l ↔ ∀ (b : β a), ¬{ fst := a, snd := b } ∈ l

ink

theorem List.not_eq_key {α : Type u} {β : α → Type v} {a : α} {l : List (Sigma β)} : ¬a ∈ List.keys l ↔ ∀ (s : Sigma β), s ∈ l → a ≠ s.fst

NodupKeys

ink

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

Determines whether the store uses a key several times.

Equations

• List.NodupKeys l = List.Nodup (List.keys l)

ink

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

ink

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

ink

@[simp]

theorem List.nodupKeys_nil {α : Type u} {β : α → Type v} : List.NodupKeys []

ink

@[simp]

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

ink

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

ink

theorem List.nodupKeys_of_nodupKeys_cons {α : Type u} {β : α → Type v} {s : Sigma β} {l : List (Sigma β)} (h : List.NodupKeys (s :: l)) : List.NodupKeys l

ink

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'.fst → s = s'

ink

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'

ink

theorem List.nodupKeys_singleton {α : Type u} {β : α → Type v} (s : Sigma β) : List.NodupKeys [s]

ink

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

ink

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

ink

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

ink

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

ink

theorem List.nodup_enum_map_fst {α : Type u} (l : List α) : List.Nodup (List.map Prod.fst (List.enum l))

ink

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

ink

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

• List.dlookup a [] = none
• List.dlookup a ({ fst := a', snd := b } :: l) = if h : a' = a then some (Eq.recOn h b) else List.dlookup a l

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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) : b ∈ List.dlookup a l

ink

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

ink

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

ink

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₂) : List.dlookup a l₁ = List.dlookup a l₂

ink

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

ink

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

• List.lookupAll a [] = []
• List.lookupAll a ({ fst := a', snd := b } :: l) = if h : a' = a then Eq.recOn h b :: List.lookupAll a l else List.lookupAll a l

ink

@[simp]

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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

ink

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₂) : List.lookupAll a l₁ = List.lookupAll a l₂

kreplace

ink

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

• List.kreplace a b = List.lookmap fun s => if a = s.fst then some { fst := a, snd := b } else none

ink

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) : List.kreplace a b l = l

ink

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) : List.kreplace a b l = l

ink

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

ink

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

ink

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

ink

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

Remove the first pair with the key a.

Equations

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

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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

ink

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₂

ink

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

ink

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

ink

theorem List.kerase_kerase {α : 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)

ink

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

ink

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₂

ink

@[simp]

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

ink

@[simp]

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

ink

@[simp]

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

ink

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₂

ink

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₂

ink

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)

ink

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

kinsert

ink

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

• List.kinsert a b l = { fst := a, snd := b } :: List.kerase a l

ink

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

ink

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

ink

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

ink

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₂

ink

theorem List.dlookup_kinsert {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} (l : List (Sigma β)) : List.dlookup a (List.kinsert a b l) = some b

ink

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

kextract

ink

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

• 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')

ink

@[simp]

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

dedupKeys

ink

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

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

Equations

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

ink

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

ink

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

ink

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

ink

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

kunion

ink

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

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

ink

@[simp]

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

ink

@[simp]

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

ink

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

ink

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

ink

@[simp]

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

ink

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

ink

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

ink

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₂

ink

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₄

ink

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

ink

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

ink

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

ink

@[simp]

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

ink

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₃)