From 0c898742f65dae82fb3ab5a3cdaab6c33d30dfcf Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Thu, 6 Mar 2025 09:54:42 +0100 Subject: [PATCH] feat: tree map lemmas for insertMany (#7331) 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> --- src/Std/Classes/Ord.lean | 32 + src/Std/Data/DTreeMap/Internal/Lemmas.lean | 1145 ++++++++++++++++- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 169 ++- src/Std/Data/DTreeMap/Lemmas.lean | 601 +++++++++ src/Std/Data/DTreeMap/Raw/Lemmas.lean | 603 ++++++++- src/Std/Data/HashMap/RawLemmas.lean | 2 +- src/Std/Data/Internal/List/Associative.lean | 60 +- src/Std/Data/TreeMap/Lemmas.lean | 312 +++++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 312 +++++ src/Std/Data/TreeSet/Lemmas.lean | 119 ++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 119 ++ 11 files changed, 3380 insertions(+), 94 deletions(-) diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean index aaa628605b..bc834079c2 100644 --- a/src/Std/Classes/Ord.lean +++ b/src/Std/Classes/Ord.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 42b0cfed14..4f6a957f57 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -38,6 +38,9 @@ scoped macro "wf_trivial" : tactic => `(tactic| | apply WF.insert | apply WF.insert! | apply WF.insertIfNew | apply WF.insertIfNew! | apply WF.erase | apply WF.erase! + | apply WF.insertMany | apply WF.insertMany! + | apply WF.constInsertMany | apply WF.constInsertMany! + | apply WF.constInsertManyIfNewUnit | apply WF.constInsertManyIfNewUnit! | apply Ordered.distinctKeys | assumption )) @@ -47,10 +50,8 @@ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] open Lean -theorem compare_eq_eq_iff_beq {k a : α} : compare k a = .eq ↔ k == a := beq_iff_eq.symm - private def helperLemmaNames : Array Name := - #[``compare_eq_eq_iff_beq] + #[``compare_eq_iff_beq, ``Bool.not_eq_true, `mem_iff_contains] private def queryNames : Array Name := #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length, @@ -72,7 +73,13 @@ private def modifyMap : Std.HashMap Name Name := ⟨`insertIfNew, ``toListModel_insertIfNew⟩, ⟨`insertIfNew!, ``toListModel_insertIfNew!⟩, ⟨`erase, ``toListModel_erase⟩, - ⟨`erase!, ``toListModel_erase!⟩] + ⟨`erase!, ``toListModel_erase!⟩, + (`insertMany, ``toListModel_insertMany_list), + (`insertMany!, ``toListModel_insertMany!_list), + (`Const.insertMany, ``Const.toListModel_insertMany_list), + (`Const.insertMany!, ``Const.toListModel_insertMany!_list), + (`Const.insertManyIfNewUnit, ``Const.toListModel_insertManyIfNewUnit_list), + (`Const.insertManyIfNewUnit!, ``Const.toListModel_insertManyIfNewUnit!_list)] private def congrNames : MacroM (Array (TSyntax `term)) := do return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm), @@ -103,6 +110,9 @@ macro_rules theorem isEmpty_empty : isEmpty (empty : Impl α β) := by simp [Impl.isEmpty_eq_isEmpty] +theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := + Iff.rfl + theorem isEmpty_insert [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.insert k v h.balanced).impl.isEmpty = false := by simp_to_model [insert] using List.isEmpty_insertEntry @@ -111,9 +121,6 @@ theorem isEmpty_insert! [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.insert! k v).isEmpty = false := by simp_to_model [insert!] using List.isEmpty_insertEntry -theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := - Iff.rfl - theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) : t.contains k = t.contains k' := by revert hab @@ -266,7 +273,7 @@ theorem mem_erase [TransOrd α] (h : t.WF) {k a : α} : using Bool.eq_iff_iff.mp <| contains_erase h theorem mem_erase! [TransOrd α] (h : t.WF) {k a : α} : - a ∈ t.erase! k ↔ compare k a ≠ .eq ∧ a ∈ t := by + a ∈ t.erase! k ↔ compare k a ≠ .eq ∧ a ∈ t := by simp [mem_iff_contains, contains_erase! h] theorem contains_of_contains_erase [TransOrd α] (h : t.WF) {k a : α} : @@ -404,12 +411,10 @@ theorem mem_of_mem_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} : theorem size_insertIfNew [TransOrd α] {k : α} (h : t.WF) {v : β k} : (t.insertIfNew k v h.balanced).impl.size = if k ∈ t then t.size else t.size + 1 := by - simp only [mem_iff_contains] simp_to_model [insertIfNew] using List.length_insertEntryIfNew theorem size_insertIfNew! [TransOrd α] {k : α} (h : t.WF) {v : β k} : (t.insertIfNew! k v).size = if k ∈ t then t.size else t.size + 1 := by - simp only [mem_iff_contains] simp_to_model [insertIfNew!] using List.length_insertEntryIfNew theorem size_le_size_insertIfNew [TransOrd α] (h : t.WF) {k : α} {v : β k} : @@ -1186,7 +1191,6 @@ theorem mem_of_mem_insertIfNew' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : a ∈ (t.insertIfNew k v h.balanced).impl → ¬ (compare k a = .eq ∧ ¬ k ∈ t) → a ∈ t := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.containsKey_of_containsKey_insertEntryIfNew' /-- This is a restatement of `contains_of_contains_insertIfNew!` that is written to exactly match the @@ -1194,7 +1198,6 @@ proof obligation in the statement of `get_insertIfNew!`. -/ theorem mem_of_mem_insertIfNew!' [TransOrd α] (h : t.WF) {k a : α} {v : β k} : a ∈ (t.insertIfNew! k v) → ¬ (compare k a = .eq ∧ ¬ k ∈ t) → a ∈ t := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.containsKey_of_containsKey_insertEntryIfNew' theorem get?_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} : @@ -1203,7 +1206,6 @@ theorem get?_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v) else t.get? a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValueCast?_insertEntryIfNew theorem get?_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} : @@ -1212,7 +1214,6 @@ theorem get?_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} { some (cast (congrArg β (compare_eq_iff_eq.mp h.1)) v) else t.get? a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValueCast?_insertEntryIfNew theorem get_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} : @@ -1221,7 +1222,6 @@ theorem get_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v else t.get a (mem_of_mem_insertIfNew' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValueCast_insertEntryIfNew theorem get_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} : @@ -1230,7 +1230,6 @@ theorem get_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {v cast (congrArg β (compare_eq_iff_eq.mp h₂.1)) v else t.get a (mem_of_mem_insertIfNew!' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValueCast_insertEntryIfNew theorem get!_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} : @@ -1239,7 +1238,6 @@ theorem get!_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [I cast (congrArg β (compare_eq_iff_eq.mp h.1)) v else t.get! a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValueCast!_insertEntryIfNew theorem get!_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [Inhabited (β a)] {v : β k} : @@ -1248,7 +1246,6 @@ theorem get!_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} [ cast (congrArg β (compare_eq_iff_eq.mp h.1)) v else t.get! a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValueCast!_insertEntryIfNew theorem getD_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} : @@ -1257,7 +1254,6 @@ theorem getD_insertIfNew [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {f cast (congrArg β (compare_eq_iff_eq.mp h.1)) v else t.getD a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValueCastD_insertEntryIfNew theorem getD_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} {fallback : β a} {v : β k} : @@ -1266,7 +1262,6 @@ theorem getD_insertIfNew! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} { cast (congrArg β (compare_eq_iff_eq.mp h.1)) v else t.getD a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValueCastD_insertEntryIfNew namespace Const @@ -1279,7 +1274,6 @@ theorem get?_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β} : some v else get? t a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValue?_insertEntryIfNew theorem get?_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} : @@ -1288,7 +1282,6 @@ theorem get?_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} : some v else get? t a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValue?_insertEntryIfNew theorem get_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} : @@ -1297,7 +1290,6 @@ theorem get_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} : v else get t a (mem_of_mem_insertIfNew' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValue_insertEntryIfNew theorem get_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} : @@ -1306,33 +1298,28 @@ theorem get_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β} {h₁} : v else get t a (mem_of_mem_insertIfNew!' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValue_insertEntryIfNew theorem get!_insertIfNew [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} {v : β} : get! (t.insertIfNew k v h.balanced).impl a = if compare k a = .eq ∧ ¬ k ∈ t then v else get! t a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValue!_insertEntryIfNew theorem get!_insertIfNew! [TransOrd α] [Inhabited β] (h : t.WF) {k a : α} {v : β} : get! (t.insertIfNew! k v) a = if compare k a = .eq ∧ ¬ k ∈ t then v else get! t a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValue!_insertEntryIfNew theorem getD_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} : getD (t.insertIfNew k v h.balanced).impl a fallback = if compare k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getValueD_insertEntryIfNew theorem getD_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {fallback v : β} : getD (t.insertIfNew! k v) a fallback = if compare k a = .eq ∧ ¬ k ∈ t then v else getD t a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getValueD_insertEntryIfNew end Const @@ -1340,55 +1327,47 @@ end Const theorem getKey?_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} : (t.insertIfNew k v h.balanced).impl.getKey? a = if compare k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getKey?_insertEntryIfNew theorem getKey?_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} : (t.insertIfNew! k v).getKey? a = if compare k a = .eq ∧ ¬ k ∈ t then some k else t.getKey? a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getKey?_insertEntryIfNew theorem getKey_insertIfNew [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} : (t.insertIfNew k v h.balanced).impl.getKey a h₁ = if h₂ : compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey a (mem_of_mem_insertIfNew' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getKey_insertEntryIfNew theorem getKey_insertIfNew! [TransOrd α] (h : t.WF) {k a : α} {v : β k} {h₁} : (t.insertIfNew! k v).getKey a h₁ = if h₂ : compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey a (mem_of_mem_insertIfNew!' h h₁ h₂) := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getKey_insertEntryIfNew theorem getKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) {k a : α} {v : β k} : (t.insertIfNew k v h.balanced).impl.getKey! a = if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getKey!_insertEntryIfNew theorem getKey!_insertIfNew! [TransOrd α] [Inhabited α] (h : t.WF) {k a : α} {v : β k} : (t.insertIfNew! k v).getKey! a = if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKey! a := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getKey!_insertEntryIfNew theorem getKeyD_insertIfNew [TransOrd α] (h : t.WF) {k a fallback : α} {v : β k} : (t.insertIfNew k v h.balanced).impl.getKeyD a fallback = if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew] using List.getKeyD_insertEntryIfNew theorem getKeyD_insertIfNew! [TransOrd α] (h : t.WF) {k a fallback : α} {v : β k} : (t.insertIfNew! k v).getKeyD a fallback = if compare k a = .eq ∧ ¬ k ∈ t then k else t.getKeyD a fallback := by - simp only [mem_iff_contains, Bool.not_eq_true] simp_to_model [insertIfNew!] using List.getKeyD_insertEntryIfNew /-! @@ -1474,13 +1453,12 @@ theorem length_keys [TransOrd α] (h : t.WF) : simp_to_model using List.length_keys_eq_length theorem isEmpty_keys : - t.keys.isEmpty = t.isEmpty := by + t.keys.isEmpty = t.isEmpty := by simp_to_model using List.isEmpty_keys_eq_isEmpty theorem contains_keys [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) : t.keys.contains k = t.contains k := by - rw [contains_eq_containsKey h.ordered, ← eq_beqOfOrd_of_lawfulBEqOrd] - simp_to_model using (List.containsKey_eq_keys_contains (a := k) (l := t.toListModel)).symm + simp_to_model using (List.containsKey_eq_keys_contains).symm theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) : k ∈ t.keys ↔ k ∈ t := by @@ -1488,7 +1466,6 @@ theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) : theorem distinct_keys [TransOrd α] (h : t.WF) : t.keys.Pairwise (fun a b => ¬ compare a b = .eq) := by - simp only [← not_congr beq_iff_eq, ← beq_eq, Bool.not_eq_true] simp_to_model using h.ordered.distinctKeys.distinct theorem map_fst_toList_eq_keys : @@ -1522,7 +1499,6 @@ theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : theorem distinct_keys_toList [TransOrd α] (h : t.WF) : t.toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by - simp only [← beq_iff, Bool.not_eq_true] simp_to_model using List.pairwise_fst_eq_false namespace Const @@ -1569,7 +1545,6 @@ theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : theorem distinct_keys_toList [TransOrd α] (h : t.WF) : (toList t).Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by - simp only [← beq_iff, Bool.not_eq_true] simp_to_model using List.pairwise_fst_eq_false_map_toProd end Const @@ -1665,4 +1640,1090 @@ end Const end monadic +theorem insertMany_cons (h : t.WF) {l : List ((a : α) × β a)} {k : α} {v : β k} : + (t.insertMany (⟨k, v⟩ :: l) h.balanced).1 = + ((t.insert k v h.balanced).impl.insertMany l h.insert.balanced).1 := by + simp [insertMany_eq_foldl, insert_eq_insert!] + +theorem insertMany!_cons {l : List ((a : α) × β a)} {k : α} {v : β k} : + (t.insertMany! (⟨k, v⟩ :: l)).1 = ((t.insert! k v).insertMany! l).1 := by + simp [insertMany!_eq_foldl] + +@[simp] +theorem contains_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + (t.insertMany l h.balanced).1.contains k = (t.contains k || (l.map Sigma.fst).contains k) := by + simp_to_model [insertMany] using List.containsKey_insertList + +@[simp] +theorem mem_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + k ∈ (t.insertMany l h.balanced).1 ↔ k ∈ t ∨ (l.map Sigma.fst).contains k := by + simp [mem_iff_contains, contains_insertMany_list h] + +@[simp] +theorem contains_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + (t.insertMany! l).1.contains k = (t.contains k || (l.map Sigma.fst).contains k) := by + simp_to_model [insertMany!] using List.containsKey_insertList + +@[simp] +theorem mem_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + k ∈ (t.insertMany! l).1 ↔ k ∈ t ∨ (l.map Sigma.fst).contains k := by + simp [mem_iff_contains, contains_insertMany!_list h] + +theorem contains_of_contains_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + (t.insertMany l h.balanced).1.contains k → + (l.map Sigma.fst).contains k = false → t.contains k := by + simp_to_model [insertMany] using List.containsKey_of_containsKey_insertList + +theorem mem_of_mem_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + k ∈ (t.insertMany l h.balanced).1 → (l.map Sigma.fst).contains k = false → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertMany_list h + +theorem contains_of_contains_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + (t.insertMany! l).1.contains k → (l.map Sigma.fst).contains k = false → t.contains k := by + simp_to_model [insertMany!] using List.containsKey_of_containsKey_insertList + +theorem mem_of_mem_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} : + k ∈ (t.insertMany! l).1 → (l.map Sigma.fst).contains k = false → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertMany!_list h + +theorem get?_insertMany_list_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] [BEq α] + [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.get? k = t.get? k := by + simp_to_model [insertMany] using List.getValueCast?_insertList_of_contains_eq_false + +theorem get?_insertMany!_list_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] [BEq α] + [LawfulBEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.get? k = t.get? k := by + simp_to_model [insertMany!] using List.getValueCast?_insertList_of_contains_eq_false + +theorem get?_insertMany_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany l h.balanced).1.get? k' = + some (cast (by congr; apply compare_eq_iff_eq.mp k_beq) v) := by + simp_to_model [insertMany] using List.getValueCast?_insertList_of_mem + +theorem get?_insertMany!_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany! l).1.get? k' = some (cast (by congr; apply compare_eq_iff_eq.mp k_beq) v) := by + simp_to_model [insertMany!] using List.getValueCast?_insertList_of_mem + +theorem get_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} + (contains : (l.map Sigma.fst).contains k = false) + {h'} : + (t.insertMany l h.balanced).1.get k h' = + t.get k (contains_of_contains_insertMany_list h h' contains) := by + simp_to_model [insertMany] using List.getValueCast_insertList_of_contains_eq_false + +theorem get_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} + (contains : (l.map Sigma.fst).contains k = false) + {h'} : + (t.insertMany! l).1.get k h' = + t.get k (contains_of_contains_insertMany!_list h h' contains) := by + simp_to_model [insertMany!] using List.getValueCast_insertList_of_contains_eq_false + +theorem get_insertMany_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + {h' : _} → + (t.insertMany l h.balanced).1.get k' h' = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany] using List.getValueCast_insertList_of_mem + +theorem get_insertMany!_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + {h' : _} → + (t.insertMany! l).1.get k' h' = cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany!] using List.getValueCast_insertList_of_mem + +theorem get!_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.get! k = t.get! k := by + simp_to_model [insertMany] using List.getValueCast!_insertList_of_contains_eq_false + +theorem get!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.get! k = t.get! k := by + simp_to_model [insertMany!] using List.getValueCast!_insertList_of_contains_eq_false + +theorem get!_insertMany_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + [Inhabited (β k')] → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany l h.balanced).1.get! k' = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany] using List.getValueCast!_insertList_of_mem + +theorem get!_insertMany!_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + [Inhabited (β k')] → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany! l).1.get! k' = cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany!] using List.getValueCast!_insertList_of_mem + +theorem getD_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} + (contains_eq_false : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.getD k fallback = t.getD k fallback := by + simp_to_model [insertMany] using List.getValueCastD_insertList_of_contains_eq_false + +theorem getD_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} {fallback : β k} + (contains_eq_false : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.getD k fallback = t.getD k fallback := by + simp_to_model [insertMany!] using List.getValueCastD_insertList_of_contains_eq_false + +theorem getD_insertMany_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + {fallback : β k'} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany l h.balanced).1.getD k' fallback = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany] using List.getValueCastD_insertList_of_mem + +theorem getD_insertMany!_list_of_mem [TransOrd α] [LawfulEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β k} → + {fallback : β k'} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : ⟨k, v⟩ ∈ l) → + (t.insertMany! l).1.getD k' fallback = cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + simp_to_model [insertMany!] using List.getValueCastD_insertList_of_mem + +theorem getKey?_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.getKey? k = t.getKey? k := by + simp_to_model [insertMany] using List.getKey?_insertList_of_contains_eq_false + +theorem getKey?_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.getKey? k = t.getKey? k := by + simp_to_model [insertMany!] using List.getKey?_insertList_of_contains_eq_false + +theorem getKey?_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany l h.balanced).1.getKey? k' = some k := by + simp_to_model [insertMany] using List.getKey?_insertList_of_mem + +theorem getKey?_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany! l).1.getKey? k' = some k := by + simp_to_model [insertMany!] using List.getKey?_insertList_of_mem + +theorem getKey_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} {k : α} + (h₁ : (l.map Sigma.fst).contains k = false) + {h'} : + (t.insertMany l h.balanced).1.getKey k h' = + t.getKey k (contains_of_contains_insertMany_list h h' h₁) := by + simp_to_model [insertMany] using List.getKey_insertList_of_contains_eq_false + +theorem getKey_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h₁ : (l.map Sigma.fst).contains k = false) + {h'} : + (t.insertMany! l).1.getKey k h' = + t.getKey k (contains_of_contains_insertMany!_list h h' h₁) := by + simp_to_model [insertMany!] using List.getKey_insertList_of_contains_eq_false + +theorem getKey_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + {h' : _} → + (t.insertMany l h.balanced).1.getKey k' h' = k := by + simp_to_model [insertMany] using List.getKey_insertList_of_mem + +theorem getKey_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + {h' : _} → + (t.insertMany! l).1.getKey k' h' = k := by + simp_to_model [insertMany!] using List.getKey_insertList_of_mem + +theorem getKey!_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.getKey! k = t.getKey! k := by + simp_to_model [insertMany] using List.getKey!_insertList_of_contains_eq_false + +theorem getKey!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited α] (h : t.WF) {l : List ((a : α) × β a)} {k : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.getKey! k = t.getKey! k := by + simp_to_model [insertMany!] using List.getKey!_insertList_of_contains_eq_false + +theorem getKey!_insertMany_list_of_mem [TransOrd α] [Inhabited α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany l h.balanced).1.getKey! k' = k := by + simp_to_model [insertMany] using List.getKey!_insertList_of_mem + +theorem getKey!_insertMany!_list_of_mem [TransOrd α] [Inhabited α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany! l).1.getKey! k' = k := by + simp_to_model [insertMany!] using List.getKey!_insertList_of_mem + +theorem getKeyD_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List ((a : α) × β a)} {k fallback : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany l h.balanced).1.getKeyD k fallback = t.getKeyD k fallback := by + simp_to_model [insertMany] using List.getKeyD_insertList_of_contains_eq_false + +theorem getKeyD_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List ((a : α) × β a)} {k fallback : α} + (h' : (l.map Sigma.fst).contains k = false) : + (t.insertMany! l).1.getKeyD k fallback = t.getKeyD k fallback := by + simp_to_model [insertMany!] using List.getKeyD_insertList_of_contains_eq_false + +theorem getKeyD_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' fallback : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany l h.balanced).1.getKeyD k' fallback = k := by + simp_to_model [insertMany] using List.getKeyD_insertList_of_mem + +theorem getKeyD_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} + {k k' fallback : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Sigma.fst) → + (t.insertMany! l).1.getKeyD k' fallback = k := by + simp_to_model [insertMany!] using List.getKeyD_insertList_of_mem + +theorem size_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (∀ (a : α), t.contains a → (l.map Sigma.fst).contains a = false) → + (t.insertMany l h.balanced).1.size = t.size + l.length := by + simp_to_model [insertMany] using List.length_insertList + +theorem size_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (∀ (a : α), t.contains a → (l.map Sigma.fst).contains a = false) → + (t.insertMany! l).1.size = t.size + l.length := by + simp_to_model [insertMany!] using List.length_insertList + +theorem size_le_size_insertMany_list [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + t.size ≤ (t.insertMany l h.balanced).1.size := by + simp_to_model [insertMany] using List.length_le_length_insertList + +theorem size_le_size_insertMany!_list [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + t.size ≤ (t.insertMany! l).1.size := by + simp_to_model [insertMany!] using List.length_le_length_insertList + +theorem size_insertMany_list_le [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + (t.insertMany l h.balanced).1.size ≤ t.size + l.length := by + simp_to_model [insertMany] using List.length_insertList_le + +theorem size_insertMany!_list_le [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + (t.insertMany! l).1.size ≤ t.size + l.length := by + simp_to_model [insertMany!] using List.length_insertList_le + +@[simp] +theorem isEmpty_insertMany_list [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + (t.insertMany l h.balanced).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [insertMany] using List.isEmpty_insertList + +@[simp] +theorem isEmpty_insertMany!_list [TransOrd α] (h : t.WF) + {l : List ((a : α) × β a)} : + (t.insertMany! l).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [insertMany!] using List.isEmpty_insertList + +namespace Const + +variable {β : Type v} {t : Impl α β} + +theorem insertMany_cons (h : t.WF) {l : List (α × β)} {k : α} {v : β} : + (Const.insertMany t ((k, v) :: l) h.balanced).1 = + (Const.insertMany (t.insert k v h.balanced).impl l h.insert.balanced).1 := by + simp [insertMany_eq_foldl, insert_eq_insert!] + +theorem insertMany!_cons {l : List (α × β)} {k : α} {v : β} : + (Const.insertMany! t ((k, v) :: l)).1 = (Const.insertMany! (t.insert! k v) l).1 := by + simp [insertMany!_eq_foldl] + +@[simp] +theorem contains_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + (Const.insertMany t l h.balanced).1.contains k = + (t.contains k || (l.map Prod.fst).contains k) := by + simp_to_model [Const.insertMany] using List.containsKey_insertListConst + +@[simp] +theorem contains_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + (Const.insertMany! t l).1.contains k = (t.contains k || (l.map Prod.fst).contains k) := by + simp_to_model [Const.insertMany!] using List.containsKey_insertListConst + +@[simp] +theorem mem_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + k ∈ (insertMany t l h.balanced).1 ↔ k ∈ t ∨ (l.map Prod.fst).contains k := by + simp [mem_iff_contains, contains_insertMany_list h] + +@[simp] +theorem mem_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + k ∈ (insertMany! t l).1 ↔ k ∈ t ∨ (l.map Prod.fst).contains k := by + simp [mem_iff_contains, contains_insertMany!_list h] + +theorem contains_of_contains_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + (insertMany t l h.balanced).1.contains k → + (l.map Prod.fst).contains k = false → t.contains k := by + simp_to_model [Const.insertMany] using List.containsKey_of_containsKey_insertListConst + +theorem mem_of_mem_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + k ∈ (insertMany t l h.balanced).1 → (l.map Prod.fst).contains k = false → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertMany_list h + +theorem contains_of_contains_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List ( α × β )} {k : α} : + (insertMany! t l).1.contains k → (l.map Prod.fst).contains k = false → t.contains k := by + simp_to_model [Const.insertMany!] using List.containsKey_of_containsKey_insertListConst + +theorem mem_of_mem_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} : + k ∈ (insertMany! t l).1 → (l.map Prod.fst).contains k = false → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertMany!_list h + +theorem getKey?_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany t l h.balanced).1.getKey? k = t.getKey? k := by + simp_to_model [Const.insertMany] using List.getKey?_insertListConst_of_contains_eq_false + +theorem getKey?_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany! t l).1.getKey? k = t.getKey? k := by + simp_to_model [Const.insertMany!] using List.getKey?_insertListConst_of_contains_eq_false + +theorem getKey?_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany t l h.balanced).1.getKey? k' = some k := by + simp_to_model [Const.insertMany] using List.getKey?_insertListConst_of_mem + +theorem getKey?_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany! t l).1.getKey? k' = some k := by + simp_to_model [Const.insertMany!] using List.getKey?_insertListConst_of_mem + +theorem getKey_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} + (h₁ : (l.map Prod.fst).contains k = false) + {h'} : + (insertMany t l h.balanced).1.getKey k h' = + t.getKey k (contains_of_contains_insertMany_list h h' h₁) := by + simp_to_model [Const.insertMany] using List.getKey_insertListConst_of_contains_eq_false + +theorem getKey_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List (α × β)} {k : α} + (h₁ : (l.map Prod.fst).contains k = false) + {h'} : + (insertMany! t l).1.getKey k h' = + t.getKey k (contains_of_contains_insertMany!_list h h' h₁) := by + simp_to_model [Const.insertMany!] using List.getKey_insertListConst_of_contains_eq_false + +theorem getKey_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + {h' : _} → + (insertMany t l h.balanced).1.getKey k' h' = k := by + simp_to_model [Const.insertMany] using List.getKey_insertListConst_of_mem + +theorem getKey_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + {h' : _} → + (insertMany! t l).1.getKey k' h' = k := by + simp_to_model [Const.insertMany!] using List.getKey_insertListConst_of_mem + +theorem getKey!_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited α] (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany t l h.balanced).1.getKey! k = t.getKey! k := by + simp_to_model [Const.insertMany] using List.getKey!_insertListConst_of_contains_eq_false + +theorem getKey!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited α] (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany! t l).1.getKey! k = t.getKey! k := by + simp_to_model [Const.insertMany!] using List.getKey!_insertListConst_of_contains_eq_false + +theorem getKey!_insertMany_list_of_mem [TransOrd α] [Inhabited α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany t l h.balanced).1.getKey! k' = k := by + simp_to_model [Const.insertMany] using List.getKey!_insertListConst_of_mem + +theorem getKey!_insertMany!_list_of_mem [TransOrd α] [Inhabited α] (h : t.WF) + {l : List (α × β)} + {k k' : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany! t l).1.getKey! k' = k := by + simp_to_model [Const.insertMany!] using List.getKey!_insertListConst_of_mem + +theorem getKeyD_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List (α × β)} {k fallback : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany t l h.balanced).1.getKeyD k fallback = t.getKeyD k fallback := by + simp_to_model [Const.insertMany] using List.getKeyD_insertListConst_of_contains_eq_false + +theorem getKeyD_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List (α × β)} {k fallback : α} + (h' : (l.map Prod.fst).contains k = false) : + (insertMany! t l).1.getKeyD k fallback = t.getKeyD k fallback := by + simp_to_model [Const.insertMany!] using List.getKeyD_insertListConst_of_contains_eq_false + +theorem getKeyD_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' fallback : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany t l h.balanced).1.getKeyD k' fallback = k := by + simp_to_model [Const.insertMany] using List.getKeyD_insertListConst_of_mem + +theorem getKeyD_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} + {k k' fallback : α} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (mem : k ∈ l.map Prod.fst) → + (insertMany! t l).1.getKeyD k' fallback = k := by + simp_to_model [Const.insertMany!] using List.getKeyD_insertListConst_of_mem + +theorem size_insertMany_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} : + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (∀ (a : α), t.contains a → (l.map Prod.fst).contains a = false) → + (insertMany t l h.balanced).1.size = t.size + l.length := by + simp_to_model [Const.insertMany] using List.length_insertListConst + +theorem size_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} : + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → + (∀ (a : α), t.contains a → (l.map Prod.fst).contains a = false) → + (insertMany! t l).1.size = t.size + l.length := by + simp_to_model [Const.insertMany!] using List.length_insertListConst + +theorem size_le_size_insertMany_list [TransOrd α] (h : t.WF) + {l : List (α × β)} : + t.size ≤ (insertMany t l h.balanced).1.size := by + simp_to_model [Const.insertMany] using List.length_le_length_insertListConst + +theorem size_le_size_insertMany!_list [TransOrd α] (h : t.WF) + {l : List (α × β)} : + t.size ≤ (insertMany! t l).1.size := by + simp_to_model [Const.insertMany!] using List.length_le_length_insertListConst + +theorem size_insertMany_list_le [TransOrd α] (h : t.WF) + {l : List (α × β)} : + (insertMany t l h.balanced).1.size ≤ t.size + l.length := by + simp_to_model [Const.insertMany] using List.length_insertListConst_le + +theorem size_insertMany!_list_le [TransOrd α] (h : t.WF) + {l : List (α × β)} : + (insertMany! t l).1.size ≤ t.size + l.length := by + simp_to_model [Const.insertMany!] using List.length_insertListConst_le + +@[simp] +theorem isEmpty_insertMany_list [TransOrd α] (h : t.WF) + {l : List (α × β)} : + (insertMany t l h.balanced).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [Const.insertMany] using List.isEmpty_insertListConst + +@[simp] +theorem isEmpty_insertMany!_list [TransOrd α] (h : t.WF) + {l : List (α × β)} : + (insertMany! t l).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [Const.insertMany!] using List.isEmpty_insertListConst + +theorem get?_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + get? (insertMany t l h.balanced).1 k = get? t k := by + simp_to_model [Const.insertMany] using List.getValue?_insertListConst_of_contains_eq_false + +theorem get?_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + get? (insertMany! t l).1 k = get? t k := by + simp_to_model [Const.insertMany!] using List.getValue?_insertListConst_of_contains_eq_false + +theorem get?_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + get? (insertMany t l h.balanced).1 k' = v := by + simp_to_model [Const.insertMany] using List.getValue?_insertListConst_of_mem + +theorem get?_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + get? (insertMany! t l).1 k' = v := by + simp_to_model [Const.insertMany!] using List.getValue?_insertListConst_of_mem + +theorem get_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} + (h₁ : (l.map Prod.fst).contains k = false) + {h'} : + get (insertMany t l h.balanced).1 k h' = + get t k (contains_of_contains_insertMany_list h h' h₁) := by + simp_to_model [Const.insertMany] using List.getValue_insertListConst_of_contains_eq_false + +theorem get_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} + (h₁ : (l.map Prod.fst).contains k = false) + {h'} : + get (insertMany! t l).1 k h' = get t k (contains_of_contains_insertMany!_list h h' h₁) := by + simp_to_model [Const.insertMany!] using List.getValue_insertListConst_of_contains_eq_false + +theorem get_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → {h' : _} → + get (insertMany t l h.balanced).1 k' h' = v := by + simp_to_model [Const.insertMany] using List.getValue_insertListConst_of_mem + +theorem get_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} : (k_beq : compare k k' = .eq) → {v : β} → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → {h' : _} → + get (insertMany! t l).1 k' h' = v := by + simp_to_model [Const.insertMany!] using List.getValue_insertListConst_of_mem + +theorem get!_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + get! (insertMany t l h.balanced).1 k = get! t k := by + simp_to_model [Const.insertMany] using List.getValue!_insertListConst_of_contains_eq_false + +theorem get!_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited β] (h : t.WF) {l : List (α × β)} {k : α} + (h' : (l.map Prod.fst).contains k = false) : + get! (insertMany! t l).1 k = get! t k := by + simp_to_model [Const.insertMany!] using List.getValue!_insertListConst_of_contains_eq_false + +theorem get!_insertMany_list_of_mem [TransOrd α] [Inhabited β] (h : t.WF) + {l : List (α × β)} {k k' : α} {v : β} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + get! (insertMany t l h.balanced).1 k' = v := by + simp_to_model [Const.insertMany] using List.getValue!_insertListConst_of_mem + +theorem get!_insertMany!_list_of_mem [TransOrd α] [Inhabited β] (h : t.WF) + {l : List (α × β)} {k k' : α} {v : β} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + get! (insertMany! t l).1 k' = v := by + simp_to_model [Const.insertMany!] using List.getValue!_insertListConst_of_mem + +theorem getD_insertMany_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} {fallback : β} + (h' : (l.map Prod.fst).contains k = false) : + getD (insertMany t l h.balanced).1 k fallback = getD t k fallback := by + simp_to_model [Const.insertMany] using List.getValueD_insertListConst_of_contains_eq_false + +theorem getD_insertMany!_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List (α × β)} {k : α} {fallback : β} + (h' : (l.map Prod.fst).contains k = false) : + getD (insertMany! t l).1 k fallback = getD t k fallback := by + simp_to_model [Const.insertMany!] using List.getValueD_insertListConst_of_contains_eq_false + +theorem getD_insertMany_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} {v fallback : β} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + getD (insertMany t l h.balanced).1 k' fallback = v := by + simp_to_model [Const.insertMany] using List.getValueD_insertListConst_of_mem + +theorem getD_insertMany!_list_of_mem [TransOrd α] (h : t.WF) + {l : List (α × β)} {k k' : α} {v fallback : β} : (k_beq : compare k k' = .eq) → + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) → (mem : ⟨k, v⟩ ∈ l) → + getD (insertMany! t l).1 k' fallback = v := by + simp_to_model [Const.insertMany!] using List.getValueD_insertListConst_of_mem + +variable {t : Impl α Unit} + +theorem insertManyIfNewUnit_cons (h : t.WF) {l : List α} {k : α} : + (insertManyIfNewUnit t (k :: l) h.balanced).1 = + (insertManyIfNewUnit (t.insertIfNew k () h.balanced).impl l h.insertIfNew.balanced).1 := by + simp [insertManyIfNewUnit_eq_foldl, insertIfNew_eq_insertIfNew!] + +theorem insertManyIfNewUnit!_cons {l : List α} {k : α} : + (insertManyIfNewUnit! t (k :: l)).1 = (insertManyIfNewUnit! (t.insertIfNew! k ()) l).1 := by + simp [insertManyIfNewUnit!_eq_foldl] + +@[simp] +theorem contains_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + (insertManyIfNewUnit t l h.balanced).1.contains k = (t.contains k || l.contains k) := by + simp_to_model [Const.insertManyIfNewUnit] using List.containsKey_insertListIfNewUnit + +@[simp] +theorem contains_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + (insertManyIfNewUnit! t l).1.contains k = (t.contains k || l.contains k) := by + simp_to_model [Const.insertManyIfNewUnit!] using List.containsKey_insertListIfNewUnit + +@[simp] +theorem mem_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + k ∈ (insertManyIfNewUnit t l h.balanced).1 ↔ k ∈ t ∨ l.contains k := by + simp [mem_iff_contains, contains_insertManyIfNewUnit_list h] + +@[simp] +theorem mem_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + k ∈ (insertManyIfNewUnit! t l).1 ↔ k ∈ t ∨ l.contains k := by + simp [mem_iff_contains, contains_insertManyIfNewUnit!_list h] + +theorem contains_of_contains_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List α} {k : α} (h₂ : l.contains k = false) : + (insertManyIfNewUnit t l h.balanced).1.contains k → t.contains k := by + simp_to_model [Const.insertManyIfNewUnit] using List.containsKey_of_containsKey_insertListIfNewUnit + +theorem contains_of_contains_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] + (h : t.WF) {l : List α} {k : α} (h₂ : l.contains k = false) : + (insertManyIfNewUnit! t l).1.contains k → t.contains k := by + simp_to_model [Const.insertManyIfNewUnit!] using List.containsKey_of_containsKey_insertListIfNewUnit + +theorem mem_of_mem_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} (contains_eq_false : l.contains k = false) : + k ∈ (insertManyIfNewUnit t l h.balanced).1 → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertManyIfNewUnit_list h contains_eq_false + +theorem mem_of_mem_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} (contains_eq_false : l.contains k = false) : + k ∈ (insertManyIfNewUnit! t l).1 → k ∈ t := by + simpa [mem_iff_contains] using contains_of_contains_insertManyIfNewUnit!_list h contains_eq_false + +theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false [TransOrd α] [BEq α] + [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} : + ¬ k ∈ t → l.contains k = false → getKey? (insertManyIfNewUnit t l h.balanced).1 k = none := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKey?_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false [TransOrd α] [BEq α] + [LawfulBEqOrd α] (h : t.WF) {l : List α} {k : α} : + ¬ k ∈ t → l.contains k = false → getKey? (insertManyIfNewUnit! t l).1 k = none := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k k' : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey? (insertManyIfNewUnit t l h.balanced).1 k' = some k := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey?_insertManyIfNewUnit!_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k k' : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey? (insertManyIfNewUnit! t l).1 k' = some k := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey?_insertManyIfNewUnit_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} : + k ∈ t → getKey? (insertManyIfNewUnit t l h.balanced).1 k = getKey? t k := by + simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains + +theorem getKey?_insertManyIfNewUnit!_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} : + k ∈ t → getKey? (insertManyIfNewUnit! t l).1 k = getKey? t k := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getKey?_insertListIfNewUnit_of_contains + +theorem getKey_insertManyIfNewUnit_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} {h'} (contains : k ∈ t) : + getKey (insertManyIfNewUnit t l h.balanced).1 k h' = getKey t k contains := by + simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains + +theorem getKey_insertManyIfNewUnit!_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} {h'} (contains : k ∈ t) : + getKey (insertManyIfNewUnit! t l).1 k h' = getKey t k contains := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getKey_insertListIfNewUnit_of_contains + +theorem getKey_insertManyIfNewUnit_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} + {k k' : α} : (k_beq : compare k k' = .eq) → {h' : _} → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey (insertManyIfNewUnit t l h.balanced).1 k' h' = k := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey_insertManyIfNewUnit!_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} + {k k' : α} : (k_beq : compare k k' = .eq) → {h' : _} → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey (insertManyIfNewUnit! t l).1 k' h' = k := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKey_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey_insertManyIfNewUnit_list_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} (contains : k ∈ t) {h'} : + getKey (insertManyIfNewUnit t l h.balanced).1 k h' = getKey t k contains := by + simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains + +theorem getKey_insertManyIfNewUnit!_list_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k : α} (contains : k ∈ t) {h'} : + getKey (insertManyIfNewUnit! t l).1 k h' = getKey t k contains := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getKey_insertListIfNewUnit_of_contains + +theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false [BEq α] [LawfulBEqOrd α] + [TransOrd α] [Inhabited α] (h : t.WF) {l : List α} {k : α} : + ¬ k ∈ t → l.contains k = false → + getKey! (insertManyIfNewUnit t l h.balanced).1 k = default := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKey!_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false [BEq α] [LawfulBEqOrd α] + [TransOrd α] [Inhabited α] (h : t.WF) {l : List α} {k : α} : + ¬ k ∈ t → l.contains k = false → + getKey! (insertManyIfNewUnit! t l).1 k = default := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKey!_insertManyIfNewUnit_list_of_not_mem_of_mem [TransOrd α] + [Inhabited α] (h : t.WF) {l : List α} {k k' : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey! (insertManyIfNewUnit t l h.balanced).1 k' = k := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey!_insertManyIfNewUnit!_list_of_not_mem_of_mem [TransOrd α] + [Inhabited α] (h : t.WF) {l : List α} {k k' : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKey! (insertManyIfNewUnit! t l).1 k' = k := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKey!_insertManyIfNewUnit_list_of_mem [TransOrd α] + [Inhabited α] (h : t.WF) {l : List α} {k : α} : + k ∈ t → getKey! (insertManyIfNewUnit t l h.balanced).1 k = getKey! t k := by + simp_to_model [Const.insertManyIfNewUnit] using List.getKey!_insertListIfNewUnit_of_contains + +theorem getKey!_insertManyIfNewUnit!_list_of_mem [TransOrd α] + [Inhabited α] (h : t.WF) {l : List α} {k : α} : + k ∈ t → getKey! (insertManyIfNewUnit! t l).1 k = getKey! t k := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getKey!_insertListIfNewUnit_of_contains + +theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false [BEq α] [LawfulBEqOrd α] + [TransOrd α] (h : t.WF) {l : List α} {k fallback : α} : + ¬ k ∈ t → l.contains k = false → getKeyD (insertManyIfNewUnit t l h.balanced).1 k fallback = fallback := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_contains_eq_false [BEq α] [LawfulBEqOrd α] + [TransOrd α] (h : t.WF) {l : List α} {k fallback : α} : + ¬ k ∈ t → l.contains k = false → getKeyD (insertManyIfNewUnit! t l).1 k fallback = fallback := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false + +theorem getKeyD_insertManyIfNewUnit_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k k' fallback : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKeyD (insertManyIfNewUnit t l h.balanced).1 k' fallback = k := by + simp_to_model [Const.insertManyIfNewUnit] using + List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKeyD_insertManyIfNewUnit!_list_of_not_mem_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k k' fallback : α} : (k_beq : compare k k' = .eq) → + ¬ k ∈ t → l.Pairwise (fun a b => ¬ compare a b = .eq) → k ∈ l → + getKeyD (insertManyIfNewUnit! t l).1 k' fallback = k := by + simp_to_model [Const.insertManyIfNewUnit!] using + List.getKeyD_insertListIfNewUnit_of_contains_eq_false_of_mem + +theorem getKeyD_insertManyIfNewUnit_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k fallback : α} : + k ∈ t → getKeyD (insertManyIfNewUnit t l h.balanced).1 k fallback = getKeyD t k fallback := by + simp_to_model [Const.insertManyIfNewUnit] using List.getKeyD_insertListIfNewUnit_of_contains + +theorem getKeyD_insertManyIfNewUnit!_list_of_mem [TransOrd α] + (h : t.WF) {l : List α} {k fallback : α} : + k ∈ t → getKeyD (insertManyIfNewUnit! t l).1 k fallback = getKeyD t k fallback := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getKeyD_insertListIfNewUnit_of_contains + +theorem size_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} : + (distinct : l.Pairwise (fun a b => ¬ compare a b = .eq)) → + (∀ (a : α), a ∈ t → l.contains a = false) → + (insertManyIfNewUnit t l h.balanced).1.size = t.size + l.length := by + simp_to_model [Const.insertManyIfNewUnit] using List.length_insertListIfNewUnit + +theorem size_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} : + (distinct : l.Pairwise (fun a b => ¬ compare a b = .eq)) → + (∀ (a : α), a ∈ t → l.contains a = false) → + (insertManyIfNewUnit! t l).1.size = t.size + l.length := by + simp_to_model [Const.insertManyIfNewUnit!] using List.length_insertListIfNewUnit + +theorem size_le_size_insertManyIfNewUnit_list [TransOrd α] (h : t.WF) + {l : List α} : + t.size ≤ (insertManyIfNewUnit t l h.balanced).1.size := by + simp_to_model [Const.insertManyIfNewUnit] using List.length_le_length_insertListIfNewUnit + +theorem size_le_size_insertManyIfNewUnit!_list [TransOrd α] (h : t.WF) + {l : List α} : + t.size ≤ (insertManyIfNewUnit! t l).1.size := by + simp_to_model [Const.insertManyIfNewUnit!] using List.length_le_length_insertListIfNewUnit + +theorem size_insertManyIfNewUnit_list_le [TransOrd α] (h : t.WF) + {l : List α} : + (insertManyIfNewUnit t l h.balanced).1.size ≤ t.size + l.length := by + simp_to_model [Const.insertManyIfNewUnit] using List.length_insertListIfNewUnit_le + +theorem size_insertManyIfNewUnit!_list_le [TransOrd α] (h : t.WF) + {l : List α} : + (insertManyIfNewUnit! t l).1.size ≤ t.size + l.length := by + simp_to_model [Const.insertManyIfNewUnit!] using List.length_insertListIfNewUnit_le + +@[simp] +theorem isEmpty_insertManyIfNewUnit_list [TransOrd α] (h : t.WF) {l : List α} : + (insertManyIfNewUnit t l h.balanced).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [Const.insertManyIfNewUnit] using List.isEmpty_insertListIfNewUnit + +@[simp] +theorem isEmpty_insertManyIfNewUnit!_list [TransOrd α] (h : t.WF) {l : List α} : + (insertManyIfNewUnit! t l).1.isEmpty = (t.isEmpty && l.isEmpty) := by + simp_to_model [Const.insertManyIfNewUnit!] using List.isEmpty_insertListIfNewUnit + +theorem get?_insertManyIfNewUnit_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + get? (insertManyIfNewUnit t l h.balanced).1 k = + if k ∈ t ∨ l.contains k then some () else none := by + simp_to_model [Const.insertManyIfNewUnit] using List.getValue?_insertListIfNewUnit + +theorem get?_insertManyIfNewUnit!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] (h : t.WF) + {l : List α} {k : α} : + get? (insertManyIfNewUnit! t l).1 k = if k ∈ t ∨ l.contains k then some () else none := by + simp_to_model [Const.insertManyIfNewUnit!] using List.getValue?_insertListIfNewUnit + +theorem get_insertManyIfNewUnit_list (h : t.WF) {l : List α} {k : α} {h'} : + get (insertManyIfNewUnit t l h.balanced).1 k h' = () := + rfl + +theorem get_insertManyIfNewUnit!_list {l : List α} {k : α} {h'} : + get (insertManyIfNewUnit! t l).1 k h' = () := + rfl + +theorem get!_insertManyIfNewUnit_list (h : t.WF) {l : List α} {k : α} : + get! (insertManyIfNewUnit t l h.balanced).1 k = () := + rfl + +theorem get!_insertManyIfNewUnit!_list {l : List α} {k : α} : + get! (insertManyIfNewUnit! t l).1 k = () := + rfl + +theorem getD_insertManyIfNewUnit_list (h : t.WF) {l : List α} {k : α} {fallback : Unit} : + getD (insertManyIfNewUnit t l h.balanced).1 k fallback = () := + rfl + +theorem getD_insertManyIfNewUnit!_list + {l : List α} {k : α} {fallback : Unit} : + getD (insertManyIfNewUnit! t l).1 k fallback = () := + rfl + +end Const + +@[simp] +theorem insertMany_empty_list_nil : + (insertMany empty ([] : List ((a : α) × (β a))) WF.empty.balanced).1 = empty := + rfl + +@[simp] +theorem insertMany!_empty_list_nil : + (insertMany! empty ([] : List ((a : α) × (β a)))).1 = empty := + rfl + +@[simp] +theorem insertMany_empty_list_singleton {k : α} {v : β k} : + (insertMany empty [⟨k, v⟩] WF.empty.balanced).1 = (empty.insert k v WF.empty.balanced).impl := + rfl + +@[simp] +theorem insertMany!_empty_list_singleton {k : α} {v : β k} : + (insertMany! empty [⟨k, v⟩]).1 = (empty.insert k v WF.empty.balanced).impl := + rfl + +theorem insertMany_empty_list_cons {k : α} {v : β k} + {tl : List ((a : α) × (β a))} : + (insertMany empty (⟨k, v⟩ :: tl) WF.empty.balanced).1 = + ((empty.insert k v WF.empty.balanced).impl.insertMany tl WF.empty.insert.balanced).1 := by + rw [insertMany_cons WF.empty] + +theorem insertMany_empty_list_cons_eq_insertMany! {k : α} {v : β k} + {tl : List ((a : α) × (β a))} : + (insertMany empty (⟨k, v⟩ :: tl) WF.empty.balanced).1 = + ((empty.insert! k v).insertMany! tl).1 := by + rw [insertMany_cons WF.empty, insertMany_eq_insertMany!, insert_eq_insert!] + +theorem contains_insertMany_empty_list [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} {k : α} : + (insertMany empty l WF.empty.balanced).1.contains k = (l.map Sigma.fst).contains k := by + simp only [contains_insertMany_list WF.empty, contains_empty, Bool.false_or] + +theorem get?_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} + (h : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.get? k = none := by + simp only [get?_insertMany_list_of_contains_eq_false WF.empty h, get?_empty] + +theorem get?_insertMany_empty_list_of_mem [TransOrd α] [LawfulEqOrd α] + {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = .eq) {v : β k} + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : ⟨k, v⟩ ∈ l) : + (insertMany empty l WF.empty.balanced).1.get? k' = + some (cast (by congr; apply compare_eq_iff_eq.mp k_beq) v) := by + rw [get?_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem get_insertMany_empty_list_of_mem [TransOrd α] [LawfulEqOrd α] + {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = .eq) {v : β k} + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : ⟨k, v⟩ ∈ l) + {h} : + (insertMany empty l WF.empty.balanced).1.get k' h = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + rw [get_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem get!_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} [Inhabited (β k)] + (h : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.get! k = default := by + simp only [get!_insertMany_list_of_contains_eq_false WF.empty h] + apply get!_empty + +theorem get!_insertMany_empty_list_of_mem [TransOrd α] [LawfulEqOrd α] + {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = .eq) {v : β k} [Inhabited (β k')] + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : ⟨k, v⟩ ∈ l) : + (insertMany empty l WF.empty.balanced).1.get! k' = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + rw [get!_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem getD_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] {l : List ((a : α) × β a)} {k : α} {fallback : β k} + (contains_eq_false : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.getD k fallback = fallback := by + rw [getD_insertMany_list_of_contains_eq_false WF.empty contains_eq_false] + apply getD_empty + +theorem getD_insertMany_empty_list_of_mem [TransOrd α] [LawfulEqOrd α] + {l : List ((a : α) × β a)} {k k' : α} (k_beq : compare k k' = .eq) {v : β k} {fallback : β k'} + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : ⟨k, v⟩ ∈ l) : + (insertMany empty l WF.empty.balanced).1.getD k' fallback = + cast (by congr; apply compare_eq_iff_eq.mp k_beq) v := by + rw [getD_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem getKey?_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} {k : α} + (h : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.getKey? k = none := by + rw [getKey?_insertMany_list_of_contains_eq_false WF.empty h] + apply getKey?_empty + +theorem getKey?_insertMany_empty_list_of_mem [TransOrd α] + {l : List ((a : α) × β a)} + {k k' : α} (k_beq : compare k k' = .eq) + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : k ∈ l.map Sigma.fst) : + (insertMany empty l WF.empty.balanced).1.getKey? k' = some k := by + rw [getKey?_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem getKey_insertMany_empty_list_of_mem [TransOrd α] + {l : List ((a : α) × β a)} + {k k' : α} (k_beq : compare k k' = .eq) + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : k ∈ l.map Sigma.fst) + {h'} : + (insertMany empty l WF.empty.balanced).1.getKey k' h' = k := by + rw [getKey_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem getKey!_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + [Inhabited α] {l : List ((a : α) × β a)} {k : α} + (h : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.getKey! k = default := by + rw [getKey!_insertMany_list_of_contains_eq_false WF.empty h] + apply getKey!_empty + +theorem getKey!_insertMany_empty_list_of_mem [TransOrd α] [Inhabited α] + {l : List ((a : α) × β a)} + {k k' : α} (k_beq : compare k k' = .eq) + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : k ∈ l.map Sigma.fst) : + (insertMany empty l WF.empty.balanced).1.getKey! k' = k := by + rw [getKey!_insertMany_list_of_mem WF.empty k_beq distinct mem] + +theorem getKeyD_insertMany_empty_list_of_contains_eq_false [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} {k fallback : α} + (h : (l.map Sigma.fst).contains k = false) : + (insertMany empty l WF.empty.balanced).1.getKeyD k fallback = fallback := by + rw [getKeyD_insertMany_list_of_contains_eq_false WF.empty h] + apply getKeyD_empty + +theorem getKeyD_insertMany_empty_list_of_mem [TransOrd α] + {l : List ((a : α) × β a)} + {k k' fallback : α} (k_beq : compare k k' = .eq) + (distinct : l.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq)) + (mem : k ∈ l.map Sigma.fst) : + (insertMany empty l WF.empty.balanced).1.getKeyD k' fallback = k := by + rw [getKeyD_insertMany_list_of_mem WF.empty k_beq distinct mem] + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 25f87e133f..ab717a7bed 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -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! -/ diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 27a7256c83..38f9ec30fd 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index b62dd6ca83..9d4524ae5c 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -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 diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index ac10d04b94..cf279612e2 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -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 diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 7d92db4d20..6a38e5b52f 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -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 α) : diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 8cade60ddc..1a58f25c6a 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 0c28a994bf..1306cd0e8f 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 6a0dc2a3d6..2756ae81b2 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 91d6a71d04..59394bd48d 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -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