max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: tree map lemmas for insertMany (#7331)

Browse source 
This PR provides lemmas about the tree map function `insertMany` and its
interaction with other functions for which lemmas already exist. Most
lemmas about `ofList`, which is related to `insertMany`, are not
included.

---------

Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert 2025-03-06 09:54:42 +01:00 • committed by GitHub
parent ca0d822619
commit 0c898742f6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
11 changed files with 3380 additions and 94 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/Std/Classes/Ord.lean
View file

@ -295,6 +295,11 @@ class LawfulBEqCmp {α : Type u} [BEq α] (cmp : α → α → Ordering) : Prop
/-- If two values compare equal, then they are logically equal. -/
compare_eq_iff_beq {a b : α} : cmp a b = .eq ↔ a == b
theorem LawfulBEqCmp.not_compare_eq_iff_beq_eq_false {α : Type u} [BEq α] {cmp}
[LawfulBEqCmp (α := α) cmp] {a b : α} : ¬ cmp a b = .eq ↔ (a == b) = false := by
rw [Bool.eq_false_iff, ne_eq, not_congr]
exact compare_eq_iff_beq
/--
A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if
the boolean equality `a == b` holds.
@ -306,6 +311,16 @@ abbrev LawfulBEqOrd (α : Type u) [BEq α] [Ord α] := LawfulBEqCmp (compare :
variable {α : Type u} [BEq α] {cmp : α → α → Ordering}
theorem LawfulBEqOrd.compare_eq_iff_beq {α : Type u} {_ : Ord α} {_ : BEq α}
[LawfulBEqOrd α] {a b : α} : compare a b = .eq ↔ (a == b) = true :=
LawfulBEqCmp.compare_eq_iff_beq
theorem LawfulBEqOrd.not_compare_eq_iff_beq_eq_false {α : Type u} {_ : BEq α} {_ : Ord α}
[LawfulBEqOrd α] {a b : α} : ¬ compare a b = .eq ↔ (a == b) = false :=
LawfulBEqCmp.not_compare_eq_iff_beq_eq_false
export LawfulBEqOrd (compare_eq_iff_beq not_compare_eq_iff_beq_eq_false)
instance [LawfulEqCmp cmp] [LawfulBEq α] :
LawfulBEqCmp cmp where
compare_eq_iff_beq := compare_eq_iff_eq.trans beq_iff_eq.symm
@ -322,6 +337,20 @@ theorem LawfulBEqCmp.equivBEq [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBE
instance LawfulBEqOrd.equivBEq [Ord α] [LawfulBEqOrd α] [TransOrd α] : EquivBEq α :=
LawfulBEqCmp.equivBEq (cmp := compare)
theorem LawfulBEqCmp.lawfulBEq [inst : LawfulBEqCmp cmp] [LawfulEqCmp cmp] : LawfulBEq α where
rfl := by simp [← inst.compare_eq_iff_beq, compare_eq_iff_eq]
eq_of_beq := by simp [← inst.compare_eq_iff_beq, compare_eq_iff_eq]
instance LawfulBEqOrd.lawfulBEq [Ord α] [LawfulBEqOrd α] [LawfulEqOrd α] : LawfulBEq α :=
LawfulBEqCmp.lawfulBEq (cmp := compare)
instance LawfulBEqCmp.lawfulBEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : LawfulEqCmp cmp where
compare_self := by simp only [compare_eq_iff_beq, beq_self_eq_true, implies_true]
eq_of_compare := by simp only [compare_eq_iff_beq, beq_iff_eq, imp_self, implies_true]
theorem LawfulBEqOrd.lawfulBEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α :=
LawfulBEqCmp.lawfulBEqCmp
end LawfulBEq
namespace Internal
@ -336,6 +365,9 @@ verification machinery for tree maps to the verification machinery for hash maps
def beqOfOrd [Ord α] : BEq α where
beq a b := compare a b == .eq
instance {_ : Ord α} : LawfulBEqOrd α where
compare_eq_iff_beq {a b} := by simp only [beqOfOrd, beq_iff_eq]
@[local simp]
theorem beq_eq [Ord α] {a b : α} : (a == b) = (compare a b == .eq) :=
rfl

1145
src/Std/Data/DTreeMap/Internal/Lemmas.lean
View file

File diff suppressed because it is too large Load diff

169
src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean
View file

@ -342,9 +342,10 @@ theorem exists_cell_of_updateAtKey [Ord α] [TransOrd α] (l : Impl α β) (hlb
beq_eq_false_iff_ne, ne_eq]
rintro a (⟨p, ⟨⟨-, hp⟩, rfl⟩⟩|⟨p, ⟨⟨-, hp⟩, rfl⟩⟩) <;> simp_all
theorem Ordered.distinctKeys [Ord α] {l : Impl α β} (h : l.Ordered) :
theorem Ordered.distinctKeys [BEq α] [Ord α] [LawfulBEqOrd α] {l : Impl α β} (h : l.Ordered) :
DistinctKeys l.toListModel :=
⟨by rw [keys_eq_map, List.pairwise_map]; exact h.imp (fun h => by simp_all)⟩
⟨by rw [keys_eq_map, List.pairwise_map]; exact h.imp (fun h => by
simp [← LawfulBEqOrd.not_compare_eq_iff_beq_eq_false, h])⟩
/-- This is the general theorem to show that modification operations are correct. -/
theorem toListModel_updateAtKey_perm [Ord α] [TransOrd α]
@ -541,8 +542,10 @@ theorem containsₘ_eq_containsKey [Ord α] [TransOrd α] {k : α} {l : Impl α
· exact fun l₁ l₂ h a hP => containsKey_of_perm hP
· exact fun l₁ l₂ h h' => containsKey_append_of_not_contains_right h'
theorem contains_eq_containsKey [Ord α] [TransOrd α] {k : α} {l : Impl α β} (hlo : l.Ordered) :
theorem contains_eq_containsKey [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α}
{l : Impl α β} (hlo : l.Ordered) :
l.contains k = containsKey k l.toListModel := by
rw [eq_beqOfOrd_of_lawfulBEqOrd instBEq]
rw [contains_eq_containsₘ, containsₘ_eq_containsKey hlo]
/-!
@ -560,8 +563,10 @@ theorem get?ₘ_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α
· exact fun l₁ l₂ h => getValueCast?_of_perm
· exact fun l₁ l₂ h => getValueCast?_append_of_containsKey_eq_false
theorem get?_eq_getValueCast? [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β}
theorem get?_eq_getValueCast? [instBEq : BEq α] [Ord α] [i : LawfulBEqOrd α] [TransOrd α]
[LawfulEqOrd α] {k : α} {t : Impl α β}
(hto : t.Ordered) : t.get? k = getValueCast? k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get?_eq_get?ₘ, get?ₘ_eq_getValueCast? hto]
/-!
@ -579,8 +584,9 @@ theorem getₘ_eq_getValueCast [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
rw [get?ₘ_eq_getValueCast? hto]
simp [getValueCast?_eq_some_getValueCast ‹_›]
theorem get_eq_getValueCast [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h}
theorem get_eq_getValueCast [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} {t : Impl α β} {h}
(hto : t.Ordered): t.get k h = getValueCast k t.toListModel (contains_eq_containsKey hto ▸ h) := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get_eq_getₘ, getₘ_eq_getValueCast _ hto]
exact contains_eq_isSome_get?ₘ hto ▸ h
@ -592,8 +598,9 @@ theorem get!ₘ_eq_getValueCast! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α
{t : Impl α β} (hto : t.Ordered) : t.get!ₘ k = getValueCast! k t.toListModel := by
simp [get!ₘ, get?ₘ_eq_getValueCast? hto, getValueCast!_eq_getValueCast?]
theorem get!_eq_getValueCast! [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
theorem get!_eq_getValueCast! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α} [Inhabited (β k)]
{t : Impl α β} (hto : t.Ordered) : t.get! k = getValueCast! k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get!_eq_get!ₘ, get!ₘ_eq_getValueCast! hto]
/-!
@ -605,9 +612,10 @@ theorem getDₘ_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α
t.getDₘ k fallback = getValueCastD k t.toListModel fallback := by
simp [getDₘ, get?ₘ_eq_getValueCast? hto, getValueCastD_eq_getValueCast?]
theorem getD_eq_getValueCastD [Ord α] [TransOrd α] [LawfulEqOrd α] {k : α}
theorem getD_eq_getValueCastD [Ord α] [instBEq : BEq α] [LawfulBEqOrd α] [TransOrd α] [LawfulEqOrd α] {k : α}
{t : Impl α β} {fallback : β k} (hto : t.Ordered) :
t.getD k fallback = getValueCastD k t.toListModel fallback := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getD_eq_getDₘ, getDₘ_eq_getValueCastD hto]
/-!
@ -625,8 +633,9 @@ theorem getKey?ₘ_eq_getKey? [Ord α] [TransOrd α] {k : α} {t : Impl α β}
· exact fun l₁ l₂ h => List.getKey?_of_perm
· exact fun l₁ l₂ h => List.getKey?_append_of_containsKey_eq_false
theorem getKey?_eq_getKey? [Ord α] [TransOrd α] {k : α} {t : Impl α β}
theorem getKey?_eq_getKey? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β}
(hto : t.Ordered) : t.getKey? k = List.getKey? k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getKey?_eq_getKey?ₘ, getKey?ₘ_eq_getKey? hto]
/-!
@ -644,8 +653,9 @@ theorem getKeyₘ_eq_getKey [Ord α] [TransOrd α] {k : α} {t : Impl α β} (h)
rw [getKey?ₘ_eq_getKey? hto]
simp [getKey?_eq_some_getKey ‹_›]
theorem getKey_eq_getKey [Ord α] [TransOrd α] {k : α} {t : Impl α β} {h}
theorem getKey_eq_getKey [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h}
(hto : t.Ordered): t.getKey k h = List.getKey k t.toListModel (contains_eq_containsKey hto ▸ h) := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getKey_eq_getKeyₘ, getKeyₘ_eq_getKey _ hto]
exact contains_eq_isSome_getKey?ₘ hto ▸ h
@ -657,8 +667,9 @@ theorem getKey!ₘ_eq_getKey! [Ord α] [TransOrd α] {k : α} [Inhabited α]
{t : Impl α β} (hto : t.Ordered) : t.getKey!ₘ k = List.getKey! k t.toListModel := by
simp [getKey!ₘ, getKey?ₘ_eq_getKey? hto, getKey!_eq_getKey?]
theorem getKey!_eq_getKey! [Ord α] [TransOrd α] {k : α} [Inhabited α]
theorem getKey!_eq_getKey! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited α]
{t : Impl α β} (hto : t.Ordered) : t.getKey! k = List.getKey! k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getKey!_eq_getKey!ₘ, getKey!ₘ_eq_getKey! hto]
/-!
@ -670,9 +681,10 @@ theorem getKeyDₘ_eq_getKeyD [Ord α] [TransOrd α] {k : α}
t.getKeyDₘ k fallback = List.getKeyD k t.toListModel fallback := by
simp [getKeyDₘ, getKey?ₘ_eq_getKey? hto, getKeyD_eq_getKey?]
theorem getKeyD_eq_getKeyD [Ord α] [TransOrd α] {k : α}
theorem getKeyD_eq_getKeyD [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
{t : Impl α β} {fallback : α} (hto : t.Ordered) :
t.getKeyD k fallback = List.getKeyD k t.toListModel fallback := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getKeyD_eq_getKeyDₘ, getKeyDₘ_eq_getKeyD hto]
namespace Const
@ -694,8 +706,9 @@ theorem get?ₘ_eq_getValue? [Ord α] [TransOrd α] {k : α} {t : Impl α (fun _
· exact fun l₁ l₂ h => getValue?_of_perm
· exact fun l₁ l₂ h => getValue?_append_of_containsKey_eq_false
theorem get?_eq_getValue? [Ord α] [TransOrd α] {k : α} {t : Impl α (fun _ => β)} (hto : t.Ordered) :
theorem get?_eq_getValue? [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α (fun _ => β)} (hto : t.Ordered) :
get? t k = getValue? k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get?_eq_get?ₘ, get?ₘ_eq_getValue? hto]
/-!
@ -713,8 +726,9 @@ theorem getₘ_eq_getValue [Ord α] [TransOrd α] {k : α} {t : Impl α β} (h)
rw [get?ₘ_eq_getValue? hto]
simp [getValue?_eq_some_getValue ‹_›]
theorem get_eq_getValue [Ord α] [TransOrd α] {k : α} {t : Impl α β} {h}
theorem get_eq_getValue [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} {t : Impl α β} {h}
(hto : t.Ordered): get t k h = getValue k t.toListModel (contains_eq_containsKey hto ▸ h) := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get_eq_getₘ, getₘ_eq_getValue _ hto]
exact contains_eq_isSome_get?ₘ hto ▸ h
@ -726,8 +740,9 @@ theorem get!ₘ_eq_getValue! [Ord α] [TransOrd α] {k : α} [Inhabited β]
{t : Impl α β} (hto : t.Ordered) : get!ₘ t k = getValue! k t.toListModel := by
simp [get!ₘ, get?ₘ_eq_getValue? hto, getValue!_eq_getValue?]
theorem get!_eq_getValue! [Ord α] [TransOrd α] {k : α} [Inhabited β]
theorem get!_eq_getValue! [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α} [Inhabited β]
{t : Impl α β} (hto : t.Ordered) : get! t k = getValue! k t.toListModel := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [get!_eq_get!ₘ, get!ₘ_eq_getValue! hto]
/-!
@ -739,9 +754,10 @@ theorem getDₘ_eq_getValueD [Ord α] [TransOrd α] {k : α}
getDₘ t k fallback = getValueD k t.toListModel fallback := by
simp [getDₘ, get?ₘ_eq_getValue? hto, getValueD_eq_getValue?]
theorem getD_eq_getValueD [Ord α] [TransOrd α] {k : α}
theorem getD_eq_getValueD [Ord α] [TransOrd α] [instBEq : BEq α] [LawfulBEqOrd α] {k : α}
{t : Impl α β} {fallback : β} (hto : t.Ordered) :
getD t k fallback = getValueD k t.toListModel fallback := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
rw [getD_eq_getDₘ, getDₘ_eq_getValueD hto]
end Const
@ -801,10 +817,10 @@ theorem WF.insert! {_ : Ord α} [TransOrd α] {k : α} {v : β k} {l : Impl α
(h : l.WF) : (l.insert! k v).WF := by
simpa [insert_eq_insert!] using WF.insert (h := h.balanced) h
theorem toListModel_insert! [Ord α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
theorem toListModel_insert! [instBEq : BEq α] [Ord α] [LawfulBEqOrd α] [TransOrd α] {k : α} {v : β k} {l : Impl α β}
(hlb : l.Balanced) (hlo : l.Ordered) :
(l.insert! k v).toListModel.Perm (insertEntry k v l.toListModel) := by
rw [insert!_eq_insertₘ]
rw [insert!_eq_insertₘ, eq_beqOfOrd_of_lawfulBEqOrd instBEq]
exact toListModel_insertₘ hlb hlo
/-!
@ -995,7 +1011,7 @@ theorem filter_eq_filterMap [Ord α] {t : Impl α β} {h} {f : (a : α) → β a
t.filter f h = t.filterMap (fun k v => if f k v then some v else none) h := by
induction t with
| leaf => rfl
| inner sz k v l r ihl ihr =>
| inner sz k v l r ihl ihr =>
simp [filter, filterMap]
cases hf : f k v <;> rw [ihl, ihr] <;> rfl
@ -1104,7 +1120,7 @@ theorem ordered_mergeWith [Ord α] [TransOrd α] [LawfulEqOrd α] {t₁ t₂ : I
(t₁.mergeWith f t₂ htb).impl.Ordered := by
induction t₂ generalizing t₁ with
| leaf => exact hto
| inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto))
| inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto))
/-!
### foldlM
@ -1348,7 +1364,7 @@ theorem ordered_mergeWith [Ord α] [TransOrd α] {t₁ t₂ : Impl α β} {f}
(mergeWith f t₁ t₂ htb).impl.Ordered := by
induction t₂ generalizing t₁ with
| leaf => exact hto
| inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto))
| inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto))
/-!
### toList
@ -1467,9 +1483,39 @@ theorem WF.eraseMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ}
(t.eraseMany! l).2 h (fun _ _ h' => h'.erase!)
/-!
### `insertMany!`
### `insertMany`
-/
theorem insertMany!_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} :
(t.insertMany! l).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by
simp [insertMany!, Id.run, ← List.foldl_hom Subtype.val]
theorem insertMany_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) :
(t.insertMany l h).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by
simp [insertMany, Id.run, insert_eq_insert!, ← List.foldl_hom Subtype.val]
theorem insertMany_eq_insertMany! {_ : Ord α} {l : List ((a : α) × β a)}
{t : Impl α β} (h : t.Balanced) :
(t.insertMany l h).val = (t.insertMany! l).val := by
simp only [insertMany_eq_foldl, insertMany!_eq_foldl]
theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{l : List ((a : α) × β a)}
{t : Impl α β} (h : t.WF) :
List.Perm (t.insertMany l h.balanced).val.toListModel (t.toListModel.insertList l) := by
simp only [insertMany_eq_foldl]
induction l generalizing t with
| nil => rfl
| cons e es ih =>
refine (ih h.insert!).trans ?_
exact insertList_perm_of_perm_first (toListModel_insert! h.balanced h.ordered)
h.insert!.ordered.distinctKeys
theorem toListModel_insertMany!_list {_ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} {t : Impl α β} (h : t.WF) :
List.Perm (t.insertMany! l).val.toListModel (t.toListModel.insertList l) := by
simpa only [← insertMany_eq_insertMany! h.balanced] using toListModel_insertMany_list h
theorem WF.insertMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ ((a : α) × β a)] {l : ρ}
{t : Impl α β} (h : t.WF) : (t.insertMany! l).1.WF :=
(t.insertMany! l).2 h (fun _ _ _ h' => h'.insert!)
@ -1482,6 +1528,87 @@ theorem WF.constInsertManyIfNewUnit! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id
{t : Impl α Unit} (h : t.WF) : (Const.insertManyIfNewUnit! t l).1.WF :=
(Const.insertManyIfNewUnit! t l).2 h (fun _ _ h' => h'.insertIfNew!)
namespace Const
variable {β : Type v}
/-!
### `insertMany`
-/
theorem insertMany!_eq_foldl {_ : Ord α} {l : List (α × β)} {t : Impl α β} :
(insertMany! t l).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by
simp only [insertMany!, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
rw [← List.foldl_hom Subtype.val]
simp only [implies_true]
theorem insertMany_eq_foldl {_ : Ord α} {l : List (α × β)}
{t : Impl α β} (h : t.Balanced) :
(Const.insertMany t l h).val = l.foldl (init := t) fun acc ⟨k, v⟩ => acc.insert! k v := by
simp only [insertMany, Id.run, Id.pure_eq, insert_eq_insert!, Id.bind_eq,
List.forIn_yield_eq_foldl]
rw [← List.foldl_hom Subtype.val]
simp only [implies_true]
theorem insertMany_eq_insertMany! {_ : Ord α} {l : List (α × β)}
{t : Impl α β} (h : t.Balanced) :
(Const.insertMany t l h).val = (Const.insertMany! t l).val := by
simp only [insertMany!_eq_foldl, insertMany_eq_foldl]
theorem toListModel_insertMany_list {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α]
{l : List (α × β)} {t : Impl α β} (h : t.WF) :
List.Perm (Const.insertMany t l h.balanced).val.toListModel (t.toListModel.insertListConst l) := by
simp only [insertMany_eq_foldl]
induction l generalizing t with
| nil => rfl
| cons e es ih =>
refine (ih h.insert!).trans ?_
exact insertList_perm_of_perm_first (toListModel_insert! h.balanced h.ordered)
h.insert!.ordered.distinctKeys
theorem toListModel_insertMany!_list {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α]
{l : List (α × β)} {t : Impl α β} (h : t.WF) :
List.Perm (Const.insertMany! t l).val.toListModel (t.toListModel.insertListConst l) := by
simpa only [← insertMany_eq_insertMany! h.balanced] using toListModel_insertMany_list h
theorem insertManyIfNewUnit_eq_foldl {_ : Ord α} {l : List α} {t : Impl α Unit} (h : t.Balanced) :
(Const.insertManyIfNewUnit t l h).val = l.foldl (init := t) fun acc k => acc.insertIfNew! k () := by
simp only [insertManyIfNewUnit, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
rw [← List.foldl_hom Subtype.val]
simp only [insertIfNew_eq_insertIfNew!, implies_true]
theorem insertManyIfNewUnit!_eq_foldl {_ : Ord α} {l : List α} {t : Impl α Unit} :
(Const.insertManyIfNewUnit! t l).val = l.foldl (init := t) fun acc k => acc.insertIfNew! k () := by
simp only [insertManyIfNewUnit!, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
rw [← List.foldl_hom Subtype.val]
simp only [implies_true]
theorem insertManyIfNewUnit_eq_insertManyIfNewUnit! {_ : Ord α} {l : List α}
{t : Impl α Unit} (h : t.Balanced) :
(Const.insertManyIfNewUnit t l h).val = (Const.insertManyIfNewUnit! t l).val := by
simp only [insertManyIfNewUnit_eq_foldl, insertManyIfNewUnit!_eq_foldl]
theorem toListModel_insertManyIfNewUnit_list {_ : Ord α} [TransOrd α] [instBEq : BEq α]
[LawfulBEqOrd α] {l : List α} {t : Impl α Unit} (h : t.WF) :
List.Perm (Const.insertManyIfNewUnit t l h.balanced).val.toListModel
(t.toListModel.insertListIfNewUnit l) := by
cases eq_beqOfOrd_of_lawfulBEqOrd instBEq
simp only [insertManyIfNewUnit_eq_foldl]
induction l generalizing t with
| nil => rfl
| cons e es ih =>
refine (ih h.insertIfNew!).trans ?_
exact insertListIfNewUnit_perm_of_perm_first (toListModel_insertIfNew! h.balanced h.ordered)
h.insertIfNew!.ordered.distinctKeys
theorem toListModel_insertManyIfNewUnit!_list {_ : Ord α} [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List α} {t : Impl α Unit} (h : t.WF) :
List.Perm (Const.insertManyIfNewUnit! t l).val.toListModel (t.toListModel.insertListIfNewUnit l) := by
simpa only [← insertManyIfNewUnit_eq_insertManyIfNewUnit! h.balanced] using
toListModel_insertManyIfNewUnit_list h
end Const
/-!
### alter!
-/

601
src/Std/Data/DTreeMap/Lemmas.lean
View file

@ -1160,4 +1160,605 @@ end Const
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β k} :
t.insertMany [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
ext <| Impl.insertMany_cons t.wf
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
(t.insertMany l).contains k = (t.contains k || (l.map Sigma.fst).contains k) :=
Impl.contains_insertMany_list t.wf
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ (l.map Sigma.fst).contains k :=
Impl.mem_insertMany_list t.wf
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
k ∈ t.insertMany l → (l.map Sigma.fst).contains k = false → k ∈ t :=
Impl.mem_of_mem_insertMany_list t.wf
theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
[LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).get? k = t.get? k :=
Impl.get?_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem get?_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
Impl.get?_insertMany_list_of_mem t.wf k_eq distinct mem
theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
[LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains : (l.map Sigma.fst).contains k = false)
{h'} :
(t.insertMany l).get k h' =
t.get k (mem_of_mem_insertMany_list h' contains) :=
Impl.get_insertMany_list_of_contains_eq_false t.wf contains
theorem get_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h'} :
(t.insertMany l).get k' h' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get_insertMany_list_of_mem t.wf k_eq distinct mem
theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp]
[LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).get! k = t.get! k :=
Impl.get!_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem get!_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get!_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
[LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} {fallback : β k}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getD k fallback = t.getD k fallback :=
Impl.getD_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.getD_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKey? k = t.getKey? k :=
Impl.getKey?_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKey? k' = some k :=
Impl.getKey?_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false)
{h'} :
(t.insertMany l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h' contains_eq_false) :=
Impl.getKey_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst)
{h'} :
(t.insertMany l).getKey k' h' = k :=
Impl.getKey_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKey! k = t.getKey! k :=
Impl.getKey!_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKey! k' = k :=
Impl.getKey!_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k fallback : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKeyD k fallback = t.getKeyD k fallback :=
Impl.getKeyD_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKeyD k' fallback = k :=
Impl.getKeyD_insertMany_list_of_mem t.wf k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Sigma.fst).contains a = false) →
(t.insertMany l).size = t.size + l.length :=
Impl.size_insertMany_list t.wf distinct
theorem size_le_size_insertMany_list [TransCmp cmp]
{l : List ((a : α) × β a)} :
t.size ≤ (t.insertMany l).size :=
Impl.size_le_size_insertMany_list t.wf
theorem size_insertMany_list_le [TransCmp cmp]
{l : List ((a : α) × β a)} :
(t.insertMany l).size ≤ t.size + l.length :=
Impl.size_insertMany_list_le t.wf
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp]
{l : List ((a : α) × β a)} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.isEmpty_insertMany_list t.wf
namespace Const
variable {β : Type v} {t : DTreeMap α β cmp}
@[simp]
theorem insertMany_nil :
insertMany t [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β} :
insertMany t [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
Const.insertMany t ((k, v) :: l) = Const.insertMany (t.insert k v) l :=
ext <| Impl.Const.insertMany_cons t.wf
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} :
(Const.insertMany t l).contains k = (t.contains k || (l.map Prod.fst).contains k) :=
Impl.Const.contains_insertMany_list t.wf
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} :
k ∈ Const.insertMany t l ↔ k ∈ t ∨ (l.map Prod.fst).contains k :=
Impl.Const.mem_insertMany_list t.wf
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ( α × β )} {k : α} :
k ∈ insertMany t l → (l.map Prod.fst).contains k = false → k ∈ t :=
Impl.Const.mem_of_mem_insertMany_list t.wf
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKey? k = t.getKey? k :=
Impl.Const.getKey?_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKey? k' = some k :=
Impl.Const.getKey?_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
(insertMany t l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h' contains_eq_false) :=
Impl.Const.getKey_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst)
{h'} :
(insertMany t l).getKey k' h' = k :=
Impl.Const.getKey_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKey! k = t.getKey! k :=
Impl.Const.getKey!_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKey! k' = k :=
Impl.Const.getKey!_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k fallback : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKeyD k fallback = t.getKeyD k fallback :=
Impl.Const.getKeyD_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKeyD k' fallback = k :=
Impl.Const.getKeyD_insertMany_list_of_mem t.wf k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Prod.fst).contains a = false) →
(insertMany t l).size = t.size + l.length :=
Impl.Const.size_insertMany_list t.wf distinct
theorem size_le_size_insertMany_list [TransCmp cmp]
{l : List (α × β)} :
t.size ≤ (insertMany t l).size :=
Impl.Const.size_le_size_insertMany_list t.wf
theorem size_insertMany_list_le [TransCmp cmp]
{l : List (α × β)} :
(insertMany t l).size ≤ t.size + l.length :=
Impl.Const.size_insertMany_list_le t.wf
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp]
{l : List (α × β)} :
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.Const.isEmpty_insertMany_list t.wf
theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
get? (insertMany t l) k = get? t k :=
Impl.Const.get?_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem get?_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
get? (insertMany t l) k' = v :=
Impl.Const.get?_insertMany_list_of_mem t.wf k_eq distinct mem
theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
get (insertMany t l) k h' = get t k (mem_of_mem_insertMany_list h' contains_eq_false) :=
Impl.Const.get_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem get_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) {h'} :
get (insertMany t l) k' h' = v :=
Impl.Const.get_insertMany_list_of_mem t.wf k_eq distinct mem
theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited β] {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
get! (insertMany t l) k = get! t k :=
Impl.Const.get!_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem get!_insertMany_list_of_mem [TransCmp cmp] [Inhabited β]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
get! (insertMany t l) k' = v :=
Impl.Const.get!_insertMany_list_of_mem t.wf k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} {fallback : β}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
getD (insertMany t l) k fallback = getD t k fallback :=
Impl.Const.getD_insertMany_list_of_contains_eq_false t.wf contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v fallback : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
getD (insertMany t l) k' fallback = v :=
Impl.Const.getD_insertMany_list_of_mem t.wf k_eq distinct mem
variable {t : DTreeMap α Unit cmp}
@[simp]
theorem insertManyIfNewUnit_nil :
insertManyIfNewUnit t [] = t :=
rfl
@[simp]
theorem insertManyIfNewUnit_list_singleton {k : α} :
insertManyIfNewUnit t [k] = t.insertIfNew k () :=
rfl
theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
insertManyIfNewUnit t (k :: l) = insertManyIfNewUnit (t.insertIfNew k ()) l :=
ext <| Impl.Const.insertManyIfNewUnit_cons t.wf
@[simp]
theorem contains_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
(insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k) :=
Impl.Const.contains_insertManyIfNewUnit_list t.wf
@[simp]
theorem mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k :=
Impl.Const.mem_insertManyIfNewUnit_list t.wf
theorem mem_of_mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertManyIfNewUnit t l → k ∈ t :=
Impl.Const.mem_of_mem_insertManyIfNewUnit_list t.wf contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} :
¬ k ∈ t → l.contains k = false → getKey? (insertManyIfNewUnit t l) k = none :=
Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false t.wf
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey? (insertManyIfNewUnit t l) k' = some k :=
Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem t.wf k_eq
theorem getKey?_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k : α} :
k ∈ t → getKey? (insertManyIfNewUnit t l) k = getKey? t k :=
Impl.Const.getKey?_insertManyIfNewUnit_list_of_mem t.wf
theorem getKey_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k : α} {h'} (contains : k ∈ t) :
getKey (insertManyIfNewUnit t l) k h' = getKey t k contains :=
Impl.Const.getKey_insertManyIfNewUnit_list_of_mem t.wf contains
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey (insertManyIfNewUnit t l) k' h' = k :=
Impl.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem t.wf k_eq
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α} :
¬ k ∈ t → l.contains k = false →
getKey! (insertManyIfNewUnit t l) k = default :=
Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false t.wf
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey! (insertManyIfNewUnit t l) k' = k :=
Impl.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem t.wf k_eq
theorem getKey!_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k : α} :
k ∈ t → getKey! (insertManyIfNewUnit t l) k = getKey! t k :=
Impl.Const.getKey!_insertManyIfNewUnit_list_of_mem t.wf
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α} :
¬ k ∈ t → l.contains k = false → getKeyD (insertManyIfNewUnit t l) k fallback = fallback :=
Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false t.wf
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKeyD (insertManyIfNewUnit t l) k' fallback = k :=
Impl.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem t.wf k_eq
theorem getKeyD_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k fallback : α} :
k ∈ t → getKeyD (insertManyIfNewUnit t l) k fallback = getKeyD t k fallback :=
Impl.Const.getKeyD_insertManyIfNewUnit_list_of_mem t.wf
theorem size_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertManyIfNewUnit t l).size = t.size + l.length :=
Impl.Const.size_insertManyIfNewUnit_list t.wf distinct
theorem size_le_size_insertManyIfNewUnit_list [TransCmp cmp]
{l : List α} :
t.size ≤ (insertManyIfNewUnit t l).size :=
Impl.Const.size_le_size_insertManyIfNewUnit_list t.wf
theorem size_insertManyIfNewUnit_list_le [TransCmp cmp]
{l : List α} :
(insertManyIfNewUnit t l).size ≤ t.size + l.length :=
Impl.Const.size_insertManyIfNewUnit_list_le t.wf
@[simp]
theorem isEmpty_insertManyIfNewUnit_list [TransCmp cmp] {l : List α} :
(insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.Const.isEmpty_insertManyIfNewUnit_list t.wf
@[simp]
theorem get?_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
get? (insertManyIfNewUnit t l) k =
if k ∈ t ∨ l.contains k then some () else none :=
Impl.Const.get?_insertManyIfNewUnit_list t.wf
@[simp]
theorem get_insertManyIfNewUnit_list {l : List α} {k : α} {h'} :
get (insertManyIfNewUnit t l) k h' = () :=
rfl
@[simp]
theorem get!_insertManyIfNewUnit_list {l : List α} {k : α} :
get! (insertManyIfNewUnit t l) k = () :=
rfl
@[simp]
theorem getD_insertManyIfNewUnit_list
{l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit t l) k fallback = () :=
rfl
end Const
@[simp]
theorem ofList_nil :
ofList ([] : List ((a : α) × (β a))) cmp = ∅ :=
rfl
@[simp]
theorem ofList_singleton {k : α} {v : β k} :
ofList [⟨k, v⟩] cmp = (∅ : DTreeMap α β cmp).insert k v :=
rfl
theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
ofList (⟨k, v⟩ :: tl) cmp = ((∅ : DTreeMap α β cmp).insert k v).insertMany tl :=
ext <| Impl.insertMany_empty_list_cons
@[simp]
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
(ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
simp [ofList, contains, Impl.ofList]
exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
@[simp]
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
k ∈ ofList l cmp ↔ (l.map Sigma.fst).contains k := by
simp [mem_iff_contains]
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).get? k = none :=
Impl.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem get?_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
Impl.get?_insertMany_empty_list_of_mem k_eq distinct mem
theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h} :
(ofList l cmp).get k' h = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get_insertMany_empty_list_of_mem k_eq distinct mem
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).get! k = default :=
Impl.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem get!_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get!_insertMany_empty_list_of_mem k_eq distinct mem
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} {fallback : β k}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getD k fallback = fallback :=
Impl.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getD_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.getD_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKey? k = none :=
Impl.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKey?_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKey? k' = some k :=
Impl.getKey?_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst)
{h'} :
(ofList l cmp).getKey k' h' = k :=
Impl.getKey_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [Inhabited α] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKey! k = default :=
Impl.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKey! k' = k :=
Impl.getKey!_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k fallback : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKeyD k fallback = fallback :=
Impl.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKeyD_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKeyD k' fallback = k :=
Impl.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
end Std.DTreeMap

603
src/Std/Data/DTreeMap/Raw/Lemmas.lean
View file

@ -288,7 +288,7 @@ theorem get?_erase_self [TransCmp cmp] (h : t.WF) {k : α} :
get? (t.erase k) k = none :=
Impl.Const.get?_erase!_self h
theorem get?_eq_get? [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {a : α} : get? t a = t.get? a :=
theorem get?_eq_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : get? t a = t.get? a :=
Impl.Const.get?_eq_get? h
theorem get?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) :
@ -1165,4 +1165,605 @@ end Const
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β k} :
t.insertMany [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List ((a : α) × β a)} {k : α} {v : β k} :
t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
ext <| Impl.insertMany!_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α} :
(t.insertMany l).contains k = (t.contains k || (l.map Sigma.fst).contains k) :=
Impl.contains_insertMany!_list h
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ (l.map Sigma.fst).contains k :=
Impl.mem_insertMany!_list h
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α} :
k ∈ t.insertMany l → (l.map Sigma.fst).contains k = false → k ∈ t :=
Impl.mem_of_mem_insertMany!_list h
theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
[LawfulBEqCmp cmp] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).get? k = t.get? k :=
Impl.get?_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem get?_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
Impl.get?_insertMany!_list_of_mem h k_eq distinct mem
theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α]
[LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α}
(contains : (l.map Sigma.fst).contains k = false)
{h'} :
(t.insertMany l).get k h' =
t.get k (mem_of_mem_insertMany_list h h' contains) :=
Impl.get_insertMany!_list_of_contains_eq_false h contains
theorem get_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h'} :
(t.insertMany l).get k' h' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get_insertMany!_list_of_mem h k_eq distinct mem
theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp]
[LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).get! k = t.get! k :=
Impl.get!_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem get!_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get!_insertMany!_list_of_mem h k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
[LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k : α} {fallback : β k}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getD k fallback = t.getD k fallback :=
Impl.getD_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.getD_insertMany!_list_of_mem h k_eq distinct mem
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKey? k = t.getKey? k :=
Impl.getKey?_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKey? k' = some k :=
Impl.getKey?_insertMany!_list_of_mem h k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false)
{h'} :
(t.insertMany l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h h' contains_eq_false) :=
Impl.getKey_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst)
{h'} :
(t.insertMany l).getKey k' h' = k :=
Impl.getKey_insertMany!_list_of_mem h k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKey! k = t.getKey! k :=
Impl.getKey!_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF)
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKey! k' = k :=
Impl.getKey!_insertMany!_list_of_mem h k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List ((a : α) × β a)} {k fallback : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(t.insertMany l).getKeyD k fallback = t.getKeyD k fallback :=
Impl.getKeyD_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(t.insertMany l).getKeyD k' fallback = k :=
Impl.getKeyD_insertMany!_list_of_mem h k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Sigma.fst).contains a = false) →
(t.insertMany l).size = t.size + l.length :=
Impl.size_insertMany!_list h distinct
theorem size_le_size_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} :
t.size ≤ (t.insertMany l).size :=
Impl.size_le_size_insertMany!_list h
theorem size_insertMany_list_le [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} :
(t.insertMany l).size ≤ t.size + l.length :=
Impl.size_insertMany!_list_le h
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List ((a : α) × β a)} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.isEmpty_insertMany!_list h
namespace Const
variable {β : Type v} {t : Raw α β cmp}
@[simp]
theorem insertMany_nil :
insertMany t [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β} :
insertMany t [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
Const.insertMany t ((k, v) :: l) = Const.insertMany (t.insert k v) l :=
ext <| Impl.Const.insertMany!_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} :
(Const.insertMany t l).contains k = (t.contains k || (l.map Prod.fst).contains k) :=
Impl.Const.contains_insertMany!_list h
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} :
k ∈ Const.insertMany t l ↔ k ∈ t ∨ (l.map Prod.fst).contains k :=
Impl.Const.mem_insertMany!_list h
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List ( α × β )} {k : α} :
k ∈ insertMany t l → (l.map Prod.fst).contains k = false → k ∈ t :=
Impl.Const.mem_of_mem_insertMany!_list h
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKey? k = t.getKey? k :=
Impl.Const.getKey?_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKey? k' = some k :=
Impl.Const.getKey?_insertMany!_list_of_mem h k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
(insertMany t l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h h' contains_eq_false) :=
Impl.Const.getKey_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst)
{h'} :
(insertMany t l).getKey k' h' = k :=
Impl.Const.getKey_insertMany!_list_of_mem h k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] (h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKey! k = t.getKey! k :=
Impl.Const.getKey!_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKey! k' = k :=
Impl.Const.getKey!_insertMany!_list_of_mem h k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k fallback : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(insertMany t l).getKeyD k fallback = t.getKeyD k fallback :=
Impl.Const.getKeyD_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(insertMany t l).getKeyD k' fallback = k :=
Impl.Const.getKeyD_insertMany!_list_of_mem h k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Prod.fst).contains a = false) →
(insertMany t l).size = t.size + l.length :=
Impl.Const.size_insertMany!_list h distinct
theorem size_le_size_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
t.size ≤ (insertMany t l).size :=
Impl.Const.size_le_size_insertMany!_list h
theorem size_insertMany_list_le [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
(insertMany t l).size ≤ t.size + l.length :=
Impl.Const.size_insertMany!_list_le h
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.Const.isEmpty_insertMany!_list h
theorem get?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
get? (insertMany t l) k = get? t k :=
Impl.Const.get?_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem get?_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
get? (insertMany t l) k' = v :=
Impl.Const.get?_insertMany!_list_of_mem h k_eq distinct mem
theorem get_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
get (insertMany t l) k h' = get t k (mem_of_mem_insertMany_list h h' contains_eq_false) :=
Impl.Const.get_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem get_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) {h'} :
get (insertMany t l) k' h' = v :=
Impl.Const.get_insertMany!_list_of_mem h k_eq distinct mem
theorem get!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited β] (h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
get! (insertMany t l) k = get! t k :=
Impl.Const.get!_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem get!_insertMany_list_of_mem [TransCmp cmp] [Inhabited β] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
get! (insertMany t l) k' = v :=
Impl.Const.get!_insertMany!_list_of_mem h k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α} {fallback : β}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
getD (insertMany t l) k fallback = getD t k fallback :=
Impl.Const.getD_insertMany!_list_of_contains_eq_false h contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v fallback : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
getD (insertMany t l) k' fallback = v :=
Impl.Const.getD_insertMany!_list_of_mem h k_eq distinct mem
variable {t : Raw α Unit cmp}
@[simp]
theorem insertManyIfNewUnit_nil :
insertManyIfNewUnit t [] = t :=
rfl
@[simp]
theorem insertManyIfNewUnit_list_singleton {k : α} :
insertManyIfNewUnit t [k] = t.insertIfNew k () :=
rfl
theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
insertManyIfNewUnit t (k :: l) = insertManyIfNewUnit (t.insertIfNew k ()) l :=
ext <| Impl.Const.insertManyIfNewUnit!_cons
@[simp]
theorem contains_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
(insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k) :=
Impl.Const.contains_insertManyIfNewUnit!_list h
@[simp]
theorem mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k :=
Impl.Const.mem_insertManyIfNewUnit!_list h
theorem mem_of_mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertManyIfNewUnit t l → k ∈ t :=
Impl.Const.mem_of_mem_insertManyIfNewUnit!_list h contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α} :
¬ k ∈ t → l.contains k = false → getKey? (insertManyIfNewUnit t l) k = none :=
Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false h
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey? (insertManyIfNewUnit t l) k' = some k :=
Impl.Const.getKey?_insertManyIfNewUnit!_list_of_not_mem_of_mem h k_eq
theorem getKey?_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} :
k ∈ t → getKey? (insertManyIfNewUnit t l) k = getKey? t k :=
Impl.Const.getKey?_insertManyIfNewUnit!_list_of_mem h
theorem getKey_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} {h'} (contains : k ∈ t) :
getKey (insertManyIfNewUnit t l) k h' = getKey t k contains :=
Impl.Const.getKey_insertManyIfNewUnit!_list_of_mem h contains
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey (insertManyIfNewUnit t l) k' h' = k :=
Impl.Const.getKey_insertManyIfNewUnit!_list_of_not_mem_of_mem h k_eq
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α} :
¬ k ∈ t → l.contains k = false →
getKey! (insertManyIfNewUnit t l) k = default :=
Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false h
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKey! (insertManyIfNewUnit t l) k' = k :=
Impl.Const.getKey!_insertManyIfNewUnit!_list_of_not_mem_of_mem h k_eq
theorem getKey!_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k : α} :
k ∈ t → getKey! (insertManyIfNewUnit t l) k = getKey! t k :=
Impl.Const.getKey!_insertManyIfNewUnit!_list_of_mem h
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k fallback : α} :
¬ k ∈ t → l.contains k = false → getKeyD (insertManyIfNewUnit t l) k fallback = fallback :=
Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false h
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq) :
¬ k ∈ t → l.Pairwise (fun a b => ¬ cmp a b = .eq) → k ∈ l →
getKeyD (insertManyIfNewUnit t l) k' fallback = k :=
Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_mem h k_eq
theorem getKeyD_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k fallback : α} :
k ∈ t → getKeyD (insertManyIfNewUnit t l) k fallback = getKeyD t k fallback :=
Impl.Const.getKeyD_insertManyIfNewUnit!_list_of_mem h
theorem size_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertManyIfNewUnit t l).size = t.size + l.length :=
Impl.Const.size_insertManyIfNewUnit!_list h distinct
theorem size_le_size_insertManyIfNewUnit_list [TransCmp cmp] (h : t.WF)
{l : List α} :
t.size ≤ (insertManyIfNewUnit t l).size :=
Impl.Const.size_le_size_insertManyIfNewUnit!_list h
theorem size_insertManyIfNewUnit_list_le [TransCmp cmp] (h : t.WF)
{l : List α} :
(insertManyIfNewUnit t l).size ≤ t.size + l.length :=
Impl.Const.size_insertManyIfNewUnit!_list_le h
@[simp]
theorem isEmpty_insertManyIfNewUnit_list [TransCmp cmp] (h : t.WF) {l : List α} :
(insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty) :=
Impl.Const.isEmpty_insertManyIfNewUnit!_list h
@[simp]
theorem get?_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
get? (insertManyIfNewUnit t l) k =
if k ∈ t ∨ l.contains k then some () else none :=
Impl.Const.get?_insertManyIfNewUnit!_list h
@[simp]
theorem get_insertManyIfNewUnit_list {l : List α} {k : α} {h'} :
get (insertManyIfNewUnit t l) k h' = () :=
rfl
@[simp]
theorem get!_insertManyIfNewUnit_list {l : List α} {k : α} :
get! (insertManyIfNewUnit t l) k = () :=
rfl
@[simp]
theorem getD_insertManyIfNewUnit_list
{l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit t l) k fallback = () :=
rfl
end Const
@[simp]
theorem ofList_nil :
ofList ([] : List ((a : α) × (β a))) cmp = ∅ :=
rfl
@[simp]
theorem ofList_singleton {k : α} {v : β k} :
ofList [⟨k, v⟩] cmp = (∅ : Raw α β cmp).insert k v :=
rfl
theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} :
ofList (⟨k, v⟩ :: tl) cmp = ((∅ : Raw α β cmp).insert k v).insertMany tl :=
ext <| Impl.insertMany_empty_list_cons_eq_insertMany!
@[simp]
theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
(ofList l cmp).contains k = (l.map Sigma.fst).contains k := by
simp [ofList, contains, Impl.ofList]
exact Impl.contains_insertMany_empty_list (instOrd := ⟨cmp⟩) (k := k) (l := l)
@[simp]
theorem mem_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} :
k ∈ ofList l cmp ↔ (l.map Sigma.fst).contains k := by
simp [mem_iff_contains]
theorem get?_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).get? k = none :=
Impl.get?_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem get?_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_eq) v) :=
Impl.get?_insertMany_empty_list_of_mem k_eq distinct mem
theorem get_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h} :
(ofList l cmp).get k' h = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get_insertMany_empty_list_of_mem k_eq distinct mem
theorem get!_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).get! k = default :=
Impl.get!_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem get!_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} [Inhabited (β k')]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.get!_insertMany_empty_list_of_mem k_eq distinct mem
theorem getD_ofList_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α} {fallback : β k}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getD k fallback = fallback :=
Impl.getD_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getD_ofList_of_mem [TransCmp cmp] [LawfulEqCmp cmp]
{l : List ((a : α) × β a)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β k} {fallback : β k'}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(ofList l cmp).getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_eq) v :=
Impl.getD_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey?_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKey? k = none :=
Impl.getKey?_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKey?_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKey? k' = some k :=
Impl.getKey?_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst)
{h'} :
(ofList l cmp).getKey k' h' = k :=
Impl.getKey_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKey!_ofList_of_contains_eq_false [TransCmp cmp] [Inhabited α] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKey! k = default :=
Impl.getKey!_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKey!_ofList_of_mem [TransCmp cmp] [Inhabited α]
{l : List ((a : α) × β a)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKey! k' = k :=
Impl.getKey!_insertMany_empty_list_of_mem k_eq distinct mem
theorem getKeyD_ofList_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List ((a : α) × β a)} {k fallback : α}
(contains_eq_false : (l.map Sigma.fst).contains k = false) :
(ofList l cmp).getKeyD k fallback = fallback :=
Impl.getKeyD_insertMany_empty_list_of_contains_eq_false contains_eq_false
theorem getKeyD_ofList_of_mem [TransCmp cmp]
{l : List ((a : α) × β a)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Sigma.fst) :
(ofList l cmp).getKeyD k' fallback = k :=
Impl.getKeyD_insertMany_empty_list_of_mem k_eq distinct mem
end Std.DTreeMap.Raw

2
src/Std/Data/HashMap/RawLemmas.lean
View file

@ -1068,7 +1068,7 @@ theorem mem_of_mem_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List α} {k : α}
(not_mem : ¬ k ∈ m) (contains_eq_false: l.contains k = false) :
(not_mem : ¬ k ∈ m) (contains_eq_false : l.contains k = false) :
getKey? (insertManyIfNewUnit m l) k = none :=
DHashMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h.out not_mem contains_eq_false

60
src/Std/Data/Internal/List/Associative.lean
View file

@ -2384,8 +2384,8 @@ theorem getValueCast?_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
theorem getValueCast?_insertList_of_mem [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k') {v : β k}
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') {v : β k}
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValueCast? k' (insertList l toInsert) =
@ -2412,15 +2412,15 @@ theorem getValueCast_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
theorem getValueCast_insertList_of_mem [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k') (v : β k)
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') (v : β k)
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert)
{h} :
getValueCast k' (insertList l toInsert) h =
cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast,
getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem]
getValueCast?_insertList_of_mem distinct_l k_beq distinct_toInsert mem]
theorem getValueCast!_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)} {k : α} [Inhabited (β k)]
@ -2431,14 +2431,14 @@ theorem getValueCast!_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
theorem getValueCast!_insertList_of_mem [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k') (v : β k) [Inhabited (β k')]
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') (v : β k) [Inhabited (β k')]
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValueCast! k' (insertList l toInsert) =
cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
rw [getValueCast!_eq_getValueCast?,
getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem, Option.get!_some]
getValueCast?_insertList_of_mem distinct_l k_beq distinct_toInsert mem, Option.get!_some]
theorem getValueCastD_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k}
@ -2449,14 +2449,14 @@ theorem getValueCastD_insertList_of_contains_eq_false [BEq α] [LawfulBEq α]
theorem getValueCastD_insertList_of_mem [BEq α] [LawfulBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValueCastD k' (insertList l toInsert) fallback =
cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v := by
rw [getValueCastD_eq_getValueCast?,
getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem, Option.getD_some]
getValueCast?_insertList_of_mem distinct_l k_beq distinct_toInsert mem, Option.getD_some]
theorem getKey?_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
{l toInsert : List ((a : α) × β a)} {k : α}
@ -2468,8 +2468,8 @@ theorem getKey?_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKey?_insertList_of_mem [BEq α] [EquivBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Sigma.fst) :
getKey? k' (insertList l toInsert) = some k := by
@ -2489,14 +2489,14 @@ theorem getKey_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKey_insertList_of_mem [BEq α] [EquivBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Sigma.fst)
{h} :
getKey k' (insertList l toInsert) h = k := by
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem]
getKey?_insertList_of_mem distinct_l k_beq distinct_toInsert mem]
theorem getKey!_insertList_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
{l toInsert : List ((a : α) × β a)} {k : α}
@ -2506,12 +2506,12 @@ theorem getKey!_insertList_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabite
theorem getKey!_insertList_of_mem [BEq α] [EquivBEq α] [Inhabited α]
{l toInsert : List ((a : α) × β a)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Sigma.fst) :
getKey! k' (insertList l toInsert) = k := by
rw [getKey!_eq_getKey?, getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem,
rw [getKey!_eq_getKey?, getKey?_insertList_of_mem distinct_l k_beq distinct_toInsert mem,
Option.get!_some]
theorem getKeyD_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
@ -2522,12 +2522,12 @@ theorem getKeyD_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKeyD_insertList_of_mem [BEq α] [EquivBEq α]
{l toInsert : List ((a : α) × β a)}
{k k' fallback : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' fallback : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Sigma.fst) :
getKeyD k' (insertList l toInsert) fallback = k := by
rw [getKeyD_eq_getKey?, getKey?_insertList_of_mem k_beq distinct_l distinct_toInsert mem,
rw [getKeyD_eq_getKey?, getKey?_insertList_of_mem distinct_l k_beq distinct_toInsert mem,
Option.getD_some]
theorem perm_insertList [BEq α] [EquivBEq α]
@ -2627,13 +2627,13 @@ theorem getKey?_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKey?_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Prod.fst) :
getKey? k' (insertListConst l toInsert) = some k := by
unfold insertListConst
apply getKey?_insertList_of_mem k_beq distinct_l
apply getKey?_insertList_of_mem distinct_l k_beq
· simpa [List.pairwise_map]
· simp only [List.map_map, Prod.fst_comp_toSigma]
exact mem
@ -2649,14 +2649,14 @@ theorem getKey_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKey_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Prod.fst)
{h} :
getKey k' (insertListConst l toInsert) h = k := by
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem]
getKey?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem]
theorem getKey!_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α] [Inhabited α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
@ -2667,12 +2667,12 @@ theorem getKey!_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α] [Inh
theorem getKey!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Prod.fst) :
getKey! k' (insertListConst l toInsert) = k := by
rw [getKey!_eq_getKey?, getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem,
rw [getKey!_eq_getKey?, getKey?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem,
Option.get!_some]
theorem getKeyD_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
@ -2684,12 +2684,12 @@ theorem getKeyD_insertListConst_of_contains_eq_false [BEq α] [EquivBEq α]
theorem getKeyD_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' fallback : α} (k_beq : k == k')
(distinct_l : DistinctKeys l)
{k k' fallback : α} (k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : k ∈ toInsert.map Prod.fst) :
getKeyD k' (insertListConst l toInsert) fallback = k := by
rw [getKeyD_eq_getKey?, getKey?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem,
rw [getKeyD_eq_getKey?, getKey?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem,
Option.getD_some]
theorem length_insertListConst [BEq α] [EquivBEq α]
@ -2736,8 +2736,8 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' : α} (k_beq : k == k') {v : β}
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') {v : β}
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValue? k' (insertListConst l toInsert) = v := by
@ -2772,14 +2772,14 @@ theorem getValue_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
theorem getValue_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)}
{k k' : α} (k_beq : k == k') {v : β}
(distinct_l : DistinctKeys l)
{k k' : α} (k_beq : k == k') {v : β}
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert)
{h} :
getValue k' (insertListConst l toInsert) h = v := by
rw [← Option.some_inj, ← getValue?_eq_some_getValue,
getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem]
getValue?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem]
theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α] [Inhabited β]
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α}
@ -2789,13 +2789,14 @@ theorem getValue!_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
rw [getValue?_insertListConst_of_contains_eq_false not_contains]
theorem getValue!_insertListConst_of_mem [BEq α] [EquivBEq α] [Inhabited β]
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β} (k_beq : k == k')
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v: β}
(distinct_l : DistinctKeys l)
(k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValue! k' (insertListConst l toInsert) = v := by
rw [getValue!_eq_getValue?,
getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.get!_some]
getValue?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem, Option.get!_some]
theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k : α} {fallback : β}
@ -2805,13 +2806,14 @@ theorem getValueD_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq
rw [getValue?_insertListConst_of_contains_eq_false not_contains]
theorem getValueD_insertListConst_of_mem [BEq α] [EquivBEq α]
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β} (k_beq : k == k')
{l : List ((_ : α) × β)} {toInsert : List (α × β)} {k k' : α} {v fallback: β}
(distinct_l : DistinctKeys l)
(k_beq : k == k')
(distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
(mem : ⟨k, v⟩ ∈ toInsert) :
getValueD k' (insertListConst l toInsert) fallback= v := by
simp only [getValueD_eq_getValue?]
rw [getValue?_insertListConst_of_mem k_beq distinct_l distinct_toInsert mem, Option.getD_some]
rw [getValue?_insertListConst_of_mem distinct_l k_beq distinct_toInsert mem, Option.getD_some]
/-- Internal implementation detail of the hash map -/
def insertListIfNewUnit [BEq α] (l: List ((_ : α) × Unit)) (toInsert: List α) :

312
src/Std/Data/TreeMap/Lemmas.lean
View file

@ -791,4 +791,316 @@ theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForI
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β} :
t.insertMany [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
ext <| DTreeMap.Const.insertMany_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} :
(t.insertMany l).contains k = (t.contains k || (l.map Prod.fst).contains k) :=
DTreeMap.Const.contains_insertMany_list
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ (l.map Prod.fst).contains k :=
DTreeMap.Const.mem_insertMany_list
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} :
k ∈ t.insertMany l → (l.map Prod.fst).contains k = false → k ∈ t :=
DTreeMap.Const.mem_of_mem_insertMany_list
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKey? k = t.getKey? k :=
DTreeMap.Const.getKey?_insertMany_list_of_contains_eq_false contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKey? k' = some k :=
DTreeMap.Const.getKey?_insertMany_list_of_mem k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
(t.insertMany l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h' contains_eq_false) :=
DTreeMap.Const.getKey_insertMany_list_of_contains_eq_false contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst)
{h'} :
(t.insertMany l).getKey k' h' = k :=
DTreeMap.Const.getKey_insertMany_list_of_mem k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKey! k = t.getKey! k :=
DTreeMap.Const.getKey!_insertMany_list_of_contains_eq_false contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α]
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKey! k' = k :=
DTreeMap.Const.getKey!_insertMany_list_of_mem k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k fallback : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKeyD k fallback = t.getKeyD k fallback :=
DTreeMap.Const.getKeyD_insertMany_list_of_contains_eq_false contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKeyD k' fallback = k :=
DTreeMap.Const.getKeyD_insertMany_list_of_mem k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Prod.fst).contains a = false) →
(t.insertMany l).size = t.size + l.length :=
DTreeMap.Const.size_insertMany_list distinct
theorem size_le_size_insertMany_list [TransCmp cmp]
{l : List (α × β)} :
t.size ≤ (t.insertMany l).size :=
DTreeMap.Const.size_le_size_insertMany_list
theorem size_insertMany_list_le [TransCmp cmp]
{l : List (α × β)} :
(t.insertMany l).size ≤ t.size + l.length :=
DTreeMap.Const.size_insertMany_list_le
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp]
{l : List (α × β)} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty) :=
DTreeMap.Const.isEmpty_insertMany_list
theorem getElem?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
[LawfulBEqCmp cmp] {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l)[k]? = t[k]? :=
DTreeMap.Const.get?_insertMany_list_of_contains_eq_false contains_eq_false
theorem getElem?_insertMany_list_of_mem [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l)[k']? = some v :=
DTreeMap.Const.get?_insertMany_list_of_mem k_eq distinct mem
theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
[LawfulBEqCmp cmp]
{l : List (α × β)} {k : α}
(contains : (l.map Prod.fst).contains k = false)
{h'} :
(t.insertMany l)[k]'h' =
t.get k (mem_of_mem_insertMany_list h' contains) :=
DTreeMap.Const.get_insertMany_list_of_contains_eq_false contains
theorem getElem_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h'} :
(t.insertMany l)[k']'h' = v :=
DTreeMap.Const.get_insertMany_list_of_mem k_eq distinct mem
theorem getElem!_insertMany_list_of_contains_eq_false [TransCmp cmp]
[BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} [Inhabited β]
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l)[k]! = t.get! k :=
DTreeMap.Const.get!_insertMany_list_of_contains_eq_false contains_eq_false
theorem getElem!_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l)[k']! = v :=
DTreeMap.Const.get!_insertMany_list_of_mem k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
[BEq α] [LawfulBEqCmp cmp]
{l : List (α × β)} {k : α} {fallback : β}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getD k fallback = t.getD k fallback :=
DTreeMap.Const.getD_insertMany_list_of_contains_eq_false contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp]
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).getD k' fallback = v :=
DTreeMap.Const.getD_insertMany_list_of_mem k_eq distinct mem
variable {t : TreeMap α Unit cmp}
@[simp]
theorem insertManyIfNewUnit_nil :
insertManyIfNewUnit t [] = t :=
rfl
@[simp]
theorem insertManyIfNewUnit_list_singleton {k : α} :
insertManyIfNewUnit t [k] = t.insertIfNew k () :=
rfl
theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
insertManyIfNewUnit t (k :: l) = insertManyIfNewUnit (t.insertIfNew k ()) l :=
ext <| DTreeMap.Const.insertManyIfNewUnit_cons
@[simp]
theorem contains_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
(insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k) :=
DTreeMap.Const.contains_insertManyIfNewUnit_list
@[simp]
theorem mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k :=
DTreeMap.Const.mem_insertManyIfNewUnit_list
theorem mem_of_mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertManyIfNewUnit t l → k ∈ t :=
DTreeMap.Const.mem_of_mem_insertManyIfNewUnit_list contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKey? (insertManyIfNewUnit t l) k = none :=
DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey? (insertManyIfNewUnit t l) k' = some k :=
DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem getKey?_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k : α} (mem : k ∈ t) :
getKey? (insertManyIfNewUnit t l) k = getKey? t k :=
DTreeMap.Const.getKey?_insertManyIfNewUnit_list_of_mem mem
theorem getKey_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k : α} {h'} (contains : k ∈ t) :
getKey (insertManyIfNewUnit t l) k h' = getKey t k contains :=
DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_mem contains
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} (not_mem : ¬ k ∈ t)
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey (insertManyIfNewUnit t l) k' h' = k :=
DTreeMap.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKey! (insertManyIfNewUnit t l) k = default :=
DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey! (insertManyIfNewUnit t l) k' = k :=
DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem getKey!_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k : α} (mem : k ∈ t):
getKey! (insertManyIfNewUnit t l) k = getKey! t k :=
DTreeMap.Const.getKey!_insertManyIfNewUnit_list_of_mem mem
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKeyD (insertManyIfNewUnit t l) k fallback = fallback :=
DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKeyD (insertManyIfNewUnit t l) k' fallback = k :=
DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem getKeyD_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
{l : List α} {k fallback : α} (mem : k ∈ t) :
getKeyD (insertManyIfNewUnit t l) k fallback = getKeyD t k fallback :=
DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_mem mem
theorem size_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertManyIfNewUnit t l).size = t.size + l.length :=
DTreeMap.Const.size_insertManyIfNewUnit_list distinct
theorem size_le_size_insertManyIfNewUnit_list [TransCmp cmp]
{l : List α} :
t.size ≤ (insertManyIfNewUnit t l).size :=
DTreeMap.Const.size_le_size_insertManyIfNewUnit_list
theorem size_insertManyIfNewUnit_list_le [TransCmp cmp]
{l : List α} :
(insertManyIfNewUnit t l).size ≤ t.size + l.length :=
DTreeMap.Const.size_insertManyIfNewUnit_list_le
@[simp]
theorem isEmpty_insertManyIfNewUnit_list [TransCmp cmp] {l : List α} :
(insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty) :=
DTreeMap.Const.isEmpty_insertManyIfNewUnit_list
@[simp]
theorem getElem?_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
(insertManyIfNewUnit t l)[k]? = if k ∈ t ∨ l.contains k then some () else none :=
DTreeMap.Const.get?_insertManyIfNewUnit_list
@[simp]
theorem getElem_insertManyIfNewUnit_list {l : List α} {k : α} {h'} :
(insertManyIfNewUnit t l)[k]'h' = () :=
rfl
@[simp]
theorem getElem!_insertManyIfNewUnit_list {l : List α} {k : α} :
(insertManyIfNewUnit t l)[k]! = () :=
rfl
@[simp]
theorem getD_insertManyIfNewUnit_list
{l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit t l) k fallback = () :=
rfl
end Std.TreeMap

312
src/Std/Data/TreeMap/Raw/Lemmas.lean
View file

@ -799,4 +799,316 @@ theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m]
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} {v : β} :
t.insertMany [⟨k, v⟩] = t.insert k v :=
rfl
theorem insertMany_cons {l : List (α × β)} {k : α} {v : β} :
t.insertMany (⟨k, v⟩ :: l) = (t.insert k v).insertMany l :=
ext <| DTreeMap.Raw.Const.insertMany_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} :
(t.insertMany l).contains k = (t.contains k || (l.map Prod.fst).contains k) :=
DTreeMap.Raw.Const.contains_insertMany_list h
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} :
k ∈ t.insertMany l ↔ k ∈ t ∨ (l.map Prod.fst).contains k :=
DTreeMap.Raw.Const.mem_insertMany_list h
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} :
k ∈ t.insertMany l → (l.map Prod.fst).contains k = false → k ∈ t :=
DTreeMap.Raw.Const.mem_of_mem_insertMany_list h
theorem getKey?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKey? k = t.getKey? k :=
DTreeMap.Raw.Const.getKey?_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getKey?_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKey? k' = some k :=
DTreeMap.Raw.Const.getKey?_insertMany_list_of_mem h k_eq distinct mem
theorem getKey_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false)
{h'} :
(t.insertMany l).getKey k h' =
t.getKey k (mem_of_mem_insertMany_list h h' contains_eq_false) :=
DTreeMap.Raw.Const.getKey_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getKey_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst)
{h'} :
(t.insertMany l).getKey k' h' = k :=
DTreeMap.Raw.Const.getKey_insertMany_list_of_mem h k_eq distinct mem
theorem getKey!_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
[Inhabited α] (h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKey! k = t.getKey! k :=
DTreeMap.Raw.Const.getKey!_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getKey!_insertMany_list_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF)
{l : List (α × β)}
{k k' : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKey! k' = k :=
DTreeMap.Raw.Const.getKey!_insertMany_list_of_mem h k_eq distinct mem
theorem getKeyD_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k fallback : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getKeyD k fallback = t.getKeyD k fallback :=
DTreeMap.Raw.Const.getKeyD_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getKeyD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)}
{k k' fallback : α} (k_eq : cmp k k' = .eq)
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : k ∈ l.map Prod.fst) :
(t.insertMany l).getKeyD k' fallback = k :=
DTreeMap.Raw.Const.getKeyD_insertMany_list_of_mem h k_eq distinct mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} (distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) :
(∀ (a : α), a ∈ t → (l.map Prod.fst).contains a = false) →
(t.insertMany l).size = t.size + l.length :=
DTreeMap.Raw.Const.size_insertMany_list h distinct
theorem size_le_size_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
t.size ≤ (t.insertMany l).size :=
DTreeMap.Raw.Const.size_le_size_insertMany_list h
theorem size_insertMany_list_le [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
(t.insertMany l).size ≤ t.size + l.length :=
DTreeMap.Raw.Const.size_insertMany_list_le h
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List (α × β)} :
(t.insertMany l).isEmpty = (t.isEmpty && l.isEmpty) :=
DTreeMap.Raw.Const.isEmpty_insertMany_list h
theorem getElem?_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
[LawfulBEqCmp cmp] (h : t.WF) {l : List (α × β)} {k : α}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l)[k]? = t[k]? :=
DTreeMap.Raw.Const.get?_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getElem?_insertMany_list_of_mem [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
(h : t.WF) {l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq)) (mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l)[k']? = some v :=
DTreeMap.Raw.Const.get?_insertMany_list_of_mem h k_eq distinct mem
theorem getElem_insertMany_list_of_contains_eq_false [TransCmp cmp] [BEq α]
[LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α}
(contains : (l.map Prod.fst).contains k = false)
{h'} :
(t.insertMany l)[k]'h' =
t.get k (mem_of_mem_insertMany_list h h' contains) :=
DTreeMap.Raw.Const.get_insertMany_list_of_contains_eq_false h contains
theorem getElem_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l)
{h'} :
(t.insertMany l)[k']'h' = v :=
DTreeMap.Raw.Const.get_insertMany_list_of_mem h k_eq distinct mem
theorem getElem!_insertMany_list_of_contains_eq_false [TransCmp cmp]
[BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} [Inhabited β]
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l)[k]! = t.get! k :=
DTreeMap.Raw.Const.get!_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getElem!_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} [Inhabited β]
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l)[k']! = v :=
DTreeMap.Raw.Const.get!_insertMany_list_of_mem h k_eq distinct mem
theorem getD_insertMany_list_of_contains_eq_false [TransCmp cmp]
[BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List (α × β)} {k : α} {fallback : β}
(contains_eq_false : (l.map Prod.fst).contains k = false) :
(t.insertMany l).getD k fallback = t.getD k fallback :=
DTreeMap.Raw.Const.getD_insertMany_list_of_contains_eq_false h contains_eq_false
theorem getD_insertMany_list_of_mem [TransCmp cmp] (h : t.WF)
{l : List (α × β)} {k k' : α} (k_eq : cmp k k' = .eq) {v : β} {fallback : β}
(distinct : l.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq))
(mem : ⟨k, v⟩ ∈ l) :
(t.insertMany l).getD k' fallback = v :=
DTreeMap.Raw.Const.getD_insertMany_list_of_mem h k_eq distinct mem
variable {t : Raw α Unit cmp}
@[simp]
theorem insertManyIfNewUnit_nil :
insertManyIfNewUnit t [] = t :=
rfl
@[simp]
theorem insertManyIfNewUnit_list_singleton {k : α} :
insertManyIfNewUnit t [k] = t.insertIfNew k () :=
rfl
theorem insertManyIfNewUnit_cons {l : List α} {k : α} :
insertManyIfNewUnit t (k :: l) = insertManyIfNewUnit (t.insertIfNew k ()) l :=
ext <| DTreeMap.Raw.Const.insertManyIfNewUnit_cons
@[simp]
theorem contains_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
(insertManyIfNewUnit t l).contains k = (t.contains k || l.contains k) :=
DTreeMap.Raw.Const.contains_insertManyIfNewUnit_list h
@[simp]
theorem mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
k ∈ insertManyIfNewUnit t l ↔ k ∈ t ∨ l.contains k :=
DTreeMap.Raw.Const.mem_insertManyIfNewUnit_list h
theorem mem_of_mem_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertManyIfNewUnit t l → k ∈ t :=
DTreeMap.Raw.Const.mem_of_mem_insertManyIfNewUnit_list h contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKey? (insertManyIfNewUnit t l) k = none :=
DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey? (insertManyIfNewUnit t l) k' = some k :=
DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem getKey?_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} (mem : k ∈ t) :
getKey? (insertManyIfNewUnit t l) k = getKey? t k :=
DTreeMap.Raw.Const.getKey?_insertManyIfNewUnit_list_of_mem h mem
theorem getKey_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} {h'} (contains : k ∈ t) :
getKey (insertManyIfNewUnit t l) k h' = getKey t k contains :=
DTreeMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_mem h contains
theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} (not_mem : ¬ k ∈ t)
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey (insertManyIfNewUnit t l) k' h' = k :=
DTreeMap.Raw.Const.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKey! (insertManyIfNewUnit t l) k = default :=
DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKey! (insertManyIfNewUnit t l) k' = k :=
DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem getKey!_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t):
getKey! (insertManyIfNewUnit t l) k = getKey! t k :=
DTreeMap.Raw.Const.getKey!_insertManyIfNewUnit_list_of_mem h mem
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k fallback : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getKeyD (insertManyIfNewUnit t l) k fallback = fallback :=
DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getKeyD (insertManyIfNewUnit t l) k' fallback = k :=
DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem getKeyD_insertManyIfNewUnit_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k fallback : α} (mem : k ∈ t) :
getKeyD (insertManyIfNewUnit t l) k fallback = getKeyD t k fallback :=
DTreeMap.Raw.Const.getKeyD_insertManyIfNewUnit_list_of_mem h mem
theorem size_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertManyIfNewUnit t l).size = t.size + l.length :=
DTreeMap.Raw.Const.size_insertManyIfNewUnit_list h distinct
theorem size_le_size_insertManyIfNewUnit_list [TransCmp cmp] (h : t.WF)
{l : List α} :
t.size ≤ (insertManyIfNewUnit t l).size :=
DTreeMap.Raw.Const.size_le_size_insertManyIfNewUnit_list h
theorem size_insertManyIfNewUnit_list_le [TransCmp cmp] (h : t.WF)
{l : List α} :
(insertManyIfNewUnit t l).size ≤ t.size + l.length :=
DTreeMap.Raw.Const.size_insertManyIfNewUnit_list_le h
@[simp]
theorem isEmpty_insertManyIfNewUnit_list [TransCmp cmp] (h : t.WF) {l : List α} :
(insertManyIfNewUnit t l).isEmpty = (t.isEmpty && l.isEmpty) :=
DTreeMap.Raw.Const.isEmpty_insertManyIfNewUnit_list h
@[simp]
theorem getElem?_insertManyIfNewUnit_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
(insertManyIfNewUnit t l)[k]? = if k ∈ t ∨ l.contains k then some () else none :=
DTreeMap.Raw.Const.get?_insertManyIfNewUnit_list h
@[simp]
theorem getElem_insertManyIfNewUnit_list {l : List α} {k : α} {h'} :
(insertManyIfNewUnit t l)[k]'h' = () :=
rfl
@[simp]
theorem getElem!_insertManyIfNewUnit_list {l : List α} {k : α} :
(insertManyIfNewUnit t l)[k]! = () :=
rfl
@[simp]
theorem getD_insertManyIfNewUnit_list
{l : List α} {k : α} {fallback : Unit} :
getD (insertManyIfNewUnit t l) k fallback = () :=
rfl
end Std.TreeMap.Raw

119
src/Std/Data/TreeSet/Lemmas.lean
View file

@ -396,4 +396,123 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : α → δ → m (Fo
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} :
t.insertMany [k] = t.insert k :=
rfl
theorem insertMany_cons {l : List α} {k : α} :
t.insertMany (k :: l) = (t.insert k).insertMany l :=
ext TreeMap.insertManyIfNewUnit_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
(t.insertMany l).contains k = (t.contains k || l.contains k) :=
TreeMap.contains_insertManyIfNewUnit_list
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} :
k ∈ insertMany t l ↔ k ∈ t ∨ l.contains k :=
TreeMap.mem_insertManyIfNewUnit_list
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertMany t l → k ∈ t :=
TreeMap.mem_of_mem_insertManyIfNewUnit_list contains_eq_false
theorem get?_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
get? (insertMany t l) k = none :=
TreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem get?_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get? (insertMany t l) k' = some k :=
TreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem get?_insertMany_list_of_mem [TransCmp cmp]
{l : List α} {k : α} (mem : k ∈ t) :
get? (insertMany t l) k = get? t k :=
TreeMap.getKey?_insertManyIfNewUnit_list_of_mem mem
theorem get_insertMany_list_of_mem [TransCmp cmp]
{l : List α} {k : α} {h'} (contains : k ∈ t) :
get (insertMany t l) k h' = get t k contains :=
TreeMap.getKey_insertManyIfNewUnit_list_of_mem contains
theorem get_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} (not_mem : ¬ k ∈ t)
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get (insertMany t l) k' h' = k :=
TreeMap.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem get!_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
get! (insertMany t l) k = default :=
TreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem get!_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get! (insertMany t l) k' = k :=
TreeMap.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem get!_insertMany_list_of_mem [TransCmp cmp]
[Inhabited α] {l : List α} {k : α} (mem : k ∈ t):
get! (insertMany t l) k = get! t k :=
TreeMap.getKey!_insertManyIfNewUnit_list_of_mem mem
theorem getD_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k fallback : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getD (insertMany t l) k fallback = fallback :=
TreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
not_mem contains_eq_false
theorem getD_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
{l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getD (insertMany t l) k' fallback = k :=
TreeMap.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem k_eq not_mem distinct mem
theorem getD_insertMany_list_of_mem [TransCmp cmp]
{l : List α} {k fallback : α} (mem : k ∈ t) :
getD (insertMany t l) k fallback = getD t k fallback :=
TreeMap.getKeyD_insertManyIfNewUnit_list_of_mem mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp]
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertMany t l).size = t.size + l.length :=
TreeMap.size_insertManyIfNewUnit_list distinct
theorem size_le_size_insertMany_list [TransCmp cmp]
{l : List α} :
t.size ≤ (insertMany t l).size :=
TreeMap.size_le_size_insertManyIfNewUnit_list
theorem size_insertMany_list_le [TransCmp cmp]
{l : List α} :
(insertMany t l).size ≤ t.size + l.length :=
TreeMap.size_insertManyIfNewUnit_list_le
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp] {l : List α} :
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
TreeMap.isEmpty_insertManyIfNewUnit_list
end Std.TreeSet

119
src/Std/Data/TreeSet/Raw/Lemmas.lean
View file

@ -392,4 +392,123 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m]
end monadic
@[simp]
theorem insertMany_nil :
t.insertMany [] = t :=
rfl
@[simp]
theorem insertMany_list_singleton {k : α} :
t.insertMany [k] = t.insert k :=
rfl
theorem insertMany_cons {l : List α} {k : α} :
t.insertMany (k :: l) = (t.insert k).insertMany l :=
ext TreeMap.Raw.insertManyIfNewUnit_cons
@[simp]
theorem contains_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
(t.insertMany l).contains k = (t.contains k || l.contains k) :=
TreeMap.Raw.contains_insertManyIfNewUnit_list h
@[simp]
theorem mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} :
k ∈ insertMany t l ↔ k ∈ t ∨ l.contains k :=
TreeMap.Raw.mem_insertManyIfNewUnit_list h
theorem mem_of_mem_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α} {k : α} (contains_eq_false : l.contains k = false) :
k ∈ insertMany t l → k ∈ t :=
TreeMap.Raw.mem_of_mem_insertManyIfNewUnit_list h contains_eq_false
theorem get?_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
get? (insertMany t l) k = none :=
TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem get?_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get? (insertMany t l) k' = some k :=
TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem get?_insertMany_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} (mem : k ∈ t) :
get? (insertMany t l) k = get? t k :=
TreeMap.Raw.getKey?_insertManyIfNewUnit_list_of_mem h mem
theorem get_insertMany_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k : α} {h'} (contains : k ∈ t) :
get (insertMany t l) k h' = get t k contains :=
TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_mem h contains
theorem get_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α}
{k k' : α} (k_eq : cmp k k' = .eq) {h'} (not_mem : ¬ k ∈ t)
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get (insertMany t l) k' h' = k :=
TreeMap.Raw.getKey_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem get!_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] [Inhabited α] (h : t.WF) {l : List α} {k : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
get! (insertMany t l) k = default :=
TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem get!_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k k' : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
get! (insertMany t l) k' = k :=
TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem get!_insertMany_list_of_mem [TransCmp cmp]
[Inhabited α] (h : t.WF) {l : List α} {k : α} (mem : k ∈ t):
get! (insertMany t l) k = get! t k :=
TreeMap.Raw.getKey!_insertManyIfNewUnit_list_of_mem h mem
theorem getD_insertMany_list_of_not_mem_of_contains_eq_false
[TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF) {l : List α} {k fallback : α}
(not_mem : ¬ k ∈ t) (contains_eq_false : l.contains k = false) :
getD (insertMany t l) k fallback = fallback :=
TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false
h not_mem contains_eq_false
theorem getD_insertMany_list_of_not_mem_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k k' fallback : α} (k_eq : cmp k k' = .eq)
(not_mem : ¬ k ∈ t) (distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) (mem : k ∈ l) :
getD (insertMany t l) k' fallback = k :=
TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem h k_eq not_mem distinct mem
theorem getD_insertMany_list_of_mem [TransCmp cmp]
(h : t.WF) {l : List α} {k fallback : α} (mem : k ∈ t) :
getD (insertMany t l) k fallback = getD t k fallback :=
TreeMap.Raw.getKeyD_insertManyIfNewUnit_list_of_mem h mem
theorem size_insertMany_list [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] (h : t.WF)
{l : List α}
(distinct : l.Pairwise (fun a b => ¬ cmp a b = .eq)) :
(∀ (a : α), a ∈ t → l.contains a = false) →
(insertMany t l).size = t.size + l.length :=
TreeMap.Raw.size_insertManyIfNewUnit_list h distinct
theorem size_le_size_insertMany_list [TransCmp cmp] (h : t.WF)
{l : List α} :
t.size ≤ (insertMany t l).size :=
TreeMap.Raw.size_le_size_insertManyIfNewUnit_list h
theorem size_insertMany_list_le [TransCmp cmp] (h : t.WF)
{l : List α} :
(insertMany t l).size ≤ t.size + l.length :=
TreeMap.Raw.size_insertManyIfNewUnit_list_le h
@[simp]
theorem isEmpty_insertMany_list [TransCmp cmp] (h : t.WF) {l : List α} :
(insertMany t l).isEmpty = (t.isEmpty && l.isEmpty) :=
TreeMap.Raw.isEmpty_insertManyIfNewUnit_list h
end Std.TreeSet.Raw