lookup a l is the first value in l corresponding to the key a,
or none if no such element exists.
Equations
- list.lookup a (⟨a', b⟩ :: l) = dite (a' = a) (λ (h : a' = a), option.some (h.rec_on b)) (λ (h : ¬a' = a), list.lookup a l)
- list.lookup a list.nil = option.none
@[simp]
@[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) = option.some b
@[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
theorem
list.lookup_is_some
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l : list (sigma β)} :
theorem
list.lookup_eq_none
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l : list (sigma β)} :
list.lookup a l = option.none ↔ a ∉ l.keys
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
theorem
list.mem_lookup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l : list (sigma β)} :
l.nodupkeys → ⟨a, b⟩ ∈ l → b ∈ list.lookup a l
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
theorem
list.mem_lookup_iff
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l : list (sigma β)} :
theorem
list.perm_lookup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l₁ l₂ : list (sigma β)} :
l₁.nodupkeys → l₂.nodupkeys → l₁ ~ l₂ → list.lookup a l₁ = list.lookup a l₂
theorem
list.lookup_ext
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{l₀ l₁ : list (sigma β)} :
l₀.nodupkeys → l₁.nodupkeys → (∀ (x : α) (y : β x), y ∈ list.lookup x l₀ ↔ y ∈ list.lookup x l₁) → l₀ ~ l₁
lookup_all a l is the list of all values in l corresponding to the key a.
Equations
- list.lookup_all a (⟨a', b⟩ :: l) = dite (a' = a) (λ (h : a' = a), h.rec_on b :: list.lookup_all a l) (λ (h : ¬a' = a), list.lookup_all a l)
- list.lookup_all a list.nil = list.nil
@[simp]
@[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
@[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
theorem
list.lookup_all_eq_nil
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l : list (sigma β)} :
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
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
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
theorem
list.lookup_all_length_le_one
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → (list.lookup_all a l).length ≤ 1
theorem
list.lookup_all_eq_lookup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → list.lookup_all a l = (list.lookup a l).to_list
theorem
list.lookup_all_nodup
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → (list.lookup_all a l).nodup
theorem
list.perm_lookup_all
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l₁ l₂ : list (sigma β)} :
l₁.nodupkeys → l₂.nodupkeys → l₁ ~ l₂ → list.lookup_all a l₁ = list.lookup_all a l₂
Equations
- list.kreplace a b = list.lookmap (λ (s : sigma β), dite (a = s.fst) (λ (h : a = s.fst), option.some ⟨a, b⟩) (λ (h : ¬a = s.fst), option.none))
theorem
list.kreplace_of_forall_not
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
{l : list (sigma β)} :
(∀ (b : β a), ⟨a, b⟩ ∉ l) → list.kreplace a b l = l
theorem
list.kreplace_self
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l : list (sigma β)} :
l.nodupkeys → ⟨a, b⟩ ∈ l → list.kreplace a b l = l
theorem
list.keys_kreplace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
(l : list (sigma β)) :
(list.kreplace a b l).keys = l.keys
theorem
list.kreplace_nodupkeys
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
{l : list (sigma β)} :
(list.kreplace a b l).nodupkeys ↔ l.nodupkeys
theorem
list.perm.kreplace
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l₁ l₂ : list (sigma β)} :
l₁.nodupkeys → l₁ ~ l₂ → list.kreplace a b l₁ ~ list.kreplace a b l₂
Remove the first pair with the key a.
Equations
- list.kerase a = list.erasep (λ (s : sigma β), a = s.fst)
@[simp]
@[simp]
theorem
list.kerase_cons_eq
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : sigma β}
{l : list (sigma β)} :
a = s.fst → list.kerase a (s :: l) = l
@[simp]
theorem
list.kerase_cons_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{s : sigma β}
{l : list (sigma β)} :
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}
[decidable_eq α]
{a : α}
{l : list (sigma β)} :
a ∉ l.keys → list.kerase a l = l
theorem
list.kerase_sublist
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(l : list (sigma β)) :
list.kerase a l <+ l
theorem
list.kerase_keys_subset
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(l : list (sigma β)) :
(list.kerase a l).keys ⊆ l.keys
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
@[simp]
theorem
list.mem_keys_kerase_of_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a₁ a₂ : α}
{l : list (sigma β)} :
theorem
list.keys_kerase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l : list (sigma β)} :
(list.kerase a l).keys = l.keys.erase a
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)
theorem
list.kerase_nodupkeys
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → (list.kerase a l).nodupkeys
theorem
list.perm.kerase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l₁ l₂ : list (sigma β)} :
l₁.nodupkeys → l₁ ~ l₂ → list.kerase a l₁ ~ list.kerase a l₂
@[simp]
theorem
list.not_mem_keys_kerase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → a ∉ (list.kerase a l).keys
@[simp]
theorem
list.lookup_kerase
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
{l : list (sigma β)} :
l.nodupkeys → list.lookup a (list.kerase a l) = option.none
@[simp]
theorem
list.lookup_kerase_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{l : list (sigma β)} :
a ≠ a' → list.lookup a (list.kerase a' l) = list.lookup a l
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₂
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₂
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)
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}
[decidable_eq α]
{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}
[decidable_eq α]
{a a' : α}
{b' : β a'}
{l : list (sigma β)} :
theorem
list.kinsert_nodupkeys
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(a : α)
(b : β a)
{l : list (sigma β)} :
l.nodupkeys → (list.kinsert a b l).nodupkeys
theorem
list.perm.kinsert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l₁ l₂ : list (sigma β)} :
l₁.nodupkeys → l₁ ~ l₂ → list.kinsert a b l₁ ~ list.kinsert a b l₂
theorem
list.lookup_kinsert
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
(l : list (sigma β)) :
list.lookup a (list.kinsert a b l) = option.some b
theorem
list.lookup_kinsert_ne
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a a' : α}
{b' : β a'}
{l : list (sigma β)} :
a ≠ a' → list.lookup a (list.kinsert a' b' l) = list.lookup a l
Equations
- list.kextract a (s :: l) = dite (s.fst = a) (λ (h : s.fst = a), (option.some (h.rec_on s.snd), l)) (λ (h : ¬s.fst = a), list.kextract._match_1 a s (list.kextract a l))
- list.kextract a list.nil = (option.none (β a), list.nil (sigma β))
- list.kextract._match_1 a s (b', l') = (b', s :: l')
@[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)
Remove entries with duplicate keys from l : list (sigma β).
Equations
- list.erase_dupkeys = list.foldr (λ (x : sigma β), list.kinsert x.fst x.snd) list.nil
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
theorem
list.nodupkeys_erase_dupkeys
{α : Type u}
{β : α → Type v}
[decidable_eq α]
(l : list (sigma β)) :
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
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]
@[simp]
@[simp]
theorem
list.kunion_cons
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{s : sigma β}
{l₁ l₂ : list (sigma β)} :
@[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₂)
theorem
list.kunion_nodupkeys
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{l₁ l₂ : list (sigma β)} :
@[simp]
theorem
list.lookup_kunion_left
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l₁ l₂ : list (sigma β)} :
a ∈ l₁.keys → list.lookup a (l₁.kunion l₂) = list.lookup a l₁
@[simp]
theorem
list.lookup_kunion_right
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{l₁ l₂ : list (sigma β)} :
a ∉ l₁.keys → list.lookup a (l₁.kunion l₂) = list.lookup a l₂
@[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₂
theorem
list.mem_lookup_kunion_middle
{α : Type u}
{β : α → Type v}
[decidable_eq α]
{a : α}
{b : β a}
{l₁ l₂ l₃ : list (sigma β)} :
b ∈ list.lookup a (l₁.kunion l₃) → a ∉ l₂.keys → b ∈ list.lookup a ((l₁.kunion l₂).kunion l₃)