feat: more tree map lemmas for minKey? (#7556)
This PR provides lemmas about the tree map function `minKey?` and its interaction with other functions for which lemmas already exist. --------- Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert
GitHub
parent
cbfb9e482f
commit
d2c35fd39d
8 changed files with 742 additions and 42 deletions
|
|
@ -4227,6 +4227,14 @@ theorem minKey?_eq_none_iff [TransOrd α] (h : t.WF) :
|
|||
t.minKey? = none ↔ t.isEmpty := by
|
||||
simp_to_model using List.minKey?_eq_none_iff_isEmpty
|
||||
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE := by
|
||||
simp_to_model using List.minKey?_eq_some_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (compare km k).isLE := by
|
||||
simp_to_model using List.minKey?_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem isNone_minKey?_eq_isEmpty [TransOrd α] (h : t.WF) :
|
||||
t.minKey?.isNone = t.isEmpty := by
|
||||
simp_to_model using List.isNone_minKey?_eq_isEmpty
|
||||
|
|
@ -4303,6 +4311,15 @@ theorem minKey?_le_of_mem [TransOrd α] (h : t.WF) {k km} :
|
|||
compare km k |>.isLE :=
|
||||
minKey?_le_of_contains h
|
||||
|
||||
theorem le_minKey? [TransOrd α] {k} (h : t.WF) :
|
||||
(∀ k', t.minKey? = some k' → (compare k k').isLE) ↔
|
||||
(∀ k', k' ∈ t → (compare k k').isLE) := by
|
||||
simp_to_model using List.le_minKey?
|
||||
|
||||
theorem getKey?_minKey? [TransOrd α] (h : t.WF) {km} :
|
||||
(hkm : t.minKey? = some km) → t.getKey? km = some km := by
|
||||
simp_to_model using List.getKey?_minKey?
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_bind_getKey? [TransOrd α] (h : t.WF) :
|
||||
t.minKey?.bind t.getKey? = t.minKey? := by
|
||||
|
|
@ -4353,6 +4370,99 @@ theorem minKey?_le_minKey?_erase! [TransOrd α] (h : t.WF) {k km kme} :
|
|||
compare km kme |>.isLE := by
|
||||
simpa only [erase_eq_erase!] using minKey?_le_minKey?_erase h
|
||||
|
||||
theorem minKey?_insertIfNew [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v h.balanced).impl.minKey? =
|
||||
t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew
|
||||
|
||||
theorem minKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew! k v).minKey? =
|
||||
t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew h
|
||||
|
||||
theorem isSome_minKey?_insertIfNew [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v h.balanced).impl.minKey?.isSome := by
|
||||
simp_to_model [insertIfNew] using List.isSome_minKey?_insertEntryIfNew
|
||||
|
||||
theorem isSome_minKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew! k v).minKey?.isSome := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using isSome_minKey?_insertIfNew h
|
||||
|
||||
theorem minKey?_insertIfNew_le_minKey? [TransOrd α] (h : t.WF) {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew k v h.balanced |>.impl.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
compare kmi km |>.isLE := by
|
||||
simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew_le_minKey?
|
||||
|
||||
theorem minKey?_insertIfNew!_le_minKey? [TransOrd α] (h : t.WF) {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew! k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew! h) = kmi) →
|
||||
compare kmi km |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_minKey? h
|
||||
|
||||
theorem minKey?_insertIfNew_le_self [TransOrd α] (h : t.WF) {k v kmi} :
|
||||
(hkmi : (t.insertIfNew k v h.balanced |>.impl.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
compare kmi k |>.isLE := by
|
||||
simp_to_model [insertIfNew] using List.minKey?_insertEntryIfNew_le_self
|
||||
|
||||
theorem minKey?_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v kmi} :
|
||||
(hkmi : (t.insertIfNew! k v |>.minKey?.get <| isSome_minKey?_insertIfNew! h) = kmi) →
|
||||
compare kmi k |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_self h
|
||||
|
||||
theorem minKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) :
|
||||
(t.modify k f).minKey? = t.minKey? := by
|
||||
simp_to_model [modify] using List.minKey?_modifyKey
|
||||
|
||||
theorem minKey?_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
|
||||
(t.alter k f h.balanced).impl.minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [alter] using List.minKey?_alterKey_eq_self
|
||||
|
||||
theorem minKey?_alter!_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
|
||||
(t.alter! k f).minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simpa only [alter_eq_alter!] using minKey?_alter_eq_self h
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Impl α β}
|
||||
|
||||
theorem minKey?_modify [TransOrd α] (h : t.WF) {k f} :
|
||||
(Const.modify k f t).minKey? = t.minKey?.map fun km => if compare km k = .eq then k else km := by
|
||||
simp_to_model [Const.modify] using List.Const.minKey?_modifyKey
|
||||
|
||||
theorem minKey?_modify_eq_minKey? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} :
|
||||
(Const.modify k f t).minKey? = t.minKey? := by
|
||||
simp_to_model [Const.modify] using List.Const.minKey?_modifyKey_of_lawfulEqOrd
|
||||
|
||||
theorem isSome_minKey?_modify [TransOrd α] {k f} (h : t.WF) :
|
||||
(Const.modify k f t).minKey?.isSome = !t.isEmpty := by
|
||||
simp_to_model [Const.modify] using List.Const.isSome_minKey?_modifyKey
|
||||
|
||||
theorem isSome_minKey?_modify_eq_isSome [TransOrd α] (h : t.WF) {k f} :
|
||||
(Const.modify k f t).minKey?.isSome = t.minKey?.isSome := by
|
||||
simp_to_model [Const.modify] using List.Const.isSome_minKey?_modifyKey_eq_isSome
|
||||
|
||||
theorem compare_minKey?_modify_eq [TransOrd α] (h : t.WF) {k f km kmm} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmm : (Const.modify k f t |>.minKey? |>.get <|
|
||||
(isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
|
||||
compare kmm km = .eq := by
|
||||
simp_to_model [Const.modify] using List.Const.minKey?_modifyKey_beq
|
||||
|
||||
theorem minKey?_alter_eq_self [TransOrd α] (h : t.WF) {k f} :
|
||||
(Const.alter k f t h.balanced).impl.minKey? = some k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [Const.alter] using List.Const.minKey?_alterKey_eq_self
|
||||
|
||||
theorem minKey?_alter!_eq_self [TransOrd α] (h : t.WF) {k f} :
|
||||
(Const.alter! k f t).minKey? = some k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simpa [alter_eq_alter!] using minKey?_alter_eq_self h
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -2779,6 +2779,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] :
|
|||
t.minKey? = none ↔ t.isEmpty :=
|
||||
Impl.minKey?_eq_none_iff t.wf
|
||||
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} :
|
||||
t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
Impl.minKey?_eq_some_iff_getKey?_eq_self_and_forall t.wf
|
||||
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
|
||||
t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
Impl.minKey?_eq_some_iff_mem_and_forall t.wf
|
||||
|
||||
@[simp]
|
||||
theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] :
|
||||
t.minKey?.isNone = t.isEmpty :=
|
||||
|
|
@ -2837,6 +2845,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] {k km} :
|
|||
cmp km k |>.isLE :=
|
||||
Impl.minKey?_le_of_mem t.wf
|
||||
|
||||
theorem le_minKey? [TransCmp cmp] {k} :
|
||||
(∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
|
||||
(∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKey? t.wf
|
||||
|
||||
theorem getKey?_minKey? [TransCmp cmp] {km} :
|
||||
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
|
||||
Impl.getKey?_minKey? t.wf
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_bind_getKey? [TransCmp cmp] :
|
||||
t.minKey?.bind t.getKey? = t.minKey? :=
|
||||
|
|
@ -2864,6 +2881,71 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
Impl.minKey?_le_minKey?_erase t.wf
|
||||
|
||||
theorem minKey?_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).minKey? =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
Impl.minKey?_insertIfNew t.wf
|
||||
|
||||
theorem isSome_minKey?_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).minKey?.isSome :=
|
||||
Impl.isSome_minKey?_insertIfNew t.wf
|
||||
|
||||
theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew k v |>.minKey? |>.get isSome_minKey?_insertIfNew) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
Impl.minKey?_insertIfNew_le_minKey? t.wf
|
||||
|
||||
theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
|
||||
(hkmi : (t.insertIfNew k v |>.minKey?.get isSome_minKey?_insertIfNew) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
Impl.minKey?_insertIfNew_le_self t.wf
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
|
||||
(t.modify k f).minKey? = t.minKey? :=
|
||||
Impl.minKey?_modify t.wf
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
|
||||
(t.alter k f).minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKey?_alter_eq_self t.wf
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : DTreeMap α β cmp}
|
||||
|
||||
theorem minKey?_modify [TransCmp cmp] {k f} :
|
||||
(Const.modify t k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
|
||||
Impl.Const.minKey?_modify t.wf
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
|
||||
(Const.modify t k f).minKey? = t.minKey? :=
|
||||
Impl.Const.minKey?_modify_eq_minKey? t.wf
|
||||
|
||||
theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
|
||||
(Const.modify t k f).minKey?.isSome = !t.isEmpty :=
|
||||
Impl.Const.isSome_minKey?_modify t.wf
|
||||
|
||||
theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] {k f} :
|
||||
(Const.modify t k f).minKey?.isSome = t.minKey?.isSome :=
|
||||
Impl.Const.isSome_minKey?_modify_eq_isSome t.wf
|
||||
|
||||
theorem compare_minKey?_modify_eq [TransCmp cmp] {k f km kmm} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmm : (Const.modify t k f |>.minKey? |>.get <|
|
||||
isSome_minKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) →
|
||||
cmp kmm km = .eq :=
|
||||
Impl.Const.compare_minKey?_modify_eq t.wf
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] {k f} :
|
||||
(Const.alter t k f).minKey? = some k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKey?_alter_eq_self t.wf
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -2784,6 +2784,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] (h : t.WF) :
|
|||
t.minKey? = none ↔ t.isEmpty :=
|
||||
Impl.minKey?_eq_none_iff h
|
||||
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
Impl.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
|
||||
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
Impl.minKey?_eq_some_iff_mem_and_forall h
|
||||
|
||||
@[simp]
|
||||
theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
|
||||
t.minKey?.isNone = t.isEmpty :=
|
||||
|
|
@ -2842,6 +2850,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
|
|||
cmp km k |>.isLE :=
|
||||
Impl.minKey?_le_of_mem h
|
||||
|
||||
theorem le_minKey? [TransCmp cmp] {k} (h : t.WF) :
|
||||
(∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
|
||||
(∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKey? h
|
||||
|
||||
theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
|
||||
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
|
||||
Impl.getKey?_minKey? h
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
|
||||
t.minKey?.bind t.getKey? = t.minKey? :=
|
||||
|
|
@ -2869,6 +2886,71 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
Impl.minKey?_le_minKey?_erase! h
|
||||
|
||||
theorem minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).minKey? =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
Impl.minKey?_insertIfNew! h
|
||||
|
||||
theorem isSome_minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).minKey?.isSome :=
|
||||
Impl.isSome_minKey?_insertIfNew! h
|
||||
|
||||
theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] (h : t.WF) {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
Impl.minKey?_insertIfNew!_le_minKey? h
|
||||
|
||||
theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
|
||||
(hkmi : (t.insertIfNew k v |>.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
Impl.minKey?_insertIfNew!_le_self h
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
|
||||
(t.modify k f).minKey? = t.minKey? :=
|
||||
Impl.minKey?_modify h
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
|
||||
(t.alter k f).minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKey?_alter!_eq_self h
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Raw α β cmp}
|
||||
|
||||
theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(Const.modify t k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
|
||||
Impl.Const.minKey?_modify h
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
|
||||
(Const.modify t k f).minKey? = t.minKey? :=
|
||||
Impl.Const.minKey?_modify_eq_minKey? h
|
||||
|
||||
theorem isSome_minKey?_modify [TransCmp cmp] {k f} (h : t.WF) :
|
||||
(Const.modify t k f).minKey?.isSome = !t.isEmpty :=
|
||||
Impl.Const.isSome_minKey?_modify h
|
||||
|
||||
theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(Const.modify t k f).minKey?.isSome = t.minKey?.isSome :=
|
||||
Impl.Const.isSome_minKey?_modify_eq_isSome h
|
||||
|
||||
theorem compare_minKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmm : (Const.modify t k f |>.minKey? |>.get <|
|
||||
(isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
|
||||
cmp kmm km = .eq :=
|
||||
Impl.Const.compare_minKey?_modify_eq h
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(Const.alter t k f).minKey? = some k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKey?_alter!_eq_self h
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -696,6 +696,10 @@ theorem getKey_congr [BEq α] [EquivBEq α] {l : List ((a : α) × β a)}
|
|||
{k k' : α} (h : k == k') {h'} {h''} : getKey k l h' = getKey k' l h'' := by
|
||||
simpa only [getKey?_eq_some_getKey, h', h'', Option.some.injEq] using getKey?_congr (l := l) h
|
||||
|
||||
theorem getKey_eq_getEntry_fst [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {a : α}
|
||||
{h : containsKey a l} : getKey a l h = (getEntry a l h).fst := by
|
||||
simp [getKey, getKey?_eq_getEntry?, Option.get_map, getEntry]
|
||||
|
||||
/-- Internal implementation detail of the hash map -/
|
||||
def getKeyD [BEq α] (a : α) (l : List ((a : α) × β a)) (fallback : α) : α :=
|
||||
(getKey? a l).getD fallback
|
||||
|
|
@ -3839,6 +3843,10 @@ theorem modifyKey_eq_alterKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β
|
|||
split <;> next h =>
|
||||
simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false]
|
||||
|
||||
theorem DistinctKeys.modifyKey [BEq α] [LawfulBEq α] {a f} {l : List ((a : α) × β a)}
|
||||
(hd : DistinctKeys l) : DistinctKeys (modifyKey a f l) := by
|
||||
simpa [modifyKey_eq_alterKey] using hd.alterKey
|
||||
|
||||
theorem modifyKey_of_perm [BEq α] [LawfulBEq α] {l l' : List ((a : α) × β a)}
|
||||
{k : α} {f : β k → β k} (hl : DistinctKeys l) (h : Perm l l') :
|
||||
Perm (modifyKey k f l) (modifyKey k f l') := by
|
||||
|
|
@ -4150,6 +4158,10 @@ theorem constModifyKey_eq_modifyKey {β : Type v} [BEq α] [LawfulBEq α] {k :
|
|||
rw [modifyKey, Const.modifyKey, getValue?_eq_getValueCast?]
|
||||
cases getValueCast? k l <;> rfl
|
||||
|
||||
theorem DistinctKeys.constModifyKey {β : Type v} [BEq α] [EquivBEq α] {a f} {l : List ((_ : α) × β)}
|
||||
(hd : DistinctKeys l) : DistinctKeys (Const.modifyKey a f l) := by
|
||||
simpa [Const.modifyKey_eq_alterKey] using hd.constAlterKey
|
||||
|
||||
end Modify
|
||||
|
||||
section Min
|
||||
|
|
@ -4265,8 +4277,8 @@ theorem minEntry?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
|||
· intro e e' he he' hee' he'e
|
||||
exact hd.eq_of_mem_of_beq he he' <| compare_eq_iff_beq.mp <| TransCmp.isLE_antisymm hee' he'e
|
||||
|
||||
theorem minKey?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? l = some k ↔ getKey? k l = some k ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
|
||||
simp only [getKey?_eq_getEntry?, Option.map_eq_some', getEntry?_eq_some_iff hd]
|
||||
|
|
@ -4276,8 +4288,22 @@ theorem minKey?_eq_some_iff [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k
|
|||
· rintro ⟨⟨_, ⟨_, hm⟩, rfl⟩, hcmp⟩
|
||||
exact ⟨_, ⟨hm, hcmp⟩, rfl⟩
|
||||
|
||||
theorem minEntry?_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)}
|
||||
(hl : DistinctKeys l) (hp : l.Perm l') :
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α]
|
||||
[LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? l = some k ↔ containsKey k l ∧ ∀ k' : α, containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?, Option.map_eq_some', minEntry?_eq_some_iff _ hd]
|
||||
apply Iff.intro
|
||||
· rintro ⟨_, ⟨hm, hcmp⟩, rfl⟩
|
||||
exact ⟨containsKey_of_mem hm, hcmp⟩
|
||||
· rintro ⟨hc, hle⟩
|
||||
have heq := beq_iff_eq.mp <| getKey_eq_getEntry_fst (α := α) ▸ getKey_beq hc
|
||||
refine ⟨getEntry k l hc, ⟨mem_getEntry hc, ?_⟩, heq⟩
|
||||
intro k' hk'
|
||||
rw [heq]
|
||||
exact hle _ hk'
|
||||
|
||||
theorem minEntry?_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : l.Perm l') :
|
||||
minEntry? l = minEntry? l' := by
|
||||
cases l
|
||||
case nil => simp_all only [List.nil_perm]
|
||||
|
|
@ -4430,19 +4456,24 @@ theorem isSome_minKey?_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEq
|
|||
minKey? l |>.isSome := by
|
||||
simpa [minKey?] using isSome_minEntry?_of_containsKey hc
|
||||
|
||||
theorem getEntry?_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {em} (hem : minEntry? l = some em) :
|
||||
getEntry? em.1 l = some em := by
|
||||
simp only [minEntry?_eq_some_iff _ hd] at hem
|
||||
exact getEntry?_of_mem hd BEq.refl hem.1
|
||||
|
||||
theorem minKey?_bind_getEntry? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
(minKey? l |>.bind fun k => getEntry? k l) = minEntry? l := by
|
||||
rw [minKey?]
|
||||
cases h : minEntry? l
|
||||
· rfl
|
||||
· simp only [Option.map_some', Option.some_bind, minEntry?_eq_some_iff _ hd] at h
|
||||
exact getEntry?_of_mem hd BEq.refl h.1
|
||||
· simp [getEntry?_minKey? hd h]
|
||||
|
||||
theorem getKey?_minKey? [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} (hkm : minKey? l = some km) :
|
||||
getKey? km l = some km := by
|
||||
simp_all [minKey?_eq_some_iff hd]
|
||||
simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd]
|
||||
|
||||
theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
|
|
@ -4463,12 +4494,12 @@ theorem minKey?_eraseKey_eq_iff_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq
|
|||
minKey? (eraseKey k l) = minKey? l ↔ ∀ {km}, minKey? l = some km → (k == km) = false := by
|
||||
cases h : minKey? l
|
||||
· simp_all [minKey?_eq_none_iff_isEmpty]
|
||||
· simp only [minKey?_eq_some_iff, getKey?_eraseKey, containsKey_eraseKey, compare_eq_iff_beq,
|
||||
hd, hd.eraseKey] at ⊢ h
|
||||
· simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall, getKey?_eraseKey,
|
||||
containsKey_eraseKey, compare_eq_iff_beq, hd, hd.eraseKey] at ⊢ h
|
||||
simp_all
|
||||
|
||||
theorem minKey?_eraseKey_eq_of_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
theorem minKey?_eraseKey_eq_of_beq_minKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{k} {l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(hc : ∀ {km}, minKey? l = some km → (k == km) = false) :
|
||||
minKey? (eraseKey k l) = minKey? l := by
|
||||
rw [minKey?_eraseKey_eq_iff_beq_minKey?_eq_false hd |>.mpr]
|
||||
|
|
@ -4496,7 +4527,20 @@ theorem minKey?_le_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
|
|||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l)
|
||||
(hkm : (minKey? l |>.get <| isSome_minKey?_of_containsKey hc) = km) :
|
||||
compare km k |>.isLE := by
|
||||
simpa only [← hkm] using minKey?_eq_some_iff hd |>.mp (by simp) |>.2 _ hc
|
||||
simpa only [← hkm] using
|
||||
minKey?_eq_some_iff_getKey?_eq_self_and_forall hd |>.mp (by simp) |>.2 _ hc
|
||||
|
||||
theorem le_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)}
|
||||
(hd : DistinctKeys l) :
|
||||
(∀ k', minKey? l = some k' → (compare k k').isLE) ↔
|
||||
(∀ k', containsKey k' l → (compare k k').isLE) := by
|
||||
apply Iff.intro
|
||||
· intro h k' hk'
|
||||
have := isSome_minKey?_of_containsKey hk'
|
||||
specialize h (minKey? l |>.get <| isSome_minKey?_of_containsKey hk') (by simp)
|
||||
exact TransCmp.isLE_trans h <| minKey?_le_of_containsKey hd hk' rfl
|
||||
· intro h k' hk'
|
||||
exact h k' (containsKey_minKey? hd hk')
|
||||
|
||||
theorem isSome_minKey?_of_isSome_minKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k}
|
||||
{l : List ((a : α) × β a)} (hs : eraseKey k l |> minKey? |>.isSome) :
|
||||
|
|
@ -4519,6 +4563,184 @@ theorem minKey?_le_minKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOr
|
|||
apply minKey?_le_of_containsKey hd _ hkm
|
||||
apply containsKey_minKey?_eraseKey hd hkme
|
||||
|
||||
theorem minKey?_cons [Ord α] [TransOrd α] (e : (a : α) × β a) (l : List ((a : α) × β a)) :
|
||||
minKey? (e :: l) = some (match minKey? l with
|
||||
| none => e.1
|
||||
| some w => if compare e.1 w |>.isLE then e.1 else w) := by
|
||||
simp [minKey?, minEntry?_cons]
|
||||
cases minEntry? l
|
||||
· rfl
|
||||
· simp [min_def, apply_ite Sigma.fst]
|
||||
|
||||
theorem minEntry?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minEntry? (insertEntryIfNew k v l) =
|
||||
some (match minEntry? l with
|
||||
| none => ⟨k, v⟩
|
||||
| some e => if compare k e.1 = .lt then ⟨k, v⟩ else e) := by
|
||||
simp [insertEntryIfNew]
|
||||
cases hc : containsKey k l
|
||||
· simp only [cond_false, minEntry?_cons, Option.some.injEq]
|
||||
cases he : minEntry? l
|
||||
· simp
|
||||
· rename_i e
|
||||
simp [min_def]
|
||||
cases hcmp : compare k e.fst
|
||||
· simp
|
||||
· simp
|
||||
rw [containsKey_congr <| compare_eq_iff_beq.mp hcmp] at hc
|
||||
rw [containsKey_minKey? hd] at hc
|
||||
· contradiction
|
||||
· simp_all [minKey?]
|
||||
· simp
|
||||
· simp only [cond_true]
|
||||
have := isSome_minEntry?_of_containsKey hc
|
||||
cases h : minEntry? l
|
||||
· simp_all
|
||||
· simp
|
||||
split
|
||||
· have := minKey?_le_of_containsKey hd hc (by simp [minKey?, h]; rfl)
|
||||
simp_all [← OrientedCmp.gt_iff_lt]
|
||||
· rfl
|
||||
|
||||
theorem minKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? (insertEntryIfNew k v l) =
|
||||
some ((minKey? l).elim k fun k' => if compare k k' = .lt then k else k') := by
|
||||
simp [minKey?, minEntry?_insertEntryIfNew hd]
|
||||
cases minEntry? l <;> simp [apply_ite Sigma.fst]
|
||||
|
||||
theorem isSome_minEntry?_insertIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k}
|
||||
{l : List ((a : α) × β a)} (hl : DistinctKeys l) :
|
||||
minEntry? (insertEntryIfNew k v l) |>.isSome := by
|
||||
simp [minEntry?_insertEntryIfNew hl]
|
||||
|
||||
theorem isSome_minKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
|
||||
{v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) :
|
||||
minKey? (insertEntryIfNew k v l) |>.isSome := by
|
||||
simp [minKey?_insertEntryIfNew hl]
|
||||
|
||||
theorem minKey?_insertEntryIfNew_le_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α}
|
||||
{v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l) {km kmi} (hkm : minKey? l = some km)
|
||||
(hkmi : (insertEntryIfNew k v l |> minKey? |>.get <| isSome_minKey?_insertEntryIfNew hl) = kmi) :
|
||||
compare kmi km |>.isLE := by
|
||||
simp only [← hkmi, minKey?_insertEntryIfNew hl, hkm, Option.get_some, Option.elim_some]
|
||||
split <;> simp [*]
|
||||
|
||||
theorem minKey?_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α}
|
||||
{v : β k} {l : List ((a : α) × β a)} (hl : DistinctKeys l)
|
||||
(hkmi : (insertEntryIfNew k v l |> minKey? |>.get <| isSome_minKey?_insertEntryIfNew hl) = kmi) :
|
||||
compare kmi k |>.isLE := by
|
||||
simp only [← hkmi, minKey?_insertEntryIfNew hl, Option.get_some]
|
||||
cases minKey? l
|
||||
· simp
|
||||
· simp only [Option.elim_some]
|
||||
cases hcmp : compare k _ <;> (try simp; done)
|
||||
all_goals
|
||||
rw [OrientedCmp.eq_swap (cmp := compare)]
|
||||
simp_all
|
||||
|
||||
theorem minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? (modifyKey k f l) = minKey? l := by
|
||||
cases hkm : minKey? l
|
||||
· simp_all [minKey?_eq_none_iff_isEmpty, modifyKey]
|
||||
· simp_all [minKey?_eq_some_iff_mem_and_forall, hd.modifyKey, containsKey_modifyKey]
|
||||
|
||||
theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{k f} {l : List ((a : α) × β a)} (hd : DistinctKeys l) :
|
||||
minKey? (alterKey k f l) = some k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.alterKey, getKey?_alterKey _ hd,
|
||||
beq_self_eq_true, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true, Option.not_isSome,
|
||||
Option.isNone_iff_eq_none, reduceCtorEq, imp_false, ← Option.isSome_iff_ne_none,
|
||||
containsKey_alterKey hd, beq_iff_eq, Bool.ite_eq_true_distrib, and_congr_right_iff]
|
||||
intro hf
|
||||
apply Iff.intro
|
||||
· intro hk k' hk'
|
||||
simpa [hk', hf] using hk k'
|
||||
· intro hk k' hk'
|
||||
simp only [hf, if_true_left] at hk'
|
||||
by_cases hbeq : k == k'
|
||||
· simp [compare_eq_iff_beq.mpr hbeq]
|
||||
· exact hk k' (hk' hbeq)
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
theorem minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) :
|
||||
minKey? (modifyKey k f l) = (minKey? l).map fun km => if km == k then k else km := by
|
||||
cases hkm : minKey? l
|
||||
· simp_all [minKey?_eq_none_iff_isEmpty, modifyKey]
|
||||
· simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall, hd.constModifyKey, getKey?_modifyKey]
|
||||
cases h : _ == k
|
||||
· simp_all [BEq.symm_false h, containsKey_modifyKey]
|
||||
· simp_all [containsKey_congr (BEq.symm h), containsKey_eq_isSome_getKey?,
|
||||
containsKey_modifyKey, getKey?_modifyKey]
|
||||
intro k' hk'
|
||||
cases hcmp : compare k k' <;> try rfl
|
||||
replace hkm := hkm.2 k'
|
||||
simp only [← compare_eq_iff_beq] at *
|
||||
simp only [hcmp, reduceCtorEq, ↓reduceIte] at hk'
|
||||
specialize hkm hk'
|
||||
simp only [OrientedCmp.gt_iff_lt, Ordering.isLE_gt, Bool.false_eq_true] at *
|
||||
have := TransCmp.lt_of_isLE_of_lt hkm hcmp
|
||||
simp [this] at h
|
||||
|
||||
theorem minKey?_modifyKey_of_lawfulEqOrd [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[LawfulEqOrd α] {k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
|
||||
minKey? (modifyKey k f l) = minKey? l := by
|
||||
simp only [minKey?_modifyKey hd]
|
||||
cases minKey? l
|
||||
· rfl
|
||||
· simp only [beq_iff_eq, Option.map_some', Option.some.injEq, ite_eq_right_iff]
|
||||
exact Eq.symm
|
||||
|
||||
theorem isSome_minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
|
||||
{l : List ((_ : α) × β)} :
|
||||
(modifyKey k f l |> minKey?).isSome = !l.isEmpty := by
|
||||
simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
|
||||
theorem isSome_minKey?_modifyKey_eq_isSome [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f}
|
||||
{l : List ((_ : α) × β)} :
|
||||
(modifyKey k f l |> minKey?).isSome = (minKey? l).isSome := by
|
||||
simp [Option.isSome_map', isSome_minKey?_eq_not_isEmpty, isEmpty_modifyKey]
|
||||
|
||||
theorem minKey?_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f km kmm}
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : minKey? l = some km)
|
||||
(hkmm : (modifyKey k f l |> minKey? |>.get <|
|
||||
isSome_minKey?_modifyKey_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) :
|
||||
kmm == km := by
|
||||
simp only [minKey?_modifyKey hd, Option.get_map] at hkmm
|
||||
simp only [Option.eq_some_iff_get_eq] at hkm
|
||||
simp only [← hkmm, ← hkm.2]
|
||||
split
|
||||
· exact BEq.symm ‹_›
|
||||
· exact BEq.refl
|
||||
|
||||
theorem minKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) :
|
||||
minKey? (alterKey k f l) = some k ↔
|
||||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simp only [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd.constAlterKey, getKey?_alterKey _ hd,
|
||||
← compare_eq_iff_beq, compare_self, ↓reduceIte, ite_eq_left_iff, Bool.not_eq_true,
|
||||
Option.not_isSome, Option.isNone_iff_eq_none, reduceCtorEq, imp_false,
|
||||
← Option.isSome_iff_ne_none, containsKey_alterKey hd, Bool.ite_eq_true_distrib,
|
||||
and_congr_right_iff]
|
||||
intro hf
|
||||
apply Iff.intro
|
||||
· intro hk k' hk'
|
||||
simpa [hk', hf] using hk k'
|
||||
· intro hk k' hk'
|
||||
simp only [hf, if_true_left] at hk'
|
||||
by_cases heq : compare k k' = .eq
|
||||
· simp [heq]
|
||||
· exact hk k' (hk' heq)
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.Internal.List
|
||||
|
|
|
|||
|
|
@ -1748,6 +1748,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] :
|
|||
t.minKey? = none ↔ t.isEmpty :=
|
||||
DTreeMap.minKey?_eq_none_iff
|
||||
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} :
|
||||
t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
|
||||
t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.minKey?_eq_some_iff_mem_and_forall
|
||||
|
||||
@[simp]
|
||||
theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] :
|
||||
t.minKey?.isNone = t.isEmpty :=
|
||||
|
|
@ -1801,6 +1809,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] {k km} :
|
|||
cmp km k |>.isLE :=
|
||||
DTreeMap.minKey?_le_of_mem
|
||||
|
||||
theorem le_minKey? [TransCmp cmp] {k} :
|
||||
(∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
|
||||
(∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.le_minKey?
|
||||
|
||||
theorem getKey?_minKey? [TransCmp cmp] {km} :
|
||||
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
|
||||
DTreeMap.getKey?_minKey?
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_bind_getKey? [TransCmp cmp] :
|
||||
t.minKey?.bind t.getKey? = t.minKey? :=
|
||||
|
|
@ -1828,6 +1845,55 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
DTreeMap.minKey?_le_minKey?_erase
|
||||
|
||||
theorem minKey?_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).minKey? =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.minKey?_insertIfNew
|
||||
|
||||
theorem isSome_minKey?_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).minKey?.isSome :=
|
||||
DTreeMap.isSome_minKey?_insertIfNew
|
||||
|
||||
theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew k v |>.minKey? |>.get isSome_minKey?_insertIfNew) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
DTreeMap.minKey?_insertIfNew_le_minKey?
|
||||
|
||||
theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
|
||||
(hkmi : (t.insertIfNew k v |>.minKey?.get isSome_minKey?_insertIfNew) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
DTreeMap.minKey?_insertIfNew_le_self
|
||||
|
||||
theorem minKey?_modify [TransCmp cmp] {k f} :
|
||||
(t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
|
||||
DTreeMap.Const.minKey?_modify
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
|
||||
(t.modify k f).minKey? = t.minKey? :=
|
||||
DTreeMap.Const.minKey?_modify_eq_minKey?
|
||||
|
||||
theorem isSome_minKey?_modify [TransCmp cmp] {k f} :
|
||||
(t.modify k f).minKey?.isSome = !t.isEmpty :=
|
||||
DTreeMap.Const.isSome_minKey?_modify
|
||||
|
||||
theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] {k f} :
|
||||
(t.modify k f).minKey?.isSome = t.minKey?.isSome :=
|
||||
DTreeMap.Const.isSome_minKey?_modify_eq_isSome
|
||||
|
||||
theorem compare_minKey?_modify_eq [TransCmp cmp] {k f km kmm} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmm : (t.modify k f |>.minKey? |>.get <|
|
||||
isSome_minKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) →
|
||||
cmp kmm km = .eq :=
|
||||
DTreeMap.Const.compare_minKey?_modify_eq
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] {k f} :
|
||||
(t.alter k f).minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Const.minKey?_alter_eq_self
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap
|
||||
|
|
|
|||
|
|
@ -1757,6 +1757,14 @@ theorem minKey?_eq_none_iff [TransCmp cmp] (h : t.WF) :
|
|||
t.minKey? = none ↔ t.isEmpty :=
|
||||
DTreeMap.Raw.minKey?_eq_none_iff h
|
||||
|
||||
theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
|
||||
|
||||
theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
|
||||
t.minKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey?_eq_some_iff_mem_and_forall h
|
||||
|
||||
@[simp]
|
||||
theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
|
||||
t.minKey?.isNone = t.isEmpty :=
|
||||
|
|
@ -1810,6 +1818,15 @@ theorem minKey?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
|
|||
cmp km k |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_le_of_mem h
|
||||
|
||||
theorem le_minKey? [TransCmp cmp] {k} (h : t.WF) :
|
||||
(∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔
|
||||
(∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.Raw.le_minKey? h
|
||||
|
||||
theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
|
||||
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
|
||||
DTreeMap.Raw.getKey?_minKey? h
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
|
||||
t.minKey?.bind t.getKey? = t.minKey? :=
|
||||
|
|
@ -1837,6 +1854,55 @@ theorem minKey?_le_minKey?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_le_minKey?_erase h
|
||||
|
||||
theorem minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).minKey? =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.Raw.minKey?_insertIfNew h
|
||||
|
||||
theorem isSome_minKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).minKey?.isSome :=
|
||||
DTreeMap.Raw.isSome_minKey?_insertIfNew h
|
||||
|
||||
theorem minKey?_insertIfNew_le_minKey? [TransCmp cmp] (h : t.WF) {k v km kmi} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmi : (t.insertIfNew k v |>.minKey? |>.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_insertIfNew_le_minKey? h
|
||||
|
||||
theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
|
||||
(hkmi : (t.insertIfNew k v |>.minKey?.get <| isSome_minKey?_insertIfNew h) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_insertIfNew_le_self h
|
||||
|
||||
theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
|
||||
DTreeMap.Raw.Const.minKey?_modify h
|
||||
|
||||
@[simp]
|
||||
theorem minKey?_modify_eq_minKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} :
|
||||
(t.modify k f).minKey? = t.minKey? :=
|
||||
DTreeMap.Raw.Const.minKey?_modify_eq_minKey? h
|
||||
|
||||
theorem isSome_minKey?_modify [TransCmp cmp] {k f} (h : t.WF) :
|
||||
(t.modify k f).minKey?.isSome = !t.isEmpty :=
|
||||
DTreeMap.Raw.Const.isSome_minKey?_modify h
|
||||
|
||||
theorem isSome_minKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(t.modify k f).minKey?.isSome = t.minKey?.isSome :=
|
||||
DTreeMap.Raw.Const.isSome_minKey?_modify_eq_isSome h
|
||||
|
||||
theorem compare_minKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} :
|
||||
(hkm : t.minKey? = some km) →
|
||||
(hkmm : (t.modify k f |>.minKey? |>.get <|
|
||||
(isSome_minKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) →
|
||||
cmp kmm km = .eq :=
|
||||
DTreeMap.Raw.Const.compare_minKey?_modify_eq h
|
||||
|
||||
theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
|
||||
(t.alter k f).minKey? = some k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Raw.Const.minKey?_alter_eq_self h
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -660,76 +660,112 @@ section Min
|
|||
@[simp]
|
||||
theorem min?_emptyc :
|
||||
(∅ : TreeSet α cmp).min? = none :=
|
||||
DTreeMap.minKey?_emptyc
|
||||
TreeMap.minKey?_emptyc
|
||||
|
||||
theorem min?_of_isEmpty [TransCmp cmp] :
|
||||
(he : t.isEmpty) → t.min? = none :=
|
||||
DTreeMap.minKey?_of_isEmpty
|
||||
TreeMap.minKey?_of_isEmpty
|
||||
|
||||
@[simp]
|
||||
theorem min?_eq_none_iff [TransCmp cmp] :
|
||||
t.min? = none ↔ t.isEmpty :=
|
||||
DTreeMap.minKey?_eq_none_iff
|
||||
TreeMap.minKey?_eq_none_iff
|
||||
|
||||
theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} :
|
||||
t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
TreeMap.minKey?_eq_some_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem min?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} :
|
||||
t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
TreeMap.minKey?_eq_some_iff_mem_and_forall
|
||||
|
||||
@[simp]
|
||||
theorem isNone_min?_eq_isEmpty [TransCmp cmp] :
|
||||
t.min?.isNone = t.isEmpty :=
|
||||
DTreeMap.isNone_minKey?_eq_isEmpty
|
||||
TreeMap.isNone_minKey?_eq_isEmpty
|
||||
|
||||
@[simp]
|
||||
theorem isSome_min?_eq_not_isEmpty [TransCmp cmp] :
|
||||
t.min?.isSome = !t.isEmpty :=
|
||||
DTreeMap.isSome_minKey?_eq_not_isEmpty
|
||||
TreeMap.isSome_minKey?_eq_not_isEmpty
|
||||
|
||||
theorem min?_insert [TransCmp cmp] {k} :
|
||||
(t.insert k).min? =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
TreeMap.minKey?_insertIfNew
|
||||
|
||||
theorem isSome_min?_insert [TransCmp cmp] {k} :
|
||||
(t.insert k).min?.isSome :=
|
||||
TreeMap.isSome_minKey?_insertIfNew
|
||||
|
||||
theorem min?_insert_le_min? [TransCmp cmp] {k km kmi} :
|
||||
(hkm : t.min? = some km) →
|
||||
(hkmi : (t.insert k |>.min? |>.get isSome_min?_insert) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
TreeMap.minKey?_insertIfNew_le_minKey?
|
||||
|
||||
theorem min?_insert_le_self [TransCmp cmp] {k kmi} :
|
||||
(hkmi : (t.insert k |>.min?.get isSome_min?_insert) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
TreeMap.minKey?_insertIfNew_le_self
|
||||
|
||||
theorem contains_min? [TransCmp cmp] {km} :
|
||||
(hkm : t.min? = some km) →
|
||||
t.contains km :=
|
||||
DTreeMap.contains_minKey?
|
||||
TreeMap.contains_minKey?
|
||||
|
||||
theorem isSome_min?_of_contains [TransCmp cmp] {k} :
|
||||
(hc : t.contains k) → t.min?.isSome :=
|
||||
DTreeMap.isSome_minKey?_of_contains
|
||||
TreeMap.isSome_minKey?_of_contains
|
||||
|
||||
theorem isSome_min?_of_mem [TransCmp cmp] {k} :
|
||||
k ∈ t → t.min?.isSome :=
|
||||
DTreeMap.isSome_minKey?_of_mem
|
||||
TreeMap.isSome_minKey?_of_mem
|
||||
|
||||
theorem min?_le_of_contains [TransCmp cmp] {k km} :
|
||||
(hc : t.contains k) → (hkm : (t.min?.get <| isSome_min?_of_contains hc) = km) →
|
||||
cmp km k |>.isLE :=
|
||||
DTreeMap.minKey?_le_of_contains
|
||||
TreeMap.minKey?_le_of_contains
|
||||
|
||||
theorem min?_le_of_mem [TransCmp cmp] {k km} :
|
||||
(hc : k ∈ t) → (hkm : (t.min?.get <| isSome_min?_of_mem hc) = km) →
|
||||
cmp km k |>.isLE :=
|
||||
DTreeMap.minKey?_le_of_mem
|
||||
TreeMap.minKey?_le_of_mem
|
||||
|
||||
theorem le_min? [TransCmp cmp] {k} :
|
||||
(∀ k', t.min? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
TreeMap.le_minKey?
|
||||
|
||||
theorem get?_min? [TransCmp cmp] {km} :
|
||||
(hkm : t.min? = some km) → t.get? km = some km :=
|
||||
DTreeMap.getKey?_minKey?
|
||||
|
||||
@[simp]
|
||||
theorem min?_bind_get? [TransCmp cmp] :
|
||||
t.min?.bind t.get? = t.min? :=
|
||||
DTreeMap.minKey?_bind_getKey?
|
||||
TreeMap.minKey?_bind_getKey?
|
||||
|
||||
theorem min?_erase_eq_iff_not_compare_eq_min? [TransCmp cmp] {k} :
|
||||
(t.erase k |>.min?) = t.min? ↔
|
||||
∀ {km}, t.min? = some km → ¬ cmp k km = .eq :=
|
||||
DTreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey?
|
||||
TreeMap.minKey?_erase_eq_iff_not_compare_eq_minKey?
|
||||
|
||||
theorem min?_erase_eq_of_not_compare_eq_min? [TransCmp cmp] {k} :
|
||||
(hc : ∀ {km}, t.min? = some km → ¬ cmp k km = .eq) →
|
||||
(t.erase k |>.min?) = t.min? :=
|
||||
DTreeMap.minKey?_erase_eq_of_not_compare_eq_minKey?
|
||||
TreeMap.minKey?_erase_eq_of_not_compare_eq_minKey?
|
||||
|
||||
theorem isSome_min?_of_isSome_min?_erase [TransCmp cmp] {k} :
|
||||
(hs : t.erase k |>.min?.isSome) →
|
||||
t.min?.isSome :=
|
||||
DTreeMap.isSome_minKey?_of_isSome_minKey?_erase
|
||||
TreeMap.isSome_minKey?_of_isSome_minKey?_erase
|
||||
|
||||
theorem min?_le_min?_erase [TransCmp cmp] {k km kme} :
|
||||
(hkme : (t.erase k |>.min?) = some kme) →
|
||||
(hkm : (t.min?.get <|
|
||||
isSome_min?_of_isSome_min?_erase <| hkme ▸ Option.isSome_some) = km) →
|
||||
cmp km kme |>.isLE :=
|
||||
DTreeMap.minKey?_le_minKey?_erase
|
||||
TreeMap.minKey?_le_minKey?_erase
|
||||
|
||||
end Min
|
||||
|
||||
|
|
|
|||
|
|
@ -658,76 +658,112 @@ section Min
|
|||
@[simp]
|
||||
theorem min?_emptyc :
|
||||
(empty : Raw α cmp).min? = none :=
|
||||
DTreeMap.Raw.minKey?_emptyc
|
||||
TreeMap.Raw.minKey?_emptyc
|
||||
|
||||
theorem min?_of_isEmpty [TransCmp cmp] (h : t.WF) :
|
||||
(he : t.isEmpty) → t.min? = none :=
|
||||
DTreeMap.Raw.minKey?_of_isEmpty h
|
||||
TreeMap.Raw.minKey?_of_isEmpty h
|
||||
|
||||
@[simp]
|
||||
theorem min?_eq_none_iff [TransCmp cmp] (h : t.WF) :
|
||||
t.min? = none ↔ t.isEmpty :=
|
||||
DTreeMap.Raw.minKey?_eq_none_iff h
|
||||
TreeMap.Raw.minKey?_eq_none_iff h
|
||||
|
||||
theorem min?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} :
|
||||
t.min? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall h
|
||||
|
||||
theorem min?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} :
|
||||
t.min? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey?_eq_some_iff_mem_and_forall h
|
||||
|
||||
@[simp]
|
||||
theorem isNone_min?_eq_isEmpty [TransCmp cmp] (h : t.WF) :
|
||||
t.min?.isNone = t.isEmpty :=
|
||||
DTreeMap.Raw.isNone_minKey?_eq_isEmpty h
|
||||
TreeMap.Raw.isNone_minKey?_eq_isEmpty h
|
||||
|
||||
@[simp]
|
||||
theorem isSome_min?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) :
|
||||
t.min?.isSome = !t.isEmpty :=
|
||||
DTreeMap.Raw.isSome_minKey?_eq_not_isEmpty h
|
||||
TreeMap.Raw.isSome_minKey?_eq_not_isEmpty h
|
||||
|
||||
theorem min?_insert [TransCmp cmp] (h : t.WF) {k} :
|
||||
(t.insert k).min? =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
TreeMap.Raw.minKey?_insertIfNew h
|
||||
|
||||
theorem isSome_min?_insert [TransCmp cmp] (h : t.WF) {k} :
|
||||
(t.insert k).min?.isSome :=
|
||||
TreeMap.Raw.isSome_minKey?_insertIfNew h
|
||||
|
||||
theorem min?_insert_le_min? [TransCmp cmp] (h : t.WF) {k km kmi} :
|
||||
(hkm : t.min? = some km) →
|
||||
(hkmi : (t.insert k |>.min? |>.get <| isSome_min?_insert h) = kmi) →
|
||||
cmp kmi km |>.isLE :=
|
||||
TreeMap.Raw.minKey?_insertIfNew_le_minKey? h
|
||||
|
||||
theorem min?_insert_le_self [TransCmp cmp] (h : t.WF) {k kmi} :
|
||||
(hkmi : (t.insert k |>.min?.get <| isSome_min?_insert h) = kmi) →
|
||||
cmp kmi k |>.isLE :=
|
||||
TreeMap.Raw.minKey?_insertIfNew_le_self h
|
||||
|
||||
theorem contains_min? [TransCmp cmp] (h : t.WF) {km} :
|
||||
(hkm : t.min? = some km) →
|
||||
t.contains km :=
|
||||
DTreeMap.Raw.contains_minKey? h
|
||||
TreeMap.Raw.contains_minKey? h
|
||||
|
||||
theorem isSome_min?_of_contains [TransCmp cmp] (h : t.WF) {k} :
|
||||
(hc : t.contains k) → t.min?.isSome :=
|
||||
DTreeMap.Raw.isSome_minKey?_of_contains h
|
||||
TreeMap.Raw.isSome_minKey?_of_contains h
|
||||
|
||||
theorem isSome_min?_of_mem [TransCmp cmp] (h : t.WF) {k} :
|
||||
k ∈ t → t.min?.isSome :=
|
||||
DTreeMap.Raw.isSome_minKey?_of_mem h
|
||||
TreeMap.Raw.isSome_minKey?_of_mem h
|
||||
|
||||
theorem min?_le_of_contains [TransCmp cmp] (h : t.WF) {k km} :
|
||||
(hc : t.contains k) → (hkm : (t.min?.get <| isSome_min?_of_contains h hc) = km) →
|
||||
cmp km k |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_le_of_contains h
|
||||
TreeMap.Raw.minKey?_le_of_contains h
|
||||
|
||||
theorem min?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} :
|
||||
(hc : k ∈ t) → (hkm : (t.min?.get <| isSome_min?_of_mem h hc) = km) →
|
||||
cmp km k |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_le_of_mem h
|
||||
TreeMap.Raw.minKey?_le_of_mem h
|
||||
|
||||
theorem le_min? [TransCmp cmp] {k} (h : t.WF) :
|
||||
(∀ k', t.min? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
TreeMap.Raw.le_minKey? h
|
||||
|
||||
theorem get?_min? [TransCmp cmp] (h : t.WF) {km} :
|
||||
(hkm : t.min? = some km) → t.get? km = some km :=
|
||||
TreeMap.Raw.getKey?_minKey? h
|
||||
|
||||
@[simp]
|
||||
theorem min?_bind_get? [TransCmp cmp] (h : t.WF) :
|
||||
t.min?.bind t.get? = t.min? :=
|
||||
DTreeMap.Raw.minKey?_bind_getKey? h
|
||||
TreeMap.Raw.minKey?_bind_getKey? h
|
||||
|
||||
theorem min?_erase_eq_iff_not_compare_eq_min? [TransCmp cmp] (h : t.WF) {k} :
|
||||
(t.erase k |>.min?) = t.min? ↔
|
||||
∀ {km}, t.min? = some km → ¬ cmp k km = .eq :=
|
||||
DTreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? h
|
||||
TreeMap.Raw.minKey?_erase_eq_iff_not_compare_eq_minKey? h
|
||||
|
||||
theorem min?_erase_eq_of_not_compare_eq_min? [TransCmp cmp] (h : t.WF) {k} :
|
||||
(hc : ∀ {km}, t.min? = some km → ¬ cmp k km = .eq) →
|
||||
(t.erase k |>.min?) = t.min? :=
|
||||
DTreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? h
|
||||
TreeMap.Raw.minKey?_erase_eq_of_not_compare_eq_minKey? h
|
||||
|
||||
theorem isSome_min?_of_isSome_min?_erase [TransCmp cmp] (h : t.WF) {k} :
|
||||
(hs : t.erase k |>.min?.isSome) →
|
||||
t.min?.isSome :=
|
||||
DTreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase h
|
||||
TreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase h
|
||||
|
||||
theorem min?_le_min?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
|
||||
(hkme : (t.erase k |>.min?) = some kme) →
|
||||
(hkm : (t.min?.get <|
|
||||
isSome_min?_of_isSome_min?_erase h <| hkme ▸ Option.isSome_some) = km) →
|
||||
cmp km kme |>.isLE :=
|
||||
DTreeMap.Raw.minKey?_le_minKey?_erase h
|
||||
TreeMap.Raw.minKey?_le_minKey?_erase h
|
||||
|
||||
end Min
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue