From af741abbf5ef83b4cdfa089e4d0b897cece2a756 Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Mon, 24 Feb 2025 16:34:37 +0100 Subject: [PATCH] feat: TreeMap lemmas for 'get?' (#7167) This PR provides tree map lemmas for the interaction of `get?` with the other operations for which lemmas already exist. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 159 ++++++++++++++++++++- src/Std/Data/DTreeMap/Lemmas.lean | 102 +++++++++++++ src/Std/Data/DTreeMap/RawLemmas.lean | 102 +++++++++++++ src/Std/Data/HashMap/Lemmas.lean | 8 +- src/Std/Data/HashMap/RawLemmas.lean | 8 +- src/Std/Data/TreeMap/Lemmas.lean | 51 +++++++ src/Std/Data/TreeMap/RawLemmas.lean | 51 +++++++ 7 files changed, 466 insertions(+), 15 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index fa63b3f1cc..bb07a9efb5 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -25,11 +25,17 @@ universe u v namespace Std.DTreeMap.Internal.Impl variable {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Impl α β} +private local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ + +attribute [local instance] beqOfOrd +attribute [local instance] equivBEq_of_transOrd +attribute [local instance] lawfulBEq_of_lawfulEqOrd /-- Internal implementation detail of the tree map -/ scoped macro "wf_trivial" : tactic => `(tactic| repeat (first - | apply WF.ordered | apply WF.balanced | apply WF.insert | apply WF.insert! + | apply WF.ordered | apply WF.balanced | apply WF.empty + | apply WF.insert | apply WF.insert! | apply WF.insertIfNew | apply WF.insertIfNew! | apply WF.erase | apply WF.erase! | apply Ordered.distinctKeys @@ -41,8 +47,21 @@ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] open Lean +theorem compare_eq_eq_iff_beq {k a : α} : compare k a = .eq ↔ k == a := beq_iff_eq.symm + +theorem dif_compare {γ} [LawfulEqOrd α] {k a : α} {f : compare k a = .eq → γ} {g : ¬ compare k a = .eq → γ} : + (if h : compare k a = .eq then f h else g h) = + (if h : k == a then f (eq_of_beq h) else g (h ∘ beq_of_eq)) := by + split + · exact Eq.symm <| dif_pos (beq_of_eq ‹_› :) + · exact Eq.symm <| dif_neg (‹_› ∘ eq_of_beq :) + +private def helperLemmaNames : Array Name := + #[``dif_compare, ``compare_eq_eq_iff_beq] + private def queryNames : Array Name := - #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length] + #[``isEmpty_eq_isEmpty, ``contains_eq_containsKey, ``size_eq_length, + ``get?_eq_getValueCast?, ``Const.get?_eq_getValue?] private def modifyMap : Std.HashMap Name Name := .ofList @@ -74,13 +93,11 @@ macro_rules congrModify := congrModify.push (← `($congr:term ($(mkIdent modify) ..))) `(tactic| (simp (discharger := wf_trivial) only - [$[$(Array.map Lean.mkIdent queryNames):term],*, $[$congrModify:term],*] + [$[$(Array.map Lean.mkIdent helperLemmaNames):term],*, + $[$(Array.map Lean.mkIdent queryNames):term],*, $[$congrModify:term],*] $[apply $(using?.toArray):term];*) <;> wf_trivial) -attribute [local instance] beqOfOrd -attribute [local instance] equivBEq_of_transOrd - theorem isEmpty_empty : isEmpty (empty : Impl α β) := by simp [Impl.isEmpty_eq_isEmpty] @@ -97,7 +114,7 @@ theorem mem_iff_contains {k : α} : k ∈ t ↔ t.contains k := theorem contains_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) : t.contains k = t.contains k' := by - rw [← beq_iff_eq (b := Ordering.eq), ← beq_eq] at hab + revert hab simp_to_model using List.containsKey_congr theorem mem_congr [TransOrd α] (h : t.WF) {k k' : α} (hab : compare k k' = .eq) : @@ -409,4 +426,132 @@ theorem size_insertIfNew!_le [TransOrd α] (h : t.WF) {k : α} {v : β k} : (t.insertIfNew! k v).size ≤ t.size + 1 := by simp_to_model [insertIfNew!] using List.length_insertEntryIfNew_le +theorem get?_empty [TransOrd α] [LawfulEqOrd α] {a : α} : (empty : Impl α β).get? a = none := by + simp_to_model using List.getValueCast?_nil + +theorem get?_of_isEmpty [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : + t.isEmpty = true → t.get? a = none := by + simp_to_model; empty + +theorem get?_insert [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a k : α} {v : β k} : + (t.insert k v h.balanced).impl.get? a = + if h : compare k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a := by + simp_to_model [insert] using List.getValueCast?_insertEntry + +theorem get?_insert! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a k : α} {v : β k} : + (t.insert! k v).get? a = + if h : compare k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a := by + simp_to_model [insert!] using List.getValueCast?_insertEntry + +theorem get?_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert k v h.balanced).impl.get? k = some v := by + simp_to_model [insert] using List.getValueCast?_insertEntry_self + +theorem get?_insert!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert! k v).get? k = some v := by + simp_to_model [insert!] using List.getValueCast?_insertEntry_self + +theorem contains_eq_isSome_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : + t.contains a = (t.get? a).isSome := by + simp_to_model using List.containsKey_eq_isSome_getValueCast? + +theorem mem_iff_isSome_get? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : + a ∈ t ↔ (t.get? a).isSome := by + simpa [mem_iff_contains] using contains_eq_isSome_get? h + +theorem get?_eq_none_of_contains_eq_false [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : + t.contains a = false → t.get? a = none := by + simp_to_model using List.getValueCast?_eq_none + +theorem get?_eq_none [TransOrd α] [LawfulEqOrd α] (h : t.WF) {a : α} : + ¬ a ∈ t → t.get? a = none := by + simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h + +theorem get?_erase [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} : + (t.erase k h.balanced).impl.get? a = if compare k a = .eq then none else t.get? a := by + simp_to_model [erase] using List.getValueCast?_eraseKey + +theorem get?_erase! [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k a : α} : + (t.erase! k).get? a = if compare k a = .eq then none else t.get? a := by + simp_to_model [erase!] using List.getValueCast?_eraseKey + +theorem get?_erase_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} : + (t.erase k h.balanced).impl.get? k = none := by + simp_to_model [erase] using List.getValueCast?_eraseKey_self + +theorem get?_erase!_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} : + (t.erase! k).get? k = none := by + simp_to_model [erase!] using List.getValueCast?_eraseKey_self + +namespace Const + +variable {β : Type v} {t : Impl α β} + +theorem get?_empty [TransOrd α] {a : α} : get? a (empty : Impl α β) = none := by + simp_to_model using List.getValue?_nil + +theorem get?_of_isEmpty [TransOrd α] (h : t.WF) {a : α} : + t.isEmpty = true → get? a t = none := by + simp_to_model; empty + +theorem get?_insert [TransOrd α] (h : t.WF) {a k : α} {v : β} : + get? a (t.insert k v h.balanced).impl = + if compare k a = .eq then some v else get? a t := by + simp_to_model [insert] using List.getValue?_insertEntry + +theorem get?_insert! [TransOrd α] (h : t.WF) {a k : α} {v : β} : + get? a (t.insert! k v) = + if compare k a = .eq then some v else get? a t := by + simp_to_model [insert!] using List.getValue?_insertEntry + +theorem get?_insert_self [TransOrd α] (h : t.WF) {k : α} {v : β} : + get? k (t.insert k v h.balanced).impl = some v := by + simp_to_model [insert] using List.getValue?_insertEntry_self + +theorem get?_insert!_self [TransOrd α] (h : t.WF) {k : α} {v : β} : + get? k (t.insert! k v) = some v := by + simp_to_model [insert!] using List.getValue?_insertEntry_self + +theorem contains_eq_isSome_get? [TransOrd α] (h : t.WF) {a : α} : + t.contains a = (get? a t).isSome := by + simp_to_model using List.containsKey_eq_isSome_getValue? + +theorem mem_iff_isSome_get? [TransOrd α] (h : t.WF) {a : α} : + a ∈ t ↔ (get? a t).isSome := by + simpa [mem_iff_contains] using contains_eq_isSome_get? h + +theorem get?_eq_none_of_contains_eq_false [TransOrd α] (h : t.WF) {a : α} : + t.contains a = false → get? a t = none := by + simp_to_model using List.getValue?_eq_none.mpr + +theorem get?_eq_none [TransOrd α] (h : t.WF) {a : α} : + ¬ a ∈ t → get? a t = none := by + simpa [mem_iff_contains] using get?_eq_none_of_contains_eq_false h + +theorem get?_erase [TransOrd α] (h : t.WF) {k a : α} : + get? a (t.erase k h.balanced).impl = if compare k a = .eq then none else get? a t := by + simp_to_model [erase] using List.getValue?_eraseKey + +theorem get?_erase! [TransOrd α] (h : t.WF) {k a : α} : + get? a (t.erase! k) = if compare k a = .eq then none else get? a t := by + simp_to_model [erase!] using List.getValue?_eraseKey + +theorem get?_erase_self [TransOrd α] (h : t.WF) {k : α} : + get? k (t.erase k h.balanced).impl = none := by + simp_to_model [erase] using List.getValue?_eraseKey_self + +theorem get?_erase!_self [TransOrd α] (h : t.WF) {k : α} : + get? k (t.erase! k) = none := by + simp_to_model [erase!] using List.getValue?_eraseKey_self + +theorem get?_eq_get? [LawfulEqOrd α] [TransOrd α] (h : t.WF) {a : α} : get? a t = t.get? a := by + simp_to_model using List.getValue?_eq_getValueCast? + +theorem get?_congr [TransOrd α] (h : t.WF) {a b : α} (hab : compare a b = .eq) : + get? a t = get? b t := by + revert hab + simp_to_model using List.getValue?_congr + +end Const + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index b94a547c63..655b2864e1 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -24,6 +24,7 @@ universe u v namespace Std.DTreeMap variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap α β cmp} +private local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ private theorem ext {t t' : DTreeMap α β cmp} : t.inner = t'.inner → t = t' := by cases t; cases t'; rintro rfl; rfl @@ -237,4 +238,105 @@ theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β k} : (t.insertIfNew k v).size ≤ t.size + 1 := Impl.size_insertIfNew_le t.wf +@[simp] +theorem get?_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + (∅ : DTreeMap α β cmp).get? a = none := + Impl.get?_empty + +theorem get?_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + t.isEmpty = true → t.get? a = none := + Impl.get?_of_isEmpty t.wf + +theorem get?_insert [TransCmp cmp] [LawfulEqCmp cmp] {a k : α} {v : β k} : + (t.insert k v).get? a = + if h : cmp k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a := + Impl.get?_insert t.wf + +@[simp] +theorem get?_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + (t.insert k v).get? k = some v := + Impl.get?_insert_self t.wf + +theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + t.contains a = (t.get? a).isSome := + Impl.contains_eq_isSome_get? t.wf + +theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + a ∈ t ↔ (t.get? a).isSome := + Impl.mem_iff_isSome_get? t.wf + +theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + t.contains a = false → t.get? a = none := + Impl.get?_eq_none_of_contains_eq_false t.wf + +theorem get?_eq_none [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + ¬ a ∈ t → t.get? a = none := + Impl.get?_eq_none t.wf + +theorem get?_erase [TransCmp cmp] [LawfulEqCmp cmp] {k a : α} : + (t.erase k).get? a = if cmp k a = .eq then none else t.get? a := + Impl.get?_erase t.wf + +@[simp] +theorem get?_erase_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} : + (t.erase k).get? k = none := + Impl.get?_erase_self t.wf + +namespace Const + +variable {β : Type v} {t : DTreeMap α β cmp} + +@[simp] +theorem get?_emptyc [TransCmp cmp] {a : α} : + get? (∅ : DTreeMap α β cmp) a = none := + Impl.Const.get?_empty + +theorem get?_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty = true → get? t a = none := + Impl.Const.get?_of_isEmpty t.wf + +theorem get?_insert [TransCmp cmp] {a k : α} {v : β} : + get? (t.insert k v) a = + if cmp k a = .eq then some v else get? t a := + Impl.Const.get?_insert t.wf + +@[simp] +theorem get?_insert_self [TransCmp cmp] {k : α} {v : β} : + get? (t.insert k v) k = some v := + Impl.Const.get?_insert_self t.wf + +theorem contains_eq_isSome_get? [TransCmp cmp] {a : α} : + t.contains a = (get? t a).isSome := + Impl.Const.contains_eq_isSome_get? t.wf + +theorem mem_iff_isSome_get? [TransCmp cmp] {a : α} : + a ∈ t ↔ (get? t a).isSome := + Impl.Const.mem_iff_isSome_get? t.wf + +theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : + t.contains a = false → get? t a = none := + Impl.Const.get?_eq_none_of_contains_eq_false t.wf + +theorem get?_eq_none [TransCmp cmp] {a : α} : + ¬ a ∈ t → get? t a = none := + Impl.Const.get?_eq_none t.wf + +theorem get?_erase [TransCmp cmp] {k a : α} : + get? (t.erase k) a = if cmp k a = .eq then none else get? t a := + Impl.Const.get?_erase t.wf + +@[simp] +theorem get?_erase_self [TransCmp cmp] {k : α} : + get? (t.erase k) k = none := + Impl.Const.get?_erase_self t.wf + +theorem get?_eq_get? [LawfulEqCmp cmp] [TransCmp cmp] {a : α} : get? t a = t.get? a := + Impl.Const.get?_eq_get? t.wf + +theorem get?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) : + get? t a = get? t b := + Impl.Const.get?_congr t.wf hab + +end Const + end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/RawLemmas.lean b/src/Std/Data/DTreeMap/RawLemmas.lean index 4033e7f9a1..f956787e76 100644 --- a/src/Std/Data/DTreeMap/RawLemmas.lean +++ b/src/Std/Data/DTreeMap/RawLemmas.lean @@ -24,6 +24,7 @@ universe u v namespace Std.DTreeMap.Raw variable {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : DTreeMap.Raw α β cmp} +private local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ private theorem ext {t t' : Raw α β cmp} : t.inner = t'.inner → t = t' := by cases t; cases t'; rintro rfl; rfl @@ -237,4 +238,105 @@ theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β k} : (t.insertIfNew k v).size ≤ t.size + 1 := Impl.size_insertIfNew!_le h +@[simp] +theorem get?_emptyc [TransCmp cmp] [LawfulEqCmp cmp] {a : α} : + (∅ : DTreeMap α β cmp).get? a = none := + Impl.get?_empty + +theorem get?_of_isEmpty [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : + t.isEmpty = true → t.get? a = none := + Impl.get?_of_isEmpty h + +theorem get?_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a k : α} {v : β k} : + (t.insert k v).get? a = + if h : cmp k a = .eq then some (cast (congrArg β (compare_eq_iff_eq.mp h)) v) else t.get? a := + Impl.get?_insert! h + +@[simp] +theorem get?_insert_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insert k v).get? k = some v := + Impl.get?_insert!_self h + +theorem contains_eq_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : + t.contains a = (t.get? a).isSome := + Impl.contains_eq_isSome_get? h + +theorem mem_iff_isSome_get? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : + a ∈ t ↔ (t.get? a).isSome := + Impl.mem_iff_isSome_get? h + +theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : + t.contains a = false → t.get? a = none := + Impl.get?_eq_none_of_contains_eq_false h + +theorem get?_eq_none [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {a : α} : + ¬ a ∈ t → t.get? a = none := + Impl.get?_eq_none h + +theorem get?_erase [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} : + (t.erase k).get? a = if cmp k a = .eq then none else t.get? a := + Impl.get?_erase! h + +@[simp] +theorem get?_erase_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} : + (t.erase k).get? k = none := + Impl.get?_erase!_self h + +namespace Const + +variable {β : Type v} {t : Raw α β cmp} + +@[simp] +theorem get?_emptyc [TransCmp cmp] {a : α} : + get? (∅ : Raw α β cmp) a = none := + Impl.Const.get?_empty + +theorem get?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty = true → get? t a = none := + Impl.Const.get?_of_isEmpty h + +theorem get?_insert [TransCmp cmp] (h : t.WF) {a k : α} {v : β} : + get? (t.insert k v) a = + if cmp k a = .eq then some v else get? t a := + Impl.Const.get?_insert! h + +@[simp] +theorem get?_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + get? (t.insert k v) k = some v := + Impl.Const.get?_insert!_self h + +theorem contains_eq_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} : + t.contains a = (get? t a).isSome := + Impl.Const.contains_eq_isSome_get? h + +theorem mem_iff_isSome_get? [TransCmp cmp] (h : t.WF) {a : α} : + a ∈ t ↔ (get? t a).isSome := + Impl.Const.mem_iff_isSome_get? h + +theorem get?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : + t.contains a = false → get? t a = none := + Impl.Const.get?_eq_none_of_contains_eq_false h + +theorem get?_eq_none [TransCmp cmp] (h : t.WF) {a : α} : + ¬ a ∈ t → get? t a = none := + Impl.Const.get?_eq_none h + +theorem get?_erase [TransCmp cmp] (h : t.WF) {k a : α} : + get? (t.erase k) a = if cmp k a = .eq then none else get? t a := + Impl.Const.get?_erase! h + +@[simp] +theorem get?_erase_self [TransCmp cmp] (h : t.WF) {k : α} : + get? (t.erase k) k = none := + Impl.Const.get?_erase!_self h + +theorem get?_eq_get? [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {a : α} : get? t a = t.get? a := + Impl.Const.get?_eq_get? h + +theorem get?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) : + get? t a = get? t b := + Impl.Const.get?_congr h hab + +end Const + end Std.DTreeMap.Raw diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 172ea7b730..894c28e044 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -58,10 +58,6 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : @[simp] theorem contains_empty {a : α} {c} : (empty c : HashMap α β).contains a = false := DHashMap.contains_empty -@[simp] theorem get_eq_getElem {a : α} {h} : get m a h = m[a]'h := rfl -@[simp] theorem get?_eq_getElem? {a : α} : get? m a = m[a]? := rfl -@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl - @[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : HashMap α β) := DHashMap.not_mem_empty @@ -207,6 +203,10 @@ theorem containsThenInsertIfNew_snd {k : α} {v : β} : (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v := ext DHashMap.containsThenInsertIfNew_snd +@[simp] theorem get_eq_getElem {a : α} {h} : get m a h = m[a]'h := rfl +@[simp] theorem get?_eq_getElem? {a : α} : get? m a = m[a]? := rfl +@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl + @[simp] theorem getElem?_empty {a : α} {c} : (empty c : HashMap α β)[a]? = none := DHashMap.Const.get?_empty diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 4084f331da..6f3b07c9ed 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -71,10 +71,6 @@ theorem mem_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : @[simp] theorem contains_empty {a : α} {c} : (empty c : Raw α β).contains a = false := DHashMap.Raw.contains_empty -@[simp] theorem get_eq_getElem {a : α} {h} : get m a h = m[a]'h := rfl -@[simp] theorem get?_eq_getElem? {a : α} : get? m a = m[a]? := rfl -@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl - @[simp] theorem not_mem_empty {a : α} {c} : ¬a ∈ (empty c : Raw α β) := DHashMap.Raw.not_mem_empty @@ -217,6 +213,10 @@ theorem containsThenInsertIfNew_snd (h : m.WF) {k : α} {v : β} : (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v := ext (DHashMap.Raw.containsThenInsertIfNew_snd h.out) +@[simp] theorem get_eq_getElem {a : α} {h} : get m a h = m[a]'h := rfl +@[simp] theorem get?_eq_getElem? {a : α} : get? m a = m[a]? := rfl +@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! m a = m[a]! := rfl + @[simp] theorem getElem?_empty {a : α} {c} : (empty c : Raw α β)[a]? = none := DHashMap.Raw.Const.get?_empty diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 2d3b7d4165..ef988b8b14 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -237,4 +237,55 @@ theorem size_insertIfNew_le [TransCmp cmp] {k : α} {v : β} : (t.insertIfNew k v).size ≤ t.size + 1 := DTreeMap.size_insertIfNew_le +@[simp] theorem get_eq_getElem {a : α} {h} : get t a h = t[a]'h := rfl +@[simp] theorem get?_eq_getElem? {a : α} : get? t a = t[a]? := rfl +@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! t a = t[a]! := rfl + +@[simp] +theorem getElem?_emptyc [TransCmp cmp] {a : α} : + (∅ : TreeMap α β cmp)[a]? = none := + DTreeMap.Const.get?_emptyc (cmp := cmp) (a := a) + +theorem getElem?_of_isEmpty [TransCmp cmp] {a : α} : + t.isEmpty = true → t[a]? = none := + DTreeMap.Const.get?_of_isEmpty + +theorem getElem?_insert [TransCmp cmp] {a k : α} {v : β} : + (t.insert k v)[a]? = if cmp k a = .eq then some v else t[a]? := + DTreeMap.Const.get?_insert + +@[simp] +theorem getElem?_insert_self [TransCmp cmp] {k : α} {v : β} : + (t.insert k v)[k]? = some v := + DTreeMap.Const.get?_insert_self + +theorem contains_eq_isSome_getElem? [TransCmp cmp] {a : α} : + t.contains a = t[a]?.isSome := + DTreeMap.Const.contains_eq_isSome_get? + +theorem mem_iff_isSome_getElem? [TransCmp cmp] {a : α} : + a ∈ t ↔ t[a]?.isSome := + DTreeMap.Const.mem_iff_isSome_get? + +theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] {a : α} : + t.contains a = false → t[a]? = none := + DTreeMap.Const.get?_eq_none_of_contains_eq_false + +theorem getElem?_eq_none [TransCmp cmp] {a : α} : + ¬ a ∈ t → t[a]? = none := + DTreeMap.Const.get?_eq_none + +theorem getElem?_erase [TransCmp cmp] {k a : α} : + (t.erase k)[a]? = if cmp k a = .eq then none else t[a]? := + DTreeMap.Const.get?_erase + +@[simp] +theorem getElem?_erase_self [TransCmp cmp] {k : α} : + (t.erase k)[k]? = none := + DTreeMap.Const.get?_erase_self + +theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) : + t[a]? = t[b]? := + DTreeMap.Const.get?_congr hab + end Std.TreeMap diff --git a/src/Std/Data/TreeMap/RawLemmas.lean b/src/Std/Data/TreeMap/RawLemmas.lean index 40cf4f7534..79e55021bb 100644 --- a/src/Std/Data/TreeMap/RawLemmas.lean +++ b/src/Std/Data/TreeMap/RawLemmas.lean @@ -235,4 +235,55 @@ theorem size_insertIfNew_le [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insertIfNew k v).size ≤ t.size + 1 := DTreeMap.Raw.size_insertIfNew_le h +@[simp] theorem get_eq_getElem {a : α} {h} : get t a h = t[a]'h := rfl +@[simp] theorem get?_eq_getElem? {a : α} : get? t a = t[a]? := rfl +@[simp] theorem get!_eq_getElem! [Inhabited β] {a : α} : get! t a = t[a]! := rfl + +@[simp] +theorem getElem?_emptyc [TransCmp cmp] {a : α} : + (∅ : Raw α β cmp)[a]? = none := + DTreeMap.Raw.Const.get?_emptyc (cmp := cmp) (a := a) + +theorem getElem?_of_isEmpty [TransCmp cmp] (h : t.WF) {a : α} : + t.isEmpty = true → t[a]? = none := + DTreeMap.Raw.Const.get?_of_isEmpty h + +theorem getElem?_insert [TransCmp cmp] (h : t.WF) {a k : α} {v : β} : + (t.insert k v)[a]? = if cmp k a = .eq then some v else t[a]? := + DTreeMap.Raw.Const.get?_insert h + +@[simp] +theorem getElem?_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insert k v)[k]? = some v := + DTreeMap.Raw.Const.get?_insert_self h + +theorem contains_eq_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} : + t.contains a = t[a]?.isSome := + DTreeMap.Raw.Const.contains_eq_isSome_get? h + +theorem mem_iff_isSome_getElem? [TransCmp cmp] (h : t.WF) {a : α} : + a ∈ t ↔ t[a]?.isSome := + DTreeMap.Raw.Const.mem_iff_isSome_get? h + +theorem getElem?_eq_none_of_contains_eq_false [TransCmp cmp] (h : t.WF) {a : α} : + t.contains a = false → t[a]? = none := + DTreeMap.Raw.Const.get?_eq_none_of_contains_eq_false h + +theorem getElem?_eq_none [TransCmp cmp] (h : t.WF) {a : α} : + ¬ a ∈ t → t[a]? = none := + DTreeMap.Raw.Const.get?_eq_none h + +theorem getElem?_erase [TransCmp cmp] (h : t.WF) {k a : α} : + (t.erase k)[a]? = if cmp k a = .eq then none else t[a]? := + DTreeMap.Raw.Const.get?_erase h + +@[simp] +theorem getElem?_erase_self [TransCmp cmp] (h : t.WF) {k : α} : + (t.erase k)[k]? = none := + DTreeMap.Raw.Const.get?_erase_self h + +theorem getElem?_congr [TransCmp cmp] (h : t.WF) {a b : α} (hab : cmp a b = .eq) : + t[a]? = t[b]? := + DTreeMap.Raw.Const.get?_congr h hab + end Std.TreeMap.Raw