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>
This commit is contained in:
Paul Reichert
GitHub
parent
36723d38b9
commit
af741abbf5
7 changed files with 466 additions and 15 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue