English
If we insert a key k with value v into an AList, then for any key k' the lookup of k' equals none exactly when k' ≠ k and the previous lookup is none.
Русский
Если вставить пару ключ-значение (k,v) в AList, то для любого k' поиск возвращает none тогда и только тогда, когда k' ≠ k и прежний поиск по k' равен none.
LaTeX
$$$\operatorname{AList.lookup k'}(\operatorname{AList.insert k v} l) = \mathrm{none} \iff (k' \neq k) \wedge \operatorname{AList.lookup k' } l = \mathrm{none}$$$
Lean4
@[simp]
theorem lookup_insert_eq_none {l : AList β} {k k' : α} {v : β k} :
(l.insert k v).lookup k' = none ↔ (k' ≠ k) ∧ l.lookup k' = none :=
by
by_cases h : k' = k
· subst h; simp
· simp_all [lookup_insert_ne h]
