From 2da5b528b7fffda67976214b7fc7c42168133533 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 1 Dec 2025 16:43:34 +0000 Subject: [PATCH] feat: add difference on `DTreeMap`/`TreeMap`/`TreeSet` (#11407) This PR adds the difference operation on `DTreeMap`/`TreeMap`/`TreeSet` and proves several lemmas about it. --------- Co-authored-by: Markus Himmel --- src/Std/Data/DTreeMap/Basic.lean | 11 +- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 728 +++++++++++++++++- .../Data/DTreeMap/Internal/Operations.lean | 44 ++ src/Std/Data/DTreeMap/Internal/WF/Defs.lean | 11 + src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 103 +++ src/Std/Data/DTreeMap/Lemmas.lean | 324 ++++++++ src/Std/Data/DTreeMap/Raw/Basic.lean | 9 + src/Std/Data/DTreeMap/Raw/Lemmas.lean | 368 +++++++++ src/Std/Data/DTreeMap/Raw/WF.lean | 4 + src/Std/Data/TreeMap/Basic.lean | 6 + src/Std/Data/TreeMap/Lemmas.lean | 215 ++++++ src/Std/Data/TreeMap/Raw/Basic.lean | 6 + src/Std/Data/TreeMap/Raw/Lemmas.lean | 225 ++++++ src/Std/Data/TreeMap/Raw/WF.lean | 4 + src/Std/Data/TreeSet/Basic.lean | 10 + src/Std/Data/TreeSet/Lemmas.lean | 145 ++++ src/Std/Data/TreeSet/Raw/Basic.lean | 10 + src/Std/Data/TreeSet/Raw/Lemmas.lean | 160 ++++ src/Std/Data/TreeSet/Raw/WF.lean | 4 + 19 files changed, 2385 insertions(+), 2 deletions(-) diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean index 7868d4c0e3..3687d488c6 100644 --- a/src/Std/Data/DTreeMap/Basic.lean +++ b/src/Std/Data/DTreeMap/Basic.lean @@ -1053,6 +1053,16 @@ def inter (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp := letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.inter t₂.inner t₁.wf.balanced, @Impl.WF.inter _ _ _ _ t₂.inner t₁.wf.balanced t₁.wf⟩ instance : Inter (DTreeMap α β cmp) := ⟨inter⟩ + +/-- +Computes the difference of the given tree maps. +This function always iterates through the smaller map. +-/ +def diff (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp := + letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.diff t₂.inner t₁.wf.balanced, @Impl.WF.diff α β _ t₁.inner t₁.wf t₂.inner⟩ + +instance : SDiff (DTreeMap α β cmp) := ⟨diff⟩ + /-- Erases multiple mappings from the tree map by iterating over the given collection and calling `erase`. @@ -1060,7 +1070,6 @@ Erases multiple mappings from the tree map by iterating over the given collectio @[inline] def eraseMany {ρ} [ForIn Id ρ α] (t : DTreeMap α β cmp) (l : ρ) : DTreeMap α β cmp := letI : Ord α := ⟨cmp⟩; ⟨t.inner.eraseMany l t.wf.balanced, t.wf.eraseMany⟩ - namespace Const variable {β : Type v} diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 2dba4e7ee7..824d19665d 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -47,7 +47,7 @@ macro_rules | apply WF.constInsertMany | apply WF.constInsertManyIfNewUnit | apply WF.alter | apply WF.constAlter | apply WF.modify | apply WF.constModify - | apply WF.filterMap | apply WF.filter | apply WF.map | apply WF.union | apply WF.inter) <;> wf_trivial) + | apply WF.filterMap | apply WF.filter | apply WF.map | apply WF.union | apply WF.inter | apply WF.diff) <;> wf_trivial) /-- Internal implementation detail of the tree map -/ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } ) @@ -68,6 +68,7 @@ private meta def modifyMap : Std.HashMap Name Name := ⟨`insertIfNew, ``toListModel_insertIfNew⟩, ⟨`union, ``toListModel_union_list⟩, ⟨`inter, ``toListModel_inter⟩, + ⟨`diff, ``toListModel_diff⟩, ⟨`erase, ``toListModel_erase⟩, (`insertMany, ``toListModel_insertMany_list), (`Const.insertMany, ``Const.toListModel_insertMany_list), @@ -4850,6 +4851,731 @@ theorem get!_inter!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ end Const +section Diff + +variable {m₁ m₂ : Impl α β} + +/- contains -/ +theorem contains_diff [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff m₂ h₁.balanced).contains k = (m₁.contains k && !m₂.contains k) := by + simp_to_model [diff, contains] + using List.containsKey_filter_not_contains_map_fst + +theorem contains_diff! [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff! m₂).contains k = (m₁.contains k && !m₂.contains k) := by + rw [← diff_eq_diff!] + apply contains_diff h₁ h₂ + all_goals wf_trivial + +theorem contains_diff_iff [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff m₂ h₁.balanced).contains k ↔ m₁.contains k ∧ ¬m₂.contains k := by + simp_to_model [diff, contains] + have := @List.containsKey_filter_not_contains_map_fst_iff α β _ _ m₁.toListModel m₂.toListModel h₁.ordered.distinctKeys k + simp only [Bool.not_eq_true] at this + exact this + +theorem contains_diff!_iff [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff! m₂).contains k ↔ m₁.contains k ∧ ¬m₂.contains k := by + rw [← diff_eq_diff!] + apply contains_diff_iff h₁ h₂ + all_goals wf_trivial + +theorem contains_diff_eq_false_of_contains_eq_false_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).contains k = false := by + revert h + simp_to_model [diff, contains] using List.containsKey_filter_not_contains_map_fst_eq_false_left + +theorem contains_diff!_eq_false_of_contains_eq_false_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (h : m₁.contains k = false) : + (m₁.diff! m₂).contains k = false := by + rw [← diff_eq_diff!] + apply contains_diff_eq_false_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +theorem contains_diff_eq_false_of_contains_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).contains k = false := by + revert h + simp_to_model [diff, contains] using List.containsKey_filter_not_contains_map_fst_of_contains_map_fst_right + +theorem contains_diff!_eq_false_of_contains_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (h : m₂.contains k) : + (m₁.diff! m₂).contains k = false := by + rw [← diff_eq_diff!] + apply contains_diff_eq_false_of_contains_right h₁ h₂ + all_goals wf_trivial + +/- Equiv -/ +theorem Equiv.diff_left {m₃ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) : + (m₁.diff m₃ h₁.balanced).Equiv (m₂.diff m₃ h₂.balanced) := by + revert equiv + simp_to_model [Equiv, diff] + intro equiv + apply List.Perm.filter + wf_trivial + +theorem Equiv.diff!_left {m₃ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₁.Equiv m₂) : + (m₁.diff! m₃).Equiv (m₂.diff! m₃) := by + rw [← diff_eq_diff!, ← diff_eq_diff!] + apply Equiv.diff_left + all_goals wf_trivial + +theorem Equiv.diff_right {m₃ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) : + (m₁.diff m₂ h₁.balanced).Equiv (m₁.diff m₃ h₁.balanced) := by + revert equiv + simp_to_model [Equiv, diff] + intro equiv + apply List.perm_filter_not_contains_map_fst_of_perm equiv + all_goals wf_trivial + +theorem Equiv.diff!_right {m₃ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (equiv : m₂.Equiv m₃) : + (m₁.diff! m₂).Equiv (m₁.diff! m₃) := by + rw [← diff_eq_diff!, ← diff_eq_diff!] + apply Equiv.diff_right + all_goals wf_trivial + +theorem Equiv.diff_congr {m₃ m₄ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) + (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : + (m₁.diff m₂ h₁.balanced).Equiv (m₃.diff m₄ h₃.balanced) := by + revert equiv₁ equiv₂ + simp_to_model [Equiv, diff] + intro equiv₁ equiv₂ + apply List.congr_filter_not_contains_map_fst_of_perm + all_goals wf_trivial + +theorem Equiv.diff!_congr {m₃ m₄ : Impl α β} [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) + (equiv₁ : m₁.Equiv m₃) (equiv₂ : m₂.Equiv m₄) : + (m₁.diff! m₂).Equiv (m₃.diff! m₄) := by + rw [← diff_eq_diff!, ← diff_eq_diff!] + apply Equiv.diff_congr + all_goals wf_trivial + +/- get? -/ +theorem get?_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁.diff m₂ h₁.balanced).get? k = + if m₂.contains k then none else m₁.get? k := by + simp_to_model [diff, get?, contains] using List.getValueCast?_filter_not_contains_map_fst + +theorem get?_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁.diff! m₂).get? k = + if m₂.contains k then none else m₁.get? k := by + rw [← diff_eq_diff!] + apply get?_diff h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).get? k = m₁.get? k := by + revert h + simp_to_model [diff, contains, get?] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem get?_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + (m₁.diff! m₂).get? k = m₁.get? k := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).get? k = none := by + revert h + simp_to_model [diff, contains, get?] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem get?_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + (m₁.diff! m₂).get? k = none := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).get? k = none := by + revert h + simp_to_model [diff, get?, contains] using List.getValueCast?_filter_not_contains_map_fst_of_containsKey_right + +theorem get?_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + (m₁.diff! m₂).get? k = none := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +/- get -/ +theorem get_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} : + (m₁.diff m₂ h₁.balanced).get k h_contains = + m₁.get k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by + simp_to_model [diff, get, contains] using List.getValueCast_filter_not_contains_map_fst + +theorem get_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff! m₂).contains k} : + (m₁.diff! m₂).get k h_contains = + m₁.get k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by + conv => + lhs + arg 1 + rw [← diff_eq_diff!] + . skip + . apply h₁ + simp_to_model [diff, get, contains] using List.getValueCast_filter_not_contains_map_fst + +/- getD -/ +theorem getD_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} : + (m₁.diff m₂ h₁.balanced).getD k fallback = + if m₂.contains k then fallback else m₁.getD k fallback := by + simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst + +theorem getD_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} : + (m₁.diff! m₂).getD k fallback = + if m₂.contains k then fallback else m₁.getD k fallback := by + rw [← diff_eq_diff!] + apply getD_diff h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).getD k fallback = m₁.getD k fallback := by + revert h + simp_to_model [diff, contains, getD] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem getD_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₂.contains k = false) : + (m₁.diff! m₂).getD k fallback = m₁.getD k fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).getD k fallback = fallback := by + revert h + simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right + +theorem getD_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₂.contains k) : + (m₁.diff! m₂).getD k fallback = fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).getD k fallback = fallback := by + revert h + simp_to_model [diff, getD, contains] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem getD_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (h : m₁.contains k = false) : + (m₁.diff! m₂).getD k fallback = fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +/- get! -/ +theorem get!_diff [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] : + (m₁.diff m₂ h₁.balanced).get! k = + if m₂.contains k then default else m₁.get! k := by + simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst + +theorem get!_diff! [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] : + (m₁.diff! m₂).get! k = + if m₂.contains k then default else m₁.get! k := by + rw [← diff_eq_diff!] + apply get!_diff h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).get! k = m₁.get! k := by + revert h + simp_to_model [diff, contains, get!] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem get!_diff!_of_contains_eq_false_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k = false) : + (m₁.diff! m₂).get! k = m₁.get! k := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).get! k = default := by + revert h + simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst_of_contains_map_fst_right + +theorem get!_diff!_of_contains_right [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k) : + (m₁.diff! m₂).get! k = default := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).get! k = default := by + revert h + simp_to_model [diff, get!, contains] using List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem get!_diff!_of_contains_eq_false_left [TransOrd α] [LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (h : m₁.contains k = false) : + (m₁.diff! m₂).get! k = default := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +/- getKey? -/ +theorem getKey?_diff [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁.diff m₂ h₁.balanced).getKey? k = + if m₂.contains k then none else m₁.getKey? k := by + simp_to_model [diff, contains, getKey?] using List.getKey?_filter_not_contains_map_fst + +theorem getKey?_diff! [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁.diff! m₂).getKey? k = + if m₂.contains k then none else m₁.getKey? k := by + rw [← diff_eq_diff!] + apply getKey?_diff h₁ h₂ + all_goals wf_trivial + +theorem getKey?_diff_of_contains_eq_false_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKey? k = m₁.getKey? k := by + revert h + simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem getKey?_diff!_of_contains_eq_false_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) : + (m₁.diff! m₂).getKey? k = m₁.getKey? k := by + rw [← diff_eq_diff!] + apply getKey?_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem getKey?_diff_of_contains_eq_false_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKey? k = none := by + revert h + simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem getKey?_diff!_of_contains_eq_false_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) : + (m₁.diff! m₂).getKey? k = none := by + rw [← diff_eq_diff!] + apply getKey?_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +theorem getKey?_diff_of_contains_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).getKey? k = none := by + revert h + simp_to_model [contains, getKey?, diff] using List.getKey?_filter_not_contains_map_fst_of_containsKey_right + +theorem getKey?_diff!_of_contains_right [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : m₂.contains k) : + (m₁.diff! m₂).getKey? k = none := by + rw [← diff_eq_diff!] + apply getKey?_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +/- getKey -/ +theorem getKey_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} : + (m₁.diff m₂ h₁.balanced).getKey k h_contains = + m₁.getKey k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by + simp_to_model [diff, contains, getKey] using List.getKey_filter_not_contains_map_fst + +theorem getKey_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff! m₂).contains k} : + (m₁.diff! m₂).getKey k h_contains = + m₁.getKey k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by + conv => + lhs + arg 1 + rw [← diff_eq_diff!] + . skip + . apply h₁ + simp_to_model [diff, contains, getKey] using List.getKey_filter_not_contains_map_fst + +/- getKeyD -/ +theorem getKeyD_diff [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁.diff m₂ h₁.balanced).getKeyD k fallback = + if m₂.contains k then fallback else m₁.getKeyD k fallback := by + simp_to_model [diff, getKeyD, contains] using List.getKeyD_filter_not_contains_map_fst + +theorem getKeyD_diff! [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁.diff! m₂).getKeyD k fallback = + if m₂.contains k then fallback else m₁.getKeyD k fallback := by + rw [← diff_eq_diff!] + apply getKeyD_diff h₁ h₂ + all_goals wf_trivial + +theorem getKeyD_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKeyD k fallback = m₁.getKeyD k fallback := by + revert h + simp_to_model [contains, diff, getKeyD] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right + +theorem getKeyD_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k = false) : + (m₁.diff! m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + rw [← diff_eq_diff!] + apply getKeyD_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem getKeyD_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).getKeyD k fallback = fallback := by + revert h + simp_to_model [diff, getKeyD, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_right + +theorem getKeyD_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₂.contains k) : + (m₁.diff! m₂).getKeyD k fallback = fallback := by + rw [← diff_eq_diff!] + apply getKeyD_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem getKeyD_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKeyD k fallback = fallback := by + revert h + simp_to_model [diff, getKeyD, contains] using getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left + +theorem getKeyD_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (h : m₁.contains k = false) : + (m₁.diff! m₂).getKeyD k fallback = fallback := by + rw [← diff_eq_diff!] + apply getKeyD_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +/- getKey! -/ +theorem getKey!_diff [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff m₂ h₁.balanced).getKey! k = + if m₂.contains k then default else m₁.getKey! k := by + simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst + +theorem getKey!_diff! [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁.diff! m₂).getKey! k = + if m₂.contains k then default else m₁.getKey! k := by + rw [← diff_eq_diff!] + apply getKey!_diff h₁ h₂ + all_goals wf_trivial + +theorem getKey!_diff_of_contains_eq_false_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKey! k = m₁.getKey! k := by + revert h + simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_right + +theorem getKey!_diff!_of_contains_eq_false_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₂.contains k = false) : + (m₁.diff! m₂).getKey! k = m₁.getKey! k := by + rw [← diff_eq_diff!] + apply getKey!_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem getKey!_diff_of_contains_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₂.contains k) : + (m₁.diff m₂ h₁.balanced).getKey! k = default := by + revert h + simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_right + +theorem getKey!_diff!_of_contains_right [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₂.contains k) : + (m₁.diff! m₂).getKey! k = default := by + rw [← diff_eq_diff!] + apply getKey!_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem getKey!_diff_of_contains_eq_false_left [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) : + (m₁.diff m₂ h₁.balanced).getKey! k = default := by + revert h + simp_to_model [diff, getKey!, contains] using List.getKeyD_filter_not_contains_map_fst_of_contains_eq_false_left + +theorem getKey!_diff!_of_contains_eq_false_left [Inhabited α] [TransOrd α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (h : m₁.contains k = false) : + (m₁.diff! m₂).getKey! k = default := by + rw [← diff_eq_diff!] + apply getKey!_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +/- size -/ +theorem size_diff_le_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff m₂ h₁.balanced).size ≤ m₁.size := by + simp_to_model [diff, size] using List.length_filter_le + +theorem size_diff!_le_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff! m₂).size ≤ m₁.size := by + rw [← diff_eq_diff!] + apply size_diff_le_size_left h₁ h₂ + all_goals wf_trivial + +theorem size_diff_eq_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), m₁.contains a → m₂.contains a = false) : + (m₁.diff m₂ h₁.balanced).size = m₁.size := by + revert h + simp_to_model [diff, size, contains] using List.length_filter_not_contains_map_fst_eq_length_left + +theorem size_diff!_eq_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), m₁.contains a → m₂.contains a = false) : + (m₁.diff! m₂).size = m₁.size := by + rw [← diff_eq_diff!] + apply size_diff_eq_size_left h₁ h₂ + all_goals wf_trivial + +theorem size_diff_add_size_inter_eq_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff m₂ h₁.balanced).size + (m₁.inter m₂ h₁.balanced).size = m₁.size := by + simp_to_model [diff, inter, size] using List.size_filter_not_contains_map_fst_add_size_inter_eq_size_left + +theorem size_diff!_add_size_inter!_eq_size_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff! m₂).size + (m₁.inter! m₂).size = m₁.size := by + rw [← diff_eq_diff!, ← inter_eq_inter!] + apply size_diff_add_size_inter_eq_size_left h₁ h₂ + all_goals wf_trivial + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) : + (m₁.diff m₂ h₁.balanced).isEmpty = true := by + revert h + simp_to_model [isEmpty, diff] using List.isEmpty_filter_not_contains_map_fst_left + +@[simp] +theorem isEmpty_diff!_left [TransOrd α] + (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) : + (m₁.diff! m₂).isEmpty = true := by + rw [← diff_eq_diff!] + apply isEmpty_diff_left h₁ h₂ + all_goals wf_trivial + +theorem isEmpty_diff_iff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff m₂ h₁.balanced).isEmpty ↔ ∀ k, m₁.contains k → m₂.contains k := by + simp_to_model [diff, contains, isEmpty] using List.isEmpty_filter_not_contains_map_fst_iff + +theorem isEmpty_diff!_iff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁.diff! m₂).isEmpty ↔ ∀ k, m₁.contains k → m₂.contains k := by + rw [← diff_eq_diff!] + apply isEmpty_diff_iff h₁ h₂ + all_goals wf_trivial + +end Diff + +namespace Const + +variable {β : Type v} {m₁ m₂ : Impl α (fun _ => β)} + +/- get? -/ +theorem get?_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get? (m₁.diff m₂ h₁.balanced) k = + if m₂.contains k then none else Const.get? m₁ k := by + simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst + +theorem get?_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get? (m₁.diff! m₂) k = + if m₂.contains k then none else Const.get? m₁ k := by + rw [← diff_eq_diff!] + apply get?_diff h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + Const.get? (m₁.diff m₂ h₁.balanced) k = Const.get? m₁ k := by + revert h + simp_to_model [diff, contains, Const.get?] using List.getValue?_filter_not_contains_map_fst_of_contains_eq_false_right + +theorem get?_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + Const.get? (m₁.diff! m₂) k = Const.get? m₁ k := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + Const.get? (m₁.diff m₂ h₁.balanced) k = none := by + revert h + simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem get?_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + Const.get? (m₁.diff! m₂) k = none := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +theorem get?_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + Const.get? (m₁.diff m₂ h₁.balanced) k = none := by + revert h + simp_to_model [diff, Const.get?, contains] using List.getValue?_filter_not_contains_map_fst_of_contains_right + +theorem get?_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + Const.get? (m₁.diff! m₂) k = none := by + rw [← diff_eq_diff!] + apply get?_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +/- get -/ +theorem get_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff m₂ h₁.balanced).contains k} : + Const.get (m₁.diff m₂ h₁.balanced) k h_contains = + Const.get m₁ k ((contains_diff_iff h₁ h₂).1 h_contains).1 := by + simp_to_model [diff, Const.get, contains] using List.getValue_filter_not_contains + +theorem get_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_contains : (m₁.diff! m₂).contains k} : + Const.get (m₁.diff! m₂) k h_contains = + Const.get m₁ k ((contains_diff!_iff h₁ h₂).1 h_contains).1 := by + conv => + lhs + arg 1 + rw [← diff_eq_diff!] + . skip + . apply h₁ + simp_to_model [diff, Const.get, contains] using List.getValue_filter_not_contains + +/- getD -/ +theorem getD_diff [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} : + Const.getD (m₁.diff m₂ h₁.balanced) k fallback = + if m₂.contains k then fallback else Const.getD m₁ k fallback := by + simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst + +theorem getD_diff! [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} : + Const.getD (m₁.diff! m₂) k fallback = + if m₂.contains k then fallback else Const.getD m₁ k fallback := by + rw [← diff_eq_diff!] + apply getD_diff h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₂.contains k = false) : + Const.getD (m₁.diff m₂ h₁.balanced) k fallback = Const.getD m₁ k fallback := by + revert h + simp_to_model [diff, contains, Const.getD] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem getD_diff!_of_contains_eq_false_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₂.contains k = false) : + Const.getD (m₁.diff! m₂) k fallback = Const.getD m₁ k fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₂.contains k) : + Const.getD (m₁.diff m₂ h₁.balanced) k fallback = fallback := by + revert h + simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right + +theorem getD_diff!_of_contains_right [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₂.contains k) : + Const.getD (m₁.diff! m₂) k fallback = fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem getD_diff_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₁.contains k = false) : + Const.getD (m₁.diff m₂ h₁.balanced) k fallback = fallback := by + revert h + simp_to_model [diff, Const.getD, contains] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem getD_diff!_of_contains_eq_false_left [TransOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : m₁.contains k = false) : + Const.getD (m₁.diff! m₂) k fallback = fallback := by + rw [← diff_eq_diff!] + apply getD_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +/- get! -/ +theorem get!_diff [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get! (m₁.diff m₂ h₁.balanced) k = + if m₂.contains k then default else Const.get! m₁ k := by + simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst + +theorem get!_diff! [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get! (m₁.diff! m₂) k = + if m₂.contains k then default else Const.get! m₁ k := by + rw [← diff_eq_diff!] + apply get!_diff h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_eq_false_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + Const.get! (m₁.diff m₂ h₁.balanced) k = Const.get! m₁ k := by + revert h + simp_to_model [diff, contains, Const.get!] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_right + +theorem get!_diff!_of_contains_eq_false_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k = false) : + Const.get! (m₁.diff! m₂) k = Const.get! m₁ k := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_eq_false_right h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + Const.get! (m₁.diff m₂ h₁.balanced) k = default := by + revert h + simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst_of_contains_map_fst_right + +theorem get!_diff!_of_contains_right [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₂.contains k) : + Const.get! (m₁.diff! m₂) k = default := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_right h₁ h₂ + all_goals wf_trivial + +theorem get!_diff_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + Const.get! (m₁.diff m₂ h₁.balanced) k = default := by + revert h + simp_to_model [diff, Const.get!, contains] using List.getValueD_filter_not_contains_map_fst_of_containsKey_eq_false_left + +theorem get!_diff!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : m₁.contains k = false) : + Const.get! (m₁.diff! m₂) k = default := by + rw [← diff_eq_diff!] + apply get!_diff_of_contains_eq_false_left h₁ h₂ + all_goals wf_trivial + +end Const + section Alter theorem isEmpty_alter_eq_isEmpty_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} diff --git a/src/Std/Data/DTreeMap/Internal/Operations.lean b/src/Std/Data/DTreeMap/Internal/Operations.lean index e850b5126f..20cee886e1 100644 --- a/src/Std/Data/DTreeMap/Internal/Operations.lean +++ b/src/Std/Data/DTreeMap/Internal/Operations.lean @@ -481,6 +481,36 @@ def eraseMany! [Ord α] {ρ : Type w} [ForIn Id ρ α] (t : Impl α β) (l : ρ) r := ⟨r.val.erase! a, fun h₀ h₁ => h₁ _ _ (r.2 h₀ h₁)⟩ return r +/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle. -/ +abbrev IteratedEntryErasureFrom [Ord α] (t) := + { t' // ∀ {P : Impl α β → Prop}, P t → (∀ t'' a h, P t'' → P (t''.erase a h).impl) → P t' } + +/-- Iterate over `l` and erase all of its elements from `t`. -/ +@[inline] +def eraseManyEntries [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) (h : t.Balanced) : + IteratedEntryErasureFrom t := Id.run do + let mut r := ⟨t, fun h _ => h⟩ + for ⟨a, _⟩ in l do + let hr := r.2 h (fun t'' a h _ => (t''.erase a h).balanced_impl) + r := ⟨r.val.erase a hr |>.impl, fun h₀ h₁ => h₁ _ _ _ (r.2 h₀ h₁)⟩ + return r + +/-- A tree map obtained by erasing elements from `t`, bundled with an inductive principle. -/ +abbrev IteratedSlowEntryErasureFrom [Ord α] (t) := + { t' // ∀ {P : Impl α β → Prop}, P t → (∀ t'' a, P t'' → P (t''.erase! a)) → P t' } + +/-- +Slower version of `eraseManyEntries` which can be used in absence of balance information but still +assumes the preconditions of `eraseManyEntries`, otherwise might panic. +-/ +@[inline] +def eraseManyEntries! [Ord α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (t : Impl α β) (l : ρ) : + IteratedSlowErasureFrom t := Id.run do + let mut r := ⟨t, fun h _ => h⟩ + for ⟨a, _⟩ in l do + r := ⟨r.val.erase! a, fun h₀ h₁ => h₁ _ _ (r.2 h₀ h₁)⟩ + return r + /-- A tree map obtained by inserting elements into `t`, bundled with an inductive principle. -/ abbrev IteratedInsertionInto [Ord α] (t) := { t' // ∀ {P : Impl α β → Prop}, P t → (∀ t'' a b h, P t'' → P (t''.insert a b h).impl) → P t' } @@ -792,6 +822,20 @@ information but still assumes the preconditions of `filter`, otherwise might pan def inter! [Ord α] (m₁ m₂ : Impl α β): Impl α β := if m₁.size ≤ m₂.size then m₁.filter! (fun k _ => m₂.contains k) else interSmaller m₁ m₂ +/-- +Computes the difference of the given tree maps. +This function always iterates through the smaller map. +-/ +def diff [Ord α] (t₁ t₂ : Impl α β) (h₁ : t₁.Balanced) : Impl α β := + if t₁.size ≤ t₂.size then (t₁.filter (fun p _ => !t₂.contains p) h₁).impl else (t₁.eraseManyEntries t₂ h₁) + +/-- +Slower version of `diff` which can be used in the absence of balance +information but still assumes the preconditions of `diff`, otherwise might panic. +-/ +def diff! [Ord α] (t₁ t₂ : Impl α β) : Impl α β := + if t₁.size ≤ t₂.size then t₁.filter! (fun p _ => !t₂.contains p) else t₁.eraseManyEntries! t₂ + /-- Changes the mapping of the key `k` by applying the function `f` to the current mapped value (if any). This function can be used to insert a new mapping, modify an existing one or delete it. diff --git a/src/Std/Data/DTreeMap/Internal/WF/Defs.lean b/src/Std/Data/DTreeMap/Internal/WF/Defs.lean index 3e3290077a..d3c371b7e4 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Defs.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Defs.lean @@ -76,6 +76,10 @@ theorem WF.balanced [Ord α] {t : Impl α β} (h : WF t) : t.Balanced := by case constModify ih => exact Const.balanced_modify ih case inter ih => exact balanced_inter ih +theorem WF.eraseManyEntries [Ord α] {ρ} [ForIn Id ρ ((a : α) × β a)] {t : Impl α β} {l : ρ} {h} (hwf : WF t) : + WF (t.eraseManyEntries l h).val := + (t.eraseManyEntries l h).2 hwf fun _ _ _ hwf' => hwf'.erase + theorem WF.eraseMany [Ord α] {ρ} [ForIn Id ρ α] {t : Impl α β} {l : ρ} {h} (hwf : WF t) : WF (t.eraseMany l h).val := (t.eraseMany l h).2 hwf fun _ _ _ hwf' => hwf'.erase @@ -110,6 +114,13 @@ theorem WF.union [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α . apply WF.insertManyIfNew h₂ . apply WF.insertMany h₁ +theorem WF.diff [Ord α] {t₁ : Impl α β} {h₁ : t₁.WF} {t₂ : Impl α β} : + (t₁.diff t₂ h₁.balanced).WF := by + simp [Impl.diff] + split + · apply WF.filter h₁ + · apply WF.eraseManyEntries h₁ + section Const variable {β : Type v} diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 1142017a6b..870daa6921 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1661,6 +1661,75 @@ theorem WF.eraseMany! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ α] {l : ρ} {t : Impl α β} (h : t.WF) : (t.eraseMany! l).1.WF := (t.eraseMany! l).2 h (fun _ _ h' => h'.erase!) +/-! +### `eraseManyEntries` +-/ + +theorem eraseManyEntries!_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} : + (t.eraseManyEntries! l).val = l.foldl (init := t) fun acc ⟨k, _⟩ => acc.erase! k := by + simp [eraseManyEntries!, ← List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl] + +theorem eraseManyEntries_eq_foldl {_ : Ord α} {l : List ((a : α) × β a)} {t : Impl α β} (h : t.Balanced) : + (t.eraseManyEntries l h).val = l.foldl (init := t) fun acc ⟨k, _⟩ => acc.erase! k := by + simp [eraseManyEntries, erase_eq_erase!, ← List.foldl_hom Subtype.val, List.forIn_pure_yield_eq_foldl] + +theorem eraseManyEntries_impl_eq_foldl {_ : Ord α} {t₁ : Impl α β} (h₁ : t₁.Balanced) {t₂ : Impl α β} : + (t₁.eraseManyEntries t₂ h₁).val = t₂.foldl (init := t₁) fun acc k _ => acc.erase! k := by + simp [foldl_eq_foldl] + rw [← eraseManyEntries_eq_foldl] + rotate_left + · exact h₁ + · simp only [eraseManyEntries, pure, ForIn.forIn, Id.run_bind] + rw [forIn_eq_forIn_toListModel] + congr + +theorem eraseManyEntries!_impl_eq_foldl {_ : Ord α} {t₁ : Impl α β} {t₂ : Impl α β} : + (t₁.eraseManyEntries! t₂).val = t₂.foldl (init := t₁) fun acc k _ => acc.erase! k := by + simp [foldl_eq_foldl] + rw [← eraseManyEntries!_eq_foldl] + simp only [eraseManyEntries!, pure, ForIn.forIn, Id.run_bind] + rw [forIn_eq_forIn_toListModel] + congr + +theorem eraseManyEntries_impl_eq_eraseManyEntries! {_ : Ord α} + {t₁ t₂ : Impl α β} (h : t₁.Balanced) : + (t₁.eraseManyEntries t₂ h).val = (t₁.eraseManyEntries! t₂).val := by + simp only [eraseManyEntries_impl_eq_foldl, eraseManyEntries!_impl_eq_foldl] + +theorem eraseManyEntries_impl_perm_eraseList {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] + {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : + List.Perm (t₁.eraseManyEntries t₂ h₁.balanced).val.toListModel (t₁.toListModel.eraseList (t₂.toListModel.map (·.1))) := by + rw [eraseManyEntries_impl_eq_foldl] + rw [foldl_eq_foldl] + induction t₂.toListModel generalizing t₁ with + | nil => rfl + | cons e es ih => + simp only [List.foldl_cons] + apply List.Perm.trans (@ih (t₁.erase! e.1) (h₁.erase!)) + apply eraseList_perm_of_perm_first + · apply toListModel_erase! + · exact h₁.balanced + · exact h₁.ordered + · apply h₁.erase!.ordered.distinctKeys + +theorem toListModel_eraseManyEntries_impl {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] + {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : + List.Perm (t₁.eraseManyEntries t₂ h₁.balanced).val.toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst )) := by + apply List.Perm.trans + · apply eraseManyEntries_impl_perm_eraseList h₁ + · apply eraseList_perm_filter_not_contains + · apply h₁.ordered.distinctKeys + +theorem toListModel_eraseManyEntries!_impl {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] + {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : + List.Perm (t₁.eraseManyEntries! t₂).val.toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst)) := by + rw [← eraseManyEntries_impl_eq_eraseManyEntries! h₁.balanced] + apply toListModel_eraseManyEntries_impl h₁ + +theorem WF.eraseManyEntries! {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ ((a : α) × β a)] {l : ρ} + {t : Impl α β} (h : t.WF) : (t.eraseManyEntries! l).1.WF := + (t.eraseManyEntries! l).2 h (fun _ _ h' => h'.erase!) + /-! ### `insertMany` -/ @@ -2048,6 +2117,40 @@ theorem toListModel_interSmallerFn {_ : Ord α} [TransOrd α] [BEq α] [LawfulBE simp only [heq, hml] exact h₁.ordered +/-! +### diff +-/ + +theorem toListModel_diff {_ : Ord α} [BEq α] [LawfulBEqOrd α] [TransOrd α] + {t₁ t₂ : Impl α β} (h₁ : t₁.WF) (h₂ : t₂.WF) : + List.Perm (t₁.diff t₂ h₁.balanced).toListModel (t₁.toListModel.filter (fun p => !List.contains (t₂.toListModel.map Sigma.fst) p.fst)) := by + rw [diff] + split + · simp only [toListModel_filter] + conv => + lhs + lhs + ext e + congr + rw [contains_eq_containsKey h₂.ordered] + rw [containsKey_eq_contains_map_fst] + · apply toListModel_eraseManyEntries_impl h₁ + +theorem diff_eq_diff! [Ord α] + {t₁ t₂ : Impl α β} (h₁ : t₁.WF) : + (t₁.diff t₂ h₁.balanced) = t₁.diff! t₂ := by + simp only [diff, diff!] + split + · rw [filter_eq_filter!] + . rw [eraseManyEntries_impl_eq_eraseManyEntries! h₁.balanced] + +theorem WF.diff! {_ : Ord α} [TransOrd α] + {t₁ : Impl α β} (h₁ : t₁.WF) {t₂ : Impl α β} : (t₁.diff! t₂).WF := by + simp only [Impl.diff!] + split + . exact WF.filter! h₁ + . exact WF.eraseManyEntries! h₁ + /-! ### interSmaller -/ diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index b871d6117c..453d977b49 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -2877,6 +2877,330 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] end Const +section Diff + +variable {t₁ t₂ : DTreeMap α β cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := + Impl.contains_diff t₁.wf t₂.wf + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ ¬k ∈ t₂ := + Impl.contains_diff_iff t₁.wf t₂.wf + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] + {k : α} (h : ¬k ∈ t₁) : + ¬k ∈ t₁ \ t₂ := by + rw [← contains_eq_false_iff_not_mem] at h ⊢ + exact Impl.contains_diff_eq_false_of_contains_eq_false_left t₁.wf t₂.wf h + +theorem not_mem_diff_of_mem_right [TransCmp cmp] + {k : α} (h : k ∈ t₂) : + ¬ k ∈ t₁ \ t₂ := by + rw [← contains_eq_false_iff_not_mem] + exact Impl.contains_diff_eq_false_of_contains_right t₁.wf t₂.wf h + +/- Equiv -/ +theorem Equiv.diff_left {t₃ : DTreeMap α β cmp} [TransCmp cmp] + (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := + ⟨Impl.Equiv.diff_left t₁.wf t₂.wf t₃.wf equiv.1⟩ + +theorem Equiv.diff_right {t₃ : DTreeMap α β cmp} [TransCmp cmp] + (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := + ⟨Impl.Equiv.diff_right t₁.wf t₂.wf t₃.wf equiv.1⟩ + +theorem Equiv.diff_congr {t₃ t₄ : DTreeMap α β cmp} [TransCmp cmp] + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := + ⟨Impl.Equiv.diff_congr t₁.wf t₂.wf t₃.wf t₄.wf equiv₁.1 equiv₂.1⟩ + +/- get? -/ +theorem get?_diff [TransCmp cmp] [LawfulEqCmp cmp] {k : α} : + (t₁ \ t₂).get? k = + if k ∈ t₂ then none else t₁.get? k := + Impl.get?_diff t₁.wf t₂.wf + +theorem get?_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.get?_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem get?_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.get?_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +theorem get?_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} (h : k ∈ t₂) : + (t₁ \ t₂).get? k = none := by + rw [mem_iff_contains] at h + exact Impl.get?_diff_of_contains_right t₁.wf t₂.wf h + +/- get -/ +theorem get_diff [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k (mem_diff_iff.1 h_mem).1 := + Impl.get_diff t₁.wf t₂.wf + +/- getD -/ +theorem getD_diff [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} {fallback : β k} : + (t₁ \ t₂).getD k fallback = + if k ∈ t₂ then fallback else t₁.getD k fallback := + Impl.getD_diff t₁.wf t₂.wf + +theorem getD_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} {fallback : β k} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getD_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem getD_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} {fallback : β k} (h : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := by + rw [mem_iff_contains] at h + exact Impl.getD_diff_of_contains_right t₁.wf t₂.wf h + +theorem getD_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} {fallback : β k} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getD_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +/- get! -/ +theorem get!_diff [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} [Inhabited (β k)] : + (t₁ \ t₂).get! k = + if k ∈ t₂ then default else t₁.get! k := + Impl.get!_diff t₁.wf t₂.wf + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} [Inhabited (β k)] (h : ¬k ∈ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.get!_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem get!_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} [Inhabited (β k)] (h : k ∈ t₂) : + (t₁ \ t₂).get! k = default := by + rw [mem_iff_contains] at h + exact Impl.get!_diff_of_contains_right t₁.wf t₂.wf h + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] + {k : α} [Inhabited (β k)] (h : ¬k ∈ t₁) : + (t₁ \ t₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.get!_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +/- getKey? -/ +theorem getKey?_diff [TransCmp cmp] + {k : α} : + (t₁ \ t₂).getKey? k = + if k ∈ t₂ then none else t₁.getKey? k := + Impl.getKey?_diff t₁.wf t₂.wf + +theorem getKey?_diff_of_not_mem_right [TransCmp cmp] + {k : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKey? k = t₁.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKey?_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem getKey?_diff_of_not_mem_left [TransCmp cmp] + {k : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKey?_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +theorem getKey?_diff_of_mem_right [TransCmp cmp] + {k : α} (h : k ∈ t₂) : + (t₁ \ t₂).getKey? k = none := by + rw [mem_iff_contains] at h + exact Impl.getKey?_diff_of_contains_right t₁.wf t₂.wf h + +/- getKey -/ +theorem getKey_diff [TransCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).getKey k h_mem = + t₁.getKey k (mem_diff_iff.1 h_mem).1 := + Impl.getKey_diff t₁.wf t₂.wf + +/- getKeyD -/ +theorem getKeyD_diff [TransCmp cmp] {k fallback : α} : + (t₁ \ t₂).getKeyD k fallback = + if k ∈ t₂ then fallback else t₁.getKeyD k fallback := + Impl.getKeyD_diff t₁.wf t₂.wf + +theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] {k fallback : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKeyD_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem getKeyD_diff_of_mem_right [TransCmp cmp] {k fallback : α} (h : k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = fallback := by + rw [mem_iff_contains] at h + exact Impl.getKeyD_diff_of_contains_right t₁.wf t₂.wf h + +theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] {k fallback : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKeyD_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +/- getKey! -/ +theorem getKey!_diff [Inhabited α] [TransCmp cmp] + {k : α} : + (t₁ \ t₂).getKey! k = + if k ∈ t₂ then default else t₁.getKey! k := + Impl.getKey!_diff t₁.wf t₂.wf + +theorem getKey!_diff_of_not_mem_right [Inhabited α] [TransCmp cmp] + {k : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKey! k = t₁.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKey!_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem getKey!_diff_of_mem_right [Inhabited α] [TransCmp cmp] + {k : α} (h : k ∈ t₂) : + (t₁ \ t₂).getKey! k = default := by + rw [mem_iff_contains] at h + exact Impl.getKey!_diff_of_contains_right t₁.wf t₂.wf h + +theorem getKey!_diff_of_not_mem_left [Inhabited α] [TransCmp cmp] + {k : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.getKey!_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] : + (t₁ \ t₂).size ≤ t₁.size := + Impl.size_diff_le_size_left t₁.wf t₂.wf + +theorem size_diff_eq_size_left [TransCmp cmp] + (h : ∀ (a : α), a ∈ t₁ → ¬a ∈ t₂) : + (t₁ \ t₂).size = t₁.size := by + conv at h => + ext a + rhs + rw [← contains_eq_false_iff_not_mem] + exact Impl.size_diff_eq_size_left t₁.wf t₂.wf h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + Impl.size_diff_add_size_inter_eq_size_left t₁.wf t₂.wf + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + Impl.isEmpty_diff_left t₁.wf t₂.wf h + +theorem isEmpty_diff_iff [TransCmp cmp] : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := by + exact Impl.isEmpty_diff_iff t₁.wf t₂.wf + +end Diff + +namespace Const + +variable {β : Type v} {t₁ t₂ : DTreeMap α (fun _ => β) cmp} + +/- get? -/ +theorem get?_diff [TransCmp cmp] {k : α} : + Const.get? (t₁ \ t₂) k = + if k ∈ t₂ then none else Const.get? t₁ k := + Impl.Const.get?_diff t₁.wf t₂.wf + +theorem get?_diff_of_not_mem_right [TransCmp cmp] + {k : α} (h : ¬k ∈ t₂) : + Const.get? (t₁ \ t₂) k = Const.get? t₁ k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.get?_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem get?_diff_of_not_mem_left [TransCmp cmp] + {k : α} (h : ¬k ∈ t₁) : + Const.get? (t₁ \ t₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.get?_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +theorem get?_diff_of_mem_right [TransCmp cmp] + {k : α} (h : k ∈ t₂) : + Const.get? (t₁ \ t₂) k = none := by + rw [mem_iff_contains] at h + exact Impl.Const.get?_diff_of_contains_right t₁.wf t₂.wf h + +/- get -/ +theorem get_diff [TransCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + Const.get (t₁ \ t₂) k h_mem = + Const.get t₁ k (mem_diff_iff.1 h_mem).1 := + Impl.Const.get_diff t₁.wf t₂.wf + +/- getD -/ +theorem getD_diff [TransCmp cmp] + {k : α} {fallback : β} : + Const.getD (t₁ \ t₂) k fallback = + if k ∈ t₂ then fallback else Const.getD t₁ k fallback := + Impl.Const.getD_diff t₁.wf t₂.wf + +theorem getD_diff_of_not_mem_right [TransCmp cmp] + {k : α} {fallback : β} (h : ¬k ∈ t₂) : + Const.getD (t₁ \ t₂) k fallback = Const.getD t₁ k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.getD_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem getD_diff_of_mem_right [TransCmp cmp] + {k : α} {fallback : β} (h : k ∈ t₂) : + Const.getD (t₁ \ t₂) k fallback = fallback := by + rw [mem_iff_contains] at h + exact Impl.Const.getD_diff_of_contains_right t₁.wf t₂.wf h + +theorem getD_diff_of_not_mem_left [TransCmp cmp] + {k : α} {fallback : β} (h : ¬k ∈ t₁) : + Const.getD (t₁ \ t₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.getD_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +/- get! -/ +theorem get!_diff [TransCmp cmp] [Inhabited β] + {k : α} : + Const.get! (t₁ \ t₂) k = + if k ∈ t₂ then default else Const.get! t₁ k := + Impl.Const.get!_diff t₁.wf t₂.wf + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] + {k : α} (h : ¬k ∈ t₂) : + Const.get! (t₁ \ t₂) k = Const.get! t₁ k := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.get!_diff_of_contains_eq_false_right t₁.wf t₂.wf h + +theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] + {k : α} (h : k ∈ t₂) : + Const.get! (t₁ \ t₂) k = default := by + rw [mem_iff_contains] at h + exact Impl.Const.get!_diff_of_contains_right t₁.wf t₂.wf h + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] + {k : α} (h : ¬k ∈ t₁) : + Const.get! (t₁ \ t₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at h + exact Impl.Const.get!_diff_of_contains_eq_false_left t₁.wf t₂.wf h + +end Const + section Alter theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] [LawfulEqCmp cmp] {k : α} diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean index 88b6db876e..4b008a7220 100644 --- a/src/Std/Data/DTreeMap/Raw/Basic.lean +++ b/src/Std/Data/DTreeMap/Raw/Basic.lean @@ -732,6 +732,15 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp := instance : Inter (Raw α β cmp) := ⟨inter⟩ +/-- +Computes the diffrence of the given tree maps. +This function always iteraters through the smaller map. +-/ +def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp := + letI : Ord α := ⟨cmp⟩; ⟨t₁.inner.diff! t₂.inner⟩ + +instance : SDiff (Raw α β cmp) := ⟨diff⟩ + @[inline, inherit_doc DTreeMap.eraseMany] def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α β cmp) (l : ρ) : Raw α β cmp := letI : Ord α := ⟨cmp⟩; ⟨t.inner.eraseMany! l⟩ diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 761ecdbfe7..58c576c503 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -3042,6 +3042,374 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF end Const +section Diff + +variable {t₁ t₂ : Raw α β cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := by + simp only [SDiff.sdiff] + exact Impl.contains_diff! h₁ h₂ + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ ¬k ∈ t₂ := by + simp only [SDiff.sdiff, Membership.mem] + exact Impl.contains_diff!_iff h₁ h₂ + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : ¬k ∈ t₁) : + ¬k ∈ t₁ \ t₂ := by + rw [← contains_eq_false_iff_not_mem] at h ⊢ + simp only [SDiff.sdiff] + exact Impl.contains_diff!_eq_false_of_contains_eq_false_left h₁ h₂ h + +theorem not_mem_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : k ∈ t₂) : + ¬k ∈ t₁ \ t₂ := by + rw [← contains_eq_false_iff_not_mem] + simp only [SDiff.sdiff] + exact Impl.contains_diff!_eq_false_of_contains_right h₁ h₂ h + +theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := by + simp only [SDiff.sdiff] + exact ⟨@Impl.Equiv.diff!_left _ _ ⟨cmp⟩ t₁.inner t₂.inner t₃.inner _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := by + simp only [SDiff.sdiff] + exact ⟨@Impl.Equiv.diff!_right _ _ ⟨cmp⟩ t₁.inner t₂.inner t₃.inner _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := by + simp only [SDiff.sdiff] + exact ⟨@Impl.Equiv.diff!_congr _ _ ⟨cmp⟩ t₁.inner t₂.inner t₃.inner t₄.inner _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩ + +/- get? -/ +theorem get?_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} : + (t₁ \ t₂).get? k = + if t₂.contains k then none else t₁.get? k := + Impl.get?_diff! h₁ h₂ + +theorem get?_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.get?_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem get?_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.get?_diff!_of_contains_eq_false_left h₁ h₂ h + +theorem get?_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : k ∈ t₂) : + (t₁ \ t₂).get? k = none := + Impl.get?_diff!_of_contains_right h₁ h₂ h + +/- get -/ +theorem get_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 := + Impl.get_diff! h₁ h₂ + +/- getD -/ +theorem getD_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β k} : + (t₁ \ t₂).getD k fallback = + if t₂.contains k then fallback else t₁.getD k fallback := + Impl.getD_diff! h₁ h₂ + +theorem getD_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β k} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getD_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem getD_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β k} (h : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := + Impl.getD_diff!_of_contains_right h₁ h₂ h + +theorem getD_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β k} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getD_diff!_of_contains_eq_false_left h₁ h₂ h + +/- get! -/ +theorem get!_diff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} [Inhabited (β k)] : + (t₁ \ t₂).get! k = + if t₂.contains k then default else t₁.get! k := + Impl.get!_diff! h₁ h₂ + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} [Inhabited (β k)] (h : ¬k ∈ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.get!_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem get!_diff_of_mem_right [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} [Inhabited (β k)] (h : k ∈ t₂) : + (t₁ \ t₂).get! k = default := + Impl.get!_diff!_of_contains_right h₁ h₂ h + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} [Inhabited (β k)] (h : ¬k ∈ t₁) : + (t₁ \ t₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.get!_diff!_of_contains_eq_false_left h₁ h₂ h + +/- getKey? -/ +theorem getKey?_diff [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} : + (t₁ \ t₂).getKey? k = + if t₂.contains k then none else t₁.getKey? k := + Impl.getKey?_diff! h₁ h₂ + +theorem getKey?_diff_of_not_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKey? k = t₁.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKey?_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem getKey?_diff_of_not_mem_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKey?_diff!_of_contains_eq_false_left h₁ h₂ h + +theorem getKey?_diff_of_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (h : k ∈ t₂) : + (t₁ \ t₂).getKey? k = none := + Impl.getKey?_diff!_of_contains_right h₁ h₂ h + +/- getKey -/ +theorem getKey_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).getKey k h_mem = + t₁.getKey k ((mem_diff_iff h₁ h₂).1 h_mem).1 := + Impl.getKey_diff! h₁ h₂ + +/- getKeyD -/ +theorem getKeyD_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} : + (t₁ \ t₂).getKeyD k fallback = + if t₂.contains k then fallback else t₁.getKeyD k fallback := + Impl.getKeyD_diff! h₁ h₂ + +theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKeyD_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem getKeyD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (h : k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = fallback := + Impl.getKeyD_diff!_of_contains_right h₁ h₂ h + +theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKeyD_diff!_of_contains_eq_false_left h₁ h₂ h + +/- getKey! -/ +theorem getKey!_diff [TransCmp cmp] [Inhabited α] + (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).getKey! k = + if t₂.contains k then default else t₁.getKey! k := + Impl.getKey!_diff! h₁ h₂ + +theorem getKey!_diff_of_not_mem_right [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (h : ¬k ∈ t₂) : + (t₁ \ t₂).getKey! k = t₁.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKey!_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem getKey!_diff_of_mem_right [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (h : k ∈ t₂) : + (t₁ \ t₂).getKey! k = default := + Impl.getKey!_diff!_of_contains_right h₁ h₂ h + +theorem getKey!_diff_of_not_mem_left [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (h : ¬k ∈ t₁) : + (t₁ \ t₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.getKey!_diff!_of_contains_eq_false_left h₁ h₂ h + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) : + (t₁ \ t₂).size ≤ t₁.size := + Impl.size_diff!_le_size_left h₁ h₂ + +theorem size_diff_eq_size_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) + (h : ∀ (a : α), a ∈ t₁ → ¬a ∈ t₂) : + (t₁ \ t₂).size = t₁.size := by + conv at h => + ext a + rhs + rw [← contains_eq_false_iff_not_mem] + exact Impl.size_diff!_eq_size_left h₁ h₂ h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + Impl.size_diff!_add_size_inter!_eq_size_left h₁ h₂ + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + Impl.isEmpty_diff!_left h₁ h₂ h + +theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := by + exact Impl.isEmpty_diff!_iff h₁ h₂ + +end Diff + +namespace Const + +variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β) cmp} + +/- get? -/ +theorem get?_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get? (m₁ \ m₂) k = + if m₂.contains k then none else Const.get? m₁ k := by + simp only [SDiff.sdiff] + exact Impl.Const.get?_diff! h₁ h₂ + +theorem get?_diff_of_not_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : ¬k ∈ m₂) : + Const.get? (m₁ \ m₂) k = Const.get? m₁ k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.get?_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem get?_diff_of_not_mem_left [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : ¬k ∈ m₁) : + Const.get? (m₁ \ m₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.get?_diff!_of_contains_eq_false_left h₁ h₂ h + +theorem get?_diff_of_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : k ∈ m₂) : + Const.get? (m₁ \ m₂) k = none := by + rw [mem_iff_contains] at h + simp only [SDiff.sdiff] + exact Impl.Const.get?_diff!_of_contains_right h₁ h₂ h + +/- get -/ +theorem get_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ \ m₂} : + Const.get (m₁ \ m₂) k h_mem = + Const.get m₁ k ((mem_diff_iff h₁ h₂).1 h_mem).1 := by + simp only [SDiff.sdiff] + exact Impl.Const.get_diff! h₁ h₂ + +/- getD -/ +theorem getD_diff [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} : + Const.getD (m₁ \ m₂) k fallback = + if m₂.contains k then fallback else Const.getD m₁ k fallback := by + simp only [SDiff.sdiff] + exact Impl.Const.getD_diff! h₁ h₂ + +theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : ¬k ∈ m₂) : + Const.getD (m₁ \ m₂) k fallback = Const.getD m₁ k fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.getD_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : k ∈ m₂) : + Const.getD (m₁ \ m₂) k fallback = fallback := by + rw [mem_iff_contains] at h + simp only [SDiff.sdiff] + exact Impl.Const.getD_diff!_of_contains_right h₁ h₂ h + +theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (h : ¬k ∈ m₁) : + Const.getD (m₁ \ m₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.getD_diff!_of_contains_eq_false_left h₁ h₂ h + +/- get! -/ +theorem get!_diff [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + Const.get! (m₁ \ m₂) k = + if m₂.contains k then default else Const.get! m₁ k := by + simp only [SDiff.sdiff] + exact Impl.Const.get!_diff! h₁ h₂ + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : ¬k ∈ m₂) : + Const.get! (m₁ \ m₂) k = Const.get! m₁ k := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.get!_diff!_of_contains_eq_false_right h₁ h₂ h + +theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : k ∈ m₂) : + Const.get! (m₁ \ m₂) k = default := by + rw [mem_iff_contains] at h + simp only [SDiff.sdiff] + exact Impl.Const.get!_diff!_of_contains_right h₁ h₂ h + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (h : ¬k ∈ m₁) : + Const.get! (m₁ \ m₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at h + simp only [SDiff.sdiff] + exact Impl.Const.get!_diff!_of_contains_eq_false_left h₁ h₂ h + +end Const + section Alter theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} diff --git a/src/Std/Data/DTreeMap/Raw/WF.lean b/src/Std/Data/DTreeMap/Raw/WF.lean index 5ae31dde35..d260d53aae 100644 --- a/src/Std/Data/DTreeMap/Raw/WF.lean +++ b/src/Std/Data/DTreeMap/Raw/WF.lean @@ -165,4 +165,8 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : (t₁ ∩ t₂).WF := ⟨Impl.WF.inter! h₁.out⟩ +theorem diff [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : + (t₁ \ t₂).WF := + ⟨Impl.WF.diff! h₁.out⟩ + end Std.DTreeMap.Raw.WF.Const diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean index 89085da941..e5d1afbb0a 100644 --- a/src/Std/Data/TreeMap/Basic.lean +++ b/src/Std/Data/TreeMap/Basic.lean @@ -501,6 +501,12 @@ def inter (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp := instance : Inter (TreeMap α β cmp) := ⟨inter⟩ +@[inline, inherit_doc DTreeMap.diff] +def diff (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp := + letI : Ord α := ⟨cmp⟩; ⟨DTreeMap.diff t₁.inner t₂.inner⟩ + +instance : SDiff (TreeMap α β cmp) := ⟨diff⟩ + @[inline, inherit_doc DTreeMap.Const.insertManyIfNewUnit] def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : TreeMap α Unit cmp) (l : ρ) : TreeMap α Unit cmp := ⟨DTreeMap.Const.insertManyIfNewUnit t.inner l⟩ diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 50738d31b5..260d565f9e 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -1961,6 +1961,221 @@ theorem isEmpty_inter_iff [TransCmp cmp] : end Inter +section Diff + +variable {t₁ t₂ : TreeMap α β cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := + DTreeMap.contains_diff + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂ := + DTreeMap.mem_diff_iff + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] {k : α} + (not_mem : k ∉ t₁) : + k ∉ t₁ \ t₂ := + DTreeMap.not_mem_diff_of_not_mem_left not_mem + +theorem not_mem_diff_of_mem_right [TransCmp cmp] {k : α} + (mem : k ∈ t₂) : + k ∉ t₁ \ t₂ := + DTreeMap.not_mem_diff_of_mem_right mem + +/- Equiv -/ +theorem Equiv.diff_left {t₃ : TreeMap α β cmp} [TransCmp cmp] + (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := by + constructor + apply DTreeMap.Equiv.diff_left equiv.1 + +theorem Equiv.diff_right {t₃ : TreeMap α β cmp} [TransCmp cmp] + (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := by + constructor + apply DTreeMap.Equiv.diff_right equiv.1 + +theorem Equiv.diff_congr {t₃ t₄ : TreeMap α β cmp} [TransCmp cmp] + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := by + constructor + apply DTreeMap.Equiv.diff_congr equiv₁.1 equiv₂.1 + +/- get? -/ +theorem get?_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).get? k = + if k ∈ t₂ then none else t₁.get? k := + DTreeMap.Const.get?_diff + +theorem get?_diff_of_not_mem_right [TransCmp cmp] + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := + DTreeMap.Const.get?_diff_of_not_mem_right not_mem + +theorem get?_diff_of_not_mem_left [TransCmp cmp] + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get? k = none := + DTreeMap.Const.get?_diff_of_not_mem_left not_mem + +theorem get?_diff_of_mem_right [TransCmp cmp] + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get? k = none := + DTreeMap.Const.get?_diff_of_mem_right mem + +/- get -/ +theorem get_diff [TransCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k (mem_diff_iff.1 h_mem).1 := + DTreeMap.Const.get_diff + +/- getD -/ +theorem getD_diff [TransCmp cmp] {k : α} {fallback : β} : + (t₁ \ t₂).getD k fallback = + if k ∈ t₂ then fallback else t₁.getD k fallback := + DTreeMap.Const.getD_diff + +theorem getD_diff_of_not_mem_right [TransCmp cmp] + {k : α} {fallback : β} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := + DTreeMap.Const.getD_diff_of_not_mem_right not_mem + +theorem getD_diff_of_mem_right [TransCmp cmp] + {k : α} {fallback : β} (mem : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := + DTreeMap.Const.getD_diff_of_mem_right mem + +theorem getD_diff_of_not_mem_left [TransCmp cmp] + {k : α} {fallback : β} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getD k fallback = fallback := + DTreeMap.Const.getD_diff_of_not_mem_left not_mem + +/- get! -/ +theorem get!_diff [TransCmp cmp] {k : α} [Inhabited β] : + (t₁ \ t₂).get! k = + if k ∈ t₂ then default else t₁.get! k := + DTreeMap.Const.get!_diff + +theorem get!_diff_of_not_mem_right [TransCmp cmp] + {k : α} [Inhabited β] (not_mem : k ∉ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := + DTreeMap.Const.get!_diff_of_not_mem_right not_mem + +theorem get!_diff_of_mem_right [TransCmp cmp] + {k : α} [Inhabited β] (mem : k ∈ t₂) : + (t₁ \ t₂).get! k = default := + DTreeMap.Const.get!_diff_of_mem_right mem + +theorem get!_diff_of_not_mem_left [TransCmp cmp] + {k : α} [Inhabited β] (not_mem : k ∉ t₁) : + (t₁ \ t₂).get! k = default := + DTreeMap.Const.get!_diff_of_not_mem_left not_mem + +/- getKey? -/ +theorem getKey?_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).getKey? k = + if k ∈ t₂ then none else t₁.getKey? k := + DTreeMap.getKey?_diff + +theorem getKey?_diff_of_not_mem_right [TransCmp cmp] + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKey? k = t₁.getKey? k := + DTreeMap.getKey?_diff_of_not_mem_right not_mem + +theorem getKey?_diff_of_not_mem_left [TransCmp cmp] + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKey? k = none := + DTreeMap.getKey?_diff_of_not_mem_left not_mem + +theorem getKey?_diff_of_mem_right [TransCmp cmp] + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKey? k = none := + DTreeMap.getKey?_diff_of_mem_right mem + +/- getKey -/ +theorem getKey_diff [TransCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).getKey k h_mem = + t₁.getKey k (mem_diff_iff.1 h_mem).1 := + DTreeMap.getKey_diff + +/- getKeyD -/ +theorem getKeyD_diff [TransCmp cmp] {k fallback : α} : + (t₁ \ t₂).getKeyD k fallback = + if k ∈ t₂ then fallback else t₁.getKeyD k fallback := + DTreeMap.getKeyD_diff + +theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] + {k fallback : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := + DTreeMap.getKeyD_diff_of_not_mem_right not_mem + +theorem getKeyD_diff_of_mem_right [TransCmp cmp] + {k fallback : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = fallback := + DTreeMap.getKeyD_diff_of_mem_right mem + +theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] + {k fallback : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKeyD k fallback = fallback := + DTreeMap.getKeyD_diff_of_not_mem_left not_mem + +/- getKey! -/ +theorem getKey!_diff [TransCmp cmp] [Inhabited α] {k : α} : + (t₁ \ t₂).getKey! k = + if k ∈ t₂ then default else t₁.getKey! k := + DTreeMap.getKey!_diff + +theorem getKey!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α] + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKey! k = t₁.getKey! k := + DTreeMap.getKey!_diff_of_not_mem_right not_mem + +theorem getKey!_diff_of_mem_right [TransCmp cmp] [Inhabited α] + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKey! k = default := + DTreeMap.getKey!_diff_of_mem_right mem + +theorem getKey!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α] + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKey! k = default := + DTreeMap.getKey!_diff_of_not_mem_left not_mem + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] : + (t₁ \ t₂).size ≤ t₁.size := + DTreeMap.size_diff_le_size_left + +theorem size_diff_eq_size_left [TransCmp cmp] + (h : ∀ (a : α), a ∈ t₁ → a ∉ t₂) : + (t₁ \ t₂).size = t₁.size := + DTreeMap.size_diff_eq_size_left h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + DTreeMap.size_diff_add_size_inter_eq_size_left + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + DTreeMap.isEmpty_diff_left h + +theorem isEmpty_diff_iff [TransCmp cmp] : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := + DTreeMap.isEmpty_diff_iff + +end Diff + section Alter theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] {k : α} diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean index 4fd241f1b3..4a165fe1b8 100644 --- a/src/Std/Data/TreeMap/Raw/Basic.lean +++ b/src/Std/Data/TreeMap/Raw/Basic.lean @@ -503,6 +503,12 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp := instance : Inter (Raw α β cmp) := ⟨inter⟩ +@[inline, inherit_doc DTreeMap.Raw.diff] +def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp := + ⟨DTreeMap.Raw.diff t₁.inner t₂.inner⟩ + +instance : SDiff (Raw α β cmp) := ⟨diff⟩ + @[inline, inherit_doc DTreeMap.Raw.Const.insertManyIfNewUnit] def insertManyIfNewUnit {ρ} [ForIn Id ρ α] (t : Raw α Unit cmp) (l : ρ) : Raw α Unit cmp := ⟨DTreeMap.Raw.Const.insertManyIfNewUnit t.inner l⟩ diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 81d84eac40..636374c70f 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -2012,6 +2012,231 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : end Inter +section Diff + +variable {t₁ t₂ : Raw α β cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := + DTreeMap.Raw.contains_diff h₁ h₂ + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂ := + DTreeMap.Raw.mem_diff_iff h₁ h₂ + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (not_mem : k ∉ t₁) : + k ∉ t₁ \ t₂ := + DTreeMap.Raw.not_mem_diff_of_not_mem_left h₁ h₂ not_mem + +theorem not_mem_diff_of_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (mem : k ∈ t₂) : + k ∉ t₁ \ t₂ := + DTreeMap.Raw.not_mem_diff_of_mem_right h₁ h₂ mem + +/- Equiv -/ + +theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := + ⟨DTreeMap.Raw.Equiv.diff_left h₁ h₂ h₃ equiv.1⟩ + +theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := + ⟨DTreeMap.Raw.Equiv.diff_right h₁ h₂ h₃ equiv.1⟩ + +theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α β cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := + ⟨DTreeMap.Raw.Equiv.diff_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1⟩ + +/- get? -/ +theorem get?_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).get? k = + if k ∈ t₂ then none else t₁.get? k := + DTreeMap.Raw.Const.get?_diff h₁ h₂ + +theorem get?_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := + DTreeMap.Raw.Const.get?_diff_of_not_mem_right h₁ h₂ not_mem + +theorem get?_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get? k = none := + DTreeMap.Raw.Const.get?_diff_of_not_mem_left h₁ h₂ not_mem + +theorem get?_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get? k = none := + DTreeMap.Raw.Const.get?_diff_of_mem_right h₁ h₂ mem + +/- get -/ +theorem get_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 := + DTreeMap.Raw.Const.get_diff h₁ h₂ + +/- getD -/ +theorem getD_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β} : + (t₁ \ t₂).getD k fallback = + if k ∈ t₂ then fallback else t₁.getD k fallback := + DTreeMap.Raw.Const.getD_diff h₁ h₂ + +theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := + DTreeMap.Raw.Const.getD_diff_of_not_mem_right h₁ h₂ not_mem + +theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β} (mem : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := + DTreeMap.Raw.Const.getD_diff_of_mem_right h₁ h₂ mem + +theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {fallback : β} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getD k fallback = fallback := + DTreeMap.Raw.Const.getD_diff_of_not_mem_left h₁ h₂ not_mem + +/- get! -/ +theorem get!_diff [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).get! k = + if k ∈ t₂ then default else t₁.get! k := + DTreeMap.Raw.Const.get!_diff h₁ h₂ + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := + DTreeMap.Raw.Const.get!_diff_of_not_mem_right h₁ h₂ not_mem + +theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get! k = default := + DTreeMap.Raw.Const.get!_diff_of_mem_right h₁ h₂ mem + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get! k = default := + DTreeMap.Raw.Const.get!_diff_of_not_mem_left h₁ h₂ not_mem + +/- getKey? -/ +theorem getKey?_diff [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).getKey? k = + if k ∈ t₂ then none else t₁.getKey? k := + DTreeMap.Raw.getKey?_diff h₁ h₂ + +theorem getKey?_diff_of_not_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKey? k = t₁.getKey? k := + DTreeMap.Raw.getKey?_diff_of_not_mem_right h₁ h₂ not_mem + +theorem getKey?_diff_of_not_mem_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKey? k = none := + DTreeMap.Raw.getKey?_diff_of_not_mem_left h₁ h₂ not_mem + +theorem getKey?_diff_of_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKey? k = none := + DTreeMap.Raw.getKey?_diff_of_mem_right h₁ h₂ mem + +/- getKey -/ +theorem getKey_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).getKey k h_mem = + t₁.getKey k ((mem_diff_iff h₁ h₂).1 h_mem).1 := + DTreeMap.Raw.getKey_diff h₁ h₂ + +/- getKeyD -/ +theorem getKeyD_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} : + (t₁ \ t₂).getKeyD k fallback = + if k ∈ t₂ then fallback else t₁.getKeyD k fallback := + DTreeMap.Raw.getKeyD_diff h₁ h₂ + +theorem getKeyD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKeyD k fallback = t₁.getKeyD k fallback := + DTreeMap.Raw.getKeyD_diff_of_not_mem_right h₁ h₂ not_mem + +theorem getKeyD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKeyD k fallback = fallback := + DTreeMap.Raw.getKeyD_diff_of_mem_right h₁ h₂ mem + +theorem getKeyD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKeyD k fallback = fallback := + DTreeMap.Raw.getKeyD_diff_of_not_mem_left h₁ h₂ not_mem + +/- getKey! -/ +theorem getKey!_diff [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).getKey! k = + if k ∈ t₂ then default else t₁.getKey! k := + DTreeMap.Raw.getKey!_diff h₁ h₂ + +theorem getKey!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getKey! k = t₁.getKey! k := + DTreeMap.Raw.getKey!_diff_of_not_mem_right h₁ h₂ not_mem + +theorem getKey!_diff_of_mem_right [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getKey! k = default := + DTreeMap.Raw.getKey!_diff_of_mem_right h₁ h₂ mem + +theorem getKey!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getKey! k = default := + DTreeMap.Raw.getKey!_diff_of_not_mem_left h₁ h₂ not_mem + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).size ≤ t₁.size := + DTreeMap.Raw.size_diff_le_size_left h₁ h₂ + +theorem size_diff_eq_size_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + (h : ∀ (a : α), a ∈ t₁ → a ∉ t₂) : + (t₁ \ t₂).size = t₁.size := + DTreeMap.Raw.size_diff_eq_size_left h₁ h₂ h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + DTreeMap.Raw.size_diff_add_size_inter_eq_size_left h₁ h₂ + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + DTreeMap.Raw.isEmpty_diff_left h₁ h₂ h + +theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := + DTreeMap.Raw.isEmpty_diff_iff h₁ h₂ + +end Diff + section Alter theorem isEmpty_alter_eq_isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} diff --git a/src/Std/Data/TreeMap/Raw/WF.lean b/src/Std/Data/TreeMap/Raw/WF.lean index 7a16006c7a..a4ce608e28 100644 --- a/src/Std/Data/TreeMap/Raw/WF.lean +++ b/src/Std/Data/TreeMap/Raw/WF.lean @@ -123,4 +123,8 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : (t₁ ∩ t₂).WF := ⟨InnerWF.inter h₁⟩ +theorem diff [TransCmp cmp] {t₁ t₂ : Raw α β cmp} (h₁ : t₁.WF) : + (t₁ \ t₂).WF := + ⟨InnerWF.diff h₁⟩ + end Std.TreeMap.Raw.WF diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean index 7aa106c38f..7f6b98e367 100644 --- a/src/Std/Data/TreeSet/Basic.lean +++ b/src/Std/Data/TreeSet/Basic.lean @@ -503,6 +503,16 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp := instance : Inter (TreeSet α cmp) := ⟨inter⟩ +/-- +Computes the difference of the given tree sets. + +This function always iterates through the smaller set. +-/ +def diff (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp := + ⟨TreeMap.diff t₁.inner t₂.inner⟩ + +instance : SDiff (TreeSet α cmp) := ⟨diff⟩ + /-- Erases multiple items from the tree set by iterating over the given collection and calling erase. -/ diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 55fe1c5686..2de31e600c 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -772,6 +772,151 @@ theorem isEmpty_inter_iff [TransCmp cmp] : end Inter +section Diff + +variable {t₁ t₂ : TreeSet α cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := + TreeMap.contains_diff + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂ := + TreeMap.mem_diff_iff + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] {k : α} + (not_mem : k ∉ t₁) : + k ∉ t₁ \ t₂ := + TreeMap.not_mem_diff_of_not_mem_left not_mem + +theorem not_mem_diff_of_mem_right [TransCmp cmp] {k : α} + (mem : k ∈ t₂) : + k ∉ t₁ \ t₂ := + TreeMap.not_mem_diff_of_mem_right mem + +/- Equiv -/ +theorem Equiv.diff_left {t₃ : TreeSet α cmp} [TransCmp cmp] + (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := by + constructor + apply TreeMap.Equiv.diff_left equiv.1 + +theorem Equiv.diff_right {t₃ : TreeSet α cmp} [TransCmp cmp] + (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := by + constructor + apply TreeMap.Equiv.diff_right equiv.1 + +theorem Equiv.diff_congr {t₃ t₄ : TreeSet α cmp} [TransCmp cmp] + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := by + constructor + apply TreeMap.Equiv.diff_congr equiv₁.1 equiv₂.1 + +/- get? -/ +theorem get?_diff [TransCmp cmp] {k : α} : + (t₁ \ t₂).get? k = + if k ∈ t₂ then none else t₁.get? k := + TreeMap.getKey?_diff + +theorem get?_diff_of_not_mem_right [TransCmp cmp] + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := + TreeMap.getKey?_diff_of_not_mem_right not_mem + +theorem get?_diff_of_not_mem_left [TransCmp cmp] + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get? k = none := + TreeMap.getKey?_diff_of_not_mem_left not_mem + +theorem get?_diff_of_mem_right [TransCmp cmp] + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get? k = none := + TreeMap.getKey?_diff_of_mem_right mem + +/- get -/ +theorem get_diff [TransCmp cmp] + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k (mem_diff_iff.1 h_mem).1 := + TreeMap.getKey_diff + +/- getD -/ +theorem getD_diff [TransCmp cmp] {k fallback : α} : + (t₁ \ t₂).getD k fallback = + if k ∈ t₂ then fallback else t₁.getD k fallback := + TreeMap.getKeyD_diff + +theorem getD_diff_of_not_mem_right [TransCmp cmp] + {k fallback : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := + TreeMap.getKeyD_diff_of_not_mem_right not_mem + +theorem getD_diff_of_mem_right [TransCmp cmp] + {k fallback : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := + TreeMap.getKeyD_diff_of_mem_right mem + +theorem getD_diff_of_not_mem_left [TransCmp cmp] + {k fallback : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getD k fallback = fallback := + TreeMap.getKeyD_diff_of_not_mem_left not_mem + +/- get! -/ +theorem get!_diff [TransCmp cmp] [Inhabited α] {k : α} : + (t₁ \ t₂).get! k = + if k ∈ t₂ then default else t₁.get! k := + TreeMap.getKey!_diff + +theorem get!_diff_of_not_mem_right [TransCmp cmp] [Inhabited α] + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := + TreeMap.getKey!_diff_of_not_mem_right not_mem + +theorem get!_diff_of_mem_right [TransCmp cmp] [Inhabited α] + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get! k = default := + TreeMap.getKey!_diff_of_mem_right mem + +theorem get!_diff_of_not_mem_left [TransCmp cmp] [Inhabited α] + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get! k = default := + TreeMap.getKey!_diff_of_not_mem_left not_mem + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] : + (t₁ \ t₂).size ≤ t₁.size := + TreeMap.size_diff_le_size_left + +theorem size_diff_eq_size_left [TransCmp cmp] + (h : ∀ (a : α), a ∈ t₁ → a ∉ t₂) : + (t₁ \ t₂).size = t₁.size := + TreeMap.size_diff_eq_size_left h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + TreeMap.size_diff_add_size_inter_eq_size_left + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + TreeMap.isEmpty_diff_left h + +theorem isEmpty_diff_iff [TransCmp cmp] : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := + TreeMap.isEmpty_diff_iff + +end Diff + section monadic variable {δ : Type w} {m : Type w → Type w'} diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean index 19d4b5f251..6341c9c639 100644 --- a/src/Std/Data/TreeSet/Raw/Basic.lean +++ b/src/Std/Data/TreeSet/Raw/Basic.lean @@ -353,6 +353,16 @@ def inter (t₁ t₂ : Raw α cmp) : Raw α cmp := instance : Inter (Raw α cmp) := ⟨inter⟩ +/-- +Computes the difference of the given tree sets. + +This function always iterates through the smaller set. +-/ +def diff (t₁ t₂ : Raw α cmp) : Raw α cmp := + letI : Ord α := ⟨cmp⟩; ⟨TreeMap.Raw.diff t₁.inner t₂.inner⟩ + +instance : SDiff (Raw α cmp) := ⟨diff⟩ + @[inline, inherit_doc TreeSet.empty] def eraseMany {ρ} [ForIn Id ρ α] (t : Raw α cmp) (l : ρ) : Raw α cmp := diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 1eb2ea122f..b54ebe2371 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -811,6 +811,166 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : end Inter +section Diff + +variable {t₁ t₂ : Raw α cmp} + +@[simp] +theorem diff_eq : t₁.diff t₂ = t₁ \ t₂ := by + simp only [SDiff.sdiff] + +/- contains -/ +@[simp] +theorem contains_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).contains k = (t₁.contains k && !t₂.contains k) := + TreeMap.Raw.contains_diff h₁ h₂ + +/- mem -/ +@[simp] +theorem mem_diff_iff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + k ∈ t₁ \ t₂ ↔ k ∈ t₁ ∧ k ∉ t₂ := + TreeMap.Raw.mem_diff_iff h₁ h₂ + +theorem not_mem_diff_of_not_mem_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (not_mem : k ∉ t₁) : + k ∉ t₁ \ t₂ := + TreeMap.Raw.not_mem_diff_of_not_mem_left h₁ h₂ not_mem + +theorem not_mem_diff_of_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (mem : k ∈ t₂) : + k ∉ t₁ \ t₂ := + TreeMap.Raw.not_mem_diff_of_mem_right h₁ h₂ mem + +theorem Equiv.diff_left [TransCmp cmp] {t₃ : Raw α cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₁ ~m t₂) : + (t₁ \ t₃).Equiv (t₂ \ t₃) := + ⟨TreeMap.Raw.Equiv.diff_left h₁ h₂ h₃ equiv.1⟩ + +theorem Equiv.diff_right [TransCmp cmp] {t₃ : Raw α cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (equiv : t₂ ~m t₃) : + (t₁ \ t₂).Equiv (t₁ \ t₃) := + ⟨TreeMap.Raw.Equiv.diff_right h₁ h₂ h₃ equiv.1⟩ + +theorem Equiv.diff_congr [TransCmp cmp] {t₃ t₄ : Raw α cmp} + (h₁ : t₁.WF) (h₂ : t₂.WF) (h₃ : t₃.WF) (h₄ : t₄.WF) + (equiv₁ : t₁ ~m t₃) (equiv₂ : t₂ ~m t₄) : + (t₁ \ t₂).Equiv (t₃ \ t₄) := + ⟨TreeMap.Raw.Equiv.diff_congr h₁ h₂ h₃ h₄ equiv₁.1 equiv₂.1⟩ + +/- get? -/ +theorem get?_diff [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} : + (t₁ \ t₂).get? k = + if k ∈ t₂ then none else t₁.get? k := + TreeMap.Raw.getKey?_diff h₁ h₂ + +theorem get?_diff_of_not_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).get? k = t₁.get? k := + TreeMap.Raw.getKey?_diff_of_not_mem_right h₁ h₂ not_mem + +theorem get?_diff_of_not_mem_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).get? k = none := + TreeMap.Raw.getKey?_diff_of_not_mem_left h₁ h₂ not_mem + +theorem get?_diff_of_mem_right [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} (mem : k ∈ t₂) : + (t₁ \ t₂).get? k = none := + TreeMap.Raw.getKey?_diff_of_mem_right h₁ h₂ mem + +/- get -/ +theorem get_diff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) + {k : α} {h_mem : k ∈ t₁ \ t₂} : + (t₁ \ t₂).get k h_mem = + t₁.get k ((mem_diff_iff h₁ h₂).1 h_mem).1 := + TreeMap.Raw.getKey_diff h₁ h₂ + +/- getD -/ +theorem getD_diff [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} : + (t₁ \ t₂).getD k fallback = + if k ∈ t₂ then fallback else t₁.getD k fallback := + TreeMap.Raw.getKeyD_diff h₁ h₂ + +theorem getD_diff_of_not_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (not_mem : k ∉ t₂) : + (t₁ \ t₂).getD k fallback = t₁.getD k fallback := + TreeMap.Raw.getKeyD_diff_of_not_mem_right h₁ h₂ not_mem + +theorem getD_diff_of_mem_right [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (mem : k ∈ t₂) : + (t₁ \ t₂).getD k fallback = fallback := + TreeMap.Raw.getKeyD_diff_of_mem_right h₁ h₂ mem + +theorem getD_diff_of_not_mem_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) {k fallback : α} (not_mem : k ∉ t₁) : + (t₁ \ t₂).getD k fallback = fallback := + TreeMap.Raw.getKeyD_diff_of_not_mem_left h₁ h₂ not_mem + +/- get! -/ +theorem get!_diff [TransCmp cmp] [Inhabited α] + (h₁ : t₁.WF) + (h₂ : t₂.WF) {k : α} : + (t₁ \ t₂).get! k = + if k ∈ t₂ then default else t₁.get! k := + TreeMap.Raw.getKey!_diff h₁ h₂ + +theorem get!_diff_of_not_mem_right [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (not_mem : k ∉ t₂) : + (t₁ \ t₂).get! k = t₁.get! k := + TreeMap.Raw.getKey!_diff_of_not_mem_right h₁ h₂ not_mem + +theorem get!_diff_of_mem_right [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (mem : k ∈ t₂) : + (t₁ \ t₂).get! k = default := + TreeMap.Raw.getKey!_diff_of_mem_right h₁ h₂ mem + +theorem get!_diff_of_not_mem_left [Inhabited α] + [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} + (not_mem : k ∉ t₁) : + (t₁ \ t₂).get! k = default := + TreeMap.Raw.getKey!_diff_of_not_mem_left h₁ h₂ not_mem + +/- size -/ +theorem size_diff_le_size_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) : + (t₁ \ t₂).size ≤ t₁.size := + TreeMap.Raw.size_diff_le_size_left h₁ h₂ + +theorem size_diff_eq_size_left [TransCmp cmp] (h₁ : t₁.WF) + (h₂ : t₂.WF) + (h : ∀ (a : α), a ∈ t₁ → a ∉ t₂) : + (t₁ \ t₂).size = t₁.size := + TreeMap.Raw.size_diff_eq_size_left h₁ h₂ h + +theorem size_diff_add_size_inter_eq_size_left [TransCmp cmp] + (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).size + (t₁ ∩ t₂).size = t₁.size := + TreeMap.Raw.size_diff_add_size_inter_eq_size_left h₁ h₂ + +/- isEmpty -/ +@[simp] +theorem isEmpty_diff_left [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.isEmpty) : + (t₁ \ t₂).isEmpty = true := + TreeMap.Raw.isEmpty_diff_left h₁ h₂ h + +theorem isEmpty_diff_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + (t₁ \ t₂).isEmpty ↔ ∀ k, k ∈ t₁ → k ∈ t₂ := + TreeMap.Raw.isEmpty_diff_iff h₁ h₂ + +end Diff + section monadic variable {δ : Type w} {m : Type w → Type w'} diff --git a/src/Std/Data/TreeSet/Raw/WF.lean b/src/Std/Data/TreeSet/Raw/WF.lean index ce6236e20c..eea2d4bd1b 100644 --- a/src/Std/Data/TreeSet/Raw/WF.lean +++ b/src/Std/Data/TreeSet/Raw/WF.lean @@ -87,4 +87,8 @@ theorem inter [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) : (t₁ ∩ t₂).WF := ⟨InnerWF.inter h₁⟩ +theorem diff [TransCmp cmp] {t₁ t₂ : Raw α cmp} (h₁ : t₁.WF) : + (t₁ \ t₂).WF := + ⟨InnerWF.diff h₁⟩ + end Std.TreeSet.Raw.WF