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 <markus@himmel-villmar.de>
This commit is contained in:
Wojciech Różowski
GitHub
parent
ca23ed0c17
commit
2da5b528b7
19 changed files with 2385 additions and 2 deletions
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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 : α}
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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 : α}
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 : α}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 : α}
|
||||
|
|
|
|||
|
|
@ -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⟩
|
||||
|
|
|
|||
|
|
@ -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 : α}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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.
|
||||
-/
|
||||
|
|
|
|||
|
|
@ -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'}
|
||||
|
|
|
|||
|
|
@ -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 :=
|
||||
|
|
|
|||
|
|
@ -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'}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue