feat: tree map lemmas for minKey! (#7600)
This PR provides lemmas about the tree map function `minKey!` and its interactions 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
0a96b4cf72
commit
3c2d81d3c0
10 changed files with 1097 additions and 17 deletions
|
|
@ -97,7 +97,8 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
|
|||
⟨`forIn, (``forIn_eq_forIn_toListModel, #[])⟩,
|
||||
⟨`forM, (``forM_eq_forM, #[])⟩,
|
||||
⟨`minKey?, (``minKey?_eq_minKey?, #[``(minKey?_of_perm _)])⟩,
|
||||
⟨`minKey, (``minKey_eq_minKey, #[``(minKey_of_perm _)])⟩]
|
||||
⟨`minKey, (``minKey_eq_minKey, #[``(minKey_of_perm _)])⟩,
|
||||
⟨`minKey!, (``minKey!_eq_minKey!, #[``(minKey!_of_perm _)])⟩]
|
||||
|
||||
/-- Internal implementation detail of the tree map -/
|
||||
scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
|
||||
|
|
@ -172,6 +173,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransOrd α] (h : t.WF) :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t := by
|
||||
simpa only [mem_iff_contains] using isEmpty_eq_false_iff_exists_contains_eq_true h
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransOrd α] (h : t.WF) {a : α} : (hc : t.contains a = true) →
|
||||
t.isEmpty = false := by
|
||||
simp_to_model [isEmpty, contains] using List.isEmpty_eq_false_of_containsKey
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransOrd α] (h : t.WF) :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false := by
|
||||
simp_to_model [isEmpty, contains] using List.isEmpty_iff_forall_containsKey
|
||||
|
|
@ -276,14 +281,14 @@ theorem isEmpty_erase! [TransOrd α] (h : t.WF) {k : α} :
|
|||
(t.erase! k).isEmpty = (t.isEmpty || (t.size = 1 && t.contains k)) := by
|
||||
simpa only [erase_eq_erase!] using isEmpty_erase h
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransOrd α] (h : t.WF) (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransOrd α] (h : t.WF) (k : α) :
|
||||
t.isEmpty = ((t.erase k h.balanced).impl.isEmpty && !(t.contains k)) := by
|
||||
simp_to_model [erase, isEmpty, contains] using
|
||||
List.isEmpty_eq_isEmpty_eraseKey_and_not_containsKey
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase!_and_not_containsKey [TransOrd α] (h : t.WF) (k : α) :
|
||||
t.isEmpty = ((t.erase! k).isEmpty && !(t.contains k)) := by
|
||||
simpa [erase_eq_erase!] using isEmpty_eq_isEmpty_erase_and_not_containsKey h k
|
||||
simpa [erase_eq_erase!] using isEmpty_eq_isEmpty_erase_and_not_contains h k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransOrd α] (h : t.WF) {k : α} :
|
||||
(he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
|
|
@ -4505,7 +4510,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.
|
|||
|
||||
theorem minKey_insert [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insert k v h.balanced).impl.minKey (isEmpty_insert h) =
|
||||
(t.minKey?).elim k fun k' => if compare k k'|>.isLE then k else k' := by
|
||||
t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k' := by
|
||||
simp_to_model [insert, minKey, minKey?] using List.minKey_insertEntry
|
||||
|
||||
theorem minKey_insert_le_minKey [TransOrd α] (h : t.WF) {k v he} :
|
||||
|
|
@ -4620,6 +4625,212 @@ theorem minKey_alter_eq_self [TransOrd α] (h : t.WF) {k f he} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem minKey_eq_minKey! [TransOrd α] [Inhabited α] (h : t.WF) {he} :
|
||||
t.minKey he = t.minKey! := by
|
||||
simp_to_model [minKey, minKey!] using List.minKey_eq_minKey!
|
||||
|
||||
theorem minKey?_eq_some_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.minKey? = some t.minKey! := by
|
||||
simp_to_model [minKey?, minKey!, isEmpty] using List.minKey?_eq_some_minKey!
|
||||
|
||||
theorem minKey!_eq_default [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty) → t.minKey! = default := by
|
||||
simp_to_model [minKey!, isEmpty] using List.minKey!_eq_default
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km},
|
||||
t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (compare km k).isLE := by
|
||||
simp_to_model [minKey!, getKey?, contains, isEmpty] using
|
||||
List.minKey!_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [TransOrd α]
|
||||
[LawfulEqOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km},
|
||||
t.minKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (compare km k).isLE := by
|
||||
simp_to_model [minKey!, contains, isEmpty] using List.minKey!_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem minKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v h.balanced |>.impl.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by
|
||||
simp_to_model [minKey!, minKey?, insert] using List.minKey!_insertEntry
|
||||
|
||||
theorem minKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert! k v |>.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by
|
||||
simpa [insert_eq_insert!] using minKey!_insert h
|
||||
|
||||
theorem minKey!_insert_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare (t.insert k v h.balanced |>.impl.minKey!) t.minKey! |>.isLE := by
|
||||
simp_to_model [minKey!, isEmpty, insert] using List.minKey!_insertEntry_le_minKey!
|
||||
|
||||
theorem minKey!_insert!_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare (t.insert! k v |>.minKey!) t.minKey! |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using minKey!_insert_le_minKey! h
|
||||
|
||||
theorem minKey!_insert_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare (t.insert k v h.balanced |>.impl.minKey!) k |>.isLE := by
|
||||
simp_to_model [minKey!, insert] using List.minKey!_insertEntry_le_self
|
||||
|
||||
theorem minKey!_insert!_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare (t.insert! k v |>.minKey!) k |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using minKey!_insert_le_self h
|
||||
|
||||
theorem contains_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.contains t.minKey! := by
|
||||
simp_to_model [minKey!, isEmpty, contains] using List.containsKey_minKey!
|
||||
|
||||
theorem minKey!_mem [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.minKey! ∈ t :=
|
||||
contains_minKey! h
|
||||
|
||||
theorem minKey!_le_of_contains [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (hc : t.contains k) →
|
||||
compare t.minKey! k |>.isLE := by
|
||||
simp_to_model [minKey!, contains] using List.minKey!_le_of_containsKey
|
||||
|
||||
theorem minKey!_le_of_mem [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (hc : k ∈ t) →
|
||||
compare t.minKey! k |>.isLE :=
|
||||
minKey!_le_of_contains h
|
||||
|
||||
theorem le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k},
|
||||
(compare k t.minKey!).isLE ↔ (∀ k', k' ∈ t → (compare k k').isLE) := by
|
||||
simp_to_model [minKey!, contains, isEmpty] using List.le_minKey!
|
||||
|
||||
theorem getKey?_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) →
|
||||
t.getKey? t.minKey! = some t.minKey! := by
|
||||
simp_to_model [minKey!, getKey?, isEmpty] using List.getKey?_minKey!
|
||||
|
||||
theorem getKey_minKey! [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {he},
|
||||
t.getKey t.minKey! he = t.minKey! := by
|
||||
simp_to_model [minKey!, contains, isEmpty, getKey] using List.getKey_minKey!
|
||||
|
||||
theorem getKey_minKey!_eq_minKey [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {hc},
|
||||
t.getKey t.minKey! hc = t.minKey (isEmpty_eq_false_of_contains h hc) := by
|
||||
simp_to_model [minKey!, minKey, contains, isEmpty, getKey] using List.getKey_minKey!_eq_minKey
|
||||
|
||||
theorem getKey!_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.getKey! t.minKey! = t.minKey! := by
|
||||
simp_to_model [minKey!, isEmpty, getKey!] using List.getKey!_minKey!
|
||||
|
||||
theorem getKeyD_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback},
|
||||
t.getKeyD t.minKey! fallback = t.minKey! := by
|
||||
simp_to_model [minKey!, getKeyD, isEmpty] using List.getKeyD_minKey!
|
||||
|
||||
theorem minKey!_erase_eq_iff_not_compare_minKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
(t.erase k h.balanced |>.impl.minKey!) = t.minKey! ↔
|
||||
¬ compare k t.minKey! = .eq := by
|
||||
simp_to_model [minKey!, isEmpty, erase] using List.minKey!_eraseKey_eq_iff_beq_minKey!_eq_false
|
||||
|
||||
theorem minKey!_erase!_eq_iff_not_compare_minKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) →
|
||||
(t.erase! k |>.minKey!) = t.minKey! ↔
|
||||
¬ compare k t.minKey! = .eq := by
|
||||
simpa only [erase_eq_erase!] using minKey!_erase_eq_iff_not_compare_minKey!_eq h
|
||||
|
||||
theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) → (heq : ¬ compare k t.minKey! = .eq) →
|
||||
(t.erase k h.balanced |>.impl.minKey!) = t.minKey! := by
|
||||
simp_to_model [minKey!, isEmpty, erase] using
|
||||
List.minKey!_eraseKey_eq_of_beq_minKey!_eq_false
|
||||
|
||||
theorem minKey!_erase!_eq_of_not_compare_minKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) → (heq : ¬ compare k t.minKey! = .eq) →
|
||||
(t.erase! k |>.minKey!) = t.minKey! := by
|
||||
simpa only [erase_eq_erase!] using minKey!_erase_eq_of_not_compare_minKey!_eq h
|
||||
|
||||
theorem minKey!_le_minKey!_erase [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
compare t.minKey! (t.erase k h.balanced |>.impl.minKey!) |>.isLE := by
|
||||
simp_to_model [minKey!, isEmpty, erase] using List.minKey!_le_minKey!_erase
|
||||
|
||||
theorem minKey!_le_minKey!_erase! [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) →
|
||||
compare t.minKey! (t.erase! k |>.minKey!) |>.isLE := by
|
||||
simpa only [erase_eq_erase!] using minKey!_le_minKey!_erase h
|
||||
|
||||
theorem minKey!_insertIfNew [TransOrd α] [Inhabited α] (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 [minKey!, minKey?, insertIfNew] using List.minKey!_insertEntryIfNew
|
||||
|
||||
theorem minKey!_insertIfNew! [TransOrd α] [Inhabited α] (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 minKey!_insertIfNew_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare (t.insertIfNew k v h.balanced |>.impl.minKey!) t.minKey! |>.isLE := by
|
||||
simp_to_model [minKey!, isEmpty, insertIfNew] using List.minKey!_insertEntryIfNew_le_minKey!
|
||||
|
||||
theorem minKey!_insertIfNew!_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare (t.insertIfNew! k v |>.minKey!) t.minKey! |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_le_minKey! h
|
||||
|
||||
theorem minKey!_insertIfNew_le_self [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k v},
|
||||
compare (t.insertIfNew k v h.balanced |>.impl.minKey!) k |>.isLE := by
|
||||
simp_to_model [minKey!, insertIfNew] using List.minKey!_insertEntryIfNew_le_self
|
||||
|
||||
theorem minKey!_insertIfNew!_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare (t.insertIfNew! k v |>.minKey!) k |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_le_self h
|
||||
|
||||
theorem minKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
|
||||
(t.modify k f |>.minKey!) = t.minKey! := by
|
||||
simp_to_model [minKey!, modify] using List.minKey!_modifyKey
|
||||
|
||||
theorem minKey!_alter_eq_self [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (he : (t.alter k f h.balanced).impl.isEmpty = false) →
|
||||
(t.alter k f h.balanced |>.impl.minKey!) = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [minKey!, alter, isEmpty, contains, get?] using List.minKey!_alterKey_eq_self
|
||||
|
||||
theorem minKey!_alter!_eq_self [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) {k f} :
|
||||
(he : (t.alter! k f).isEmpty = false) →
|
||||
(t.alter! k f |>.minKey!) = 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 α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (he : (modify k f t).isEmpty = false) →
|
||||
(modify k f t |> minKey!) = if compare t.minKey! k = .eq then k else t.minKey! := by
|
||||
simp_to_model [minKey!, minKey, isEmpty, Const.modify] using List.Const.minKey!_modifyKey
|
||||
|
||||
theorem minKey!_modify_eq_minKey! [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (modify k f t |> minKey!) = t.minKey! := by
|
||||
simp_to_model [minKey!, Const.modify] using List.Const.minKey!_modifyKey_eq_minKey!
|
||||
|
||||
theorem compare_minKey!_modify_eq [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
|
||||
compare (Const.modify k f t |> minKey!) t.minKey! = .eq := by
|
||||
simp_to_model [minKey!, Const.modify] using List.Const.minKey!_modifyKey_beq
|
||||
|
||||
theorem minKey!_alter_eq_self [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (he : (alter k f t h.balanced).impl.isEmpty = false) →
|
||||
(alter k f t h.balanced |>.impl.minKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [minKey!, Const.alter, contains, isEmpty, Const.get?] using
|
||||
List.Const.minKey!_alterKey_eq_self
|
||||
|
||||
theorem minKey!_alter!_eq_self [TransOrd α] [Inhabited α] (h : t.WF) {k f} :
|
||||
(he : (alter! k f t).isEmpty = false) →
|
||||
(alter! k f t |>.minKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simpa only [alter_eq_alter!] using minKey!_alter_eq_self h
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -476,6 +476,10 @@ theorem minEntry_eq_get_minEntry? [Ord α] {l : Impl α β} {he} :
|
|||
theorem minKey_eq_minEntry_fst [Ord α] {l : Impl α β} {he} : l.minKey he = (l.minEntry he).fst := by
|
||||
induction l, he using minKey.induct <;> simp only [minKey, minEntry] <;> trivial
|
||||
|
||||
theorem minKey!_eq_get!_minKey? [Ord α] [Inhabited α] {l : Impl α β} :
|
||||
l.minKey! = l.minKey?.get! := by
|
||||
induction l using minKey!.induct <;> simp_all only [minKey!, minKey?] <;> rfl
|
||||
|
||||
theorem balanceL_eq_balance {k : α} {v : β k} {l r : Impl α β} {hlb hrb hlr} :
|
||||
balanceL k v l r hlb hrb hlr = balance k v l r hlb hrb (Or.inl hlr.erase) := by
|
||||
rw [balanceL_eq_balanceLErase, balanceLErase_eq_balanceL!,
|
||||
|
|
|
|||
|
|
@ -1833,4 +1833,8 @@ theorem minKey_eq_minKey [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordere
|
|||
simp [minKey_eq_get_minKey?, minKey_eq_minEntry_fst, minEntry_eq_get_minEntry?,
|
||||
minEntry?_eq_minEntry? hlo, List.minKey?, Option.get_map]
|
||||
|
||||
theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] {l : Impl α β} (hlo : l.Ordered) :
|
||||
l.minKey! = List.minKey! l.toListModel := by
|
||||
simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -72,6 +72,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
Impl.isEmpty_eq_false_iff_exists_mem t.wf
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
Impl.isEmpty_eq_false_of_contains t.wf hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
Impl.isEmpty_iff_forall_contains t.wf
|
||||
|
|
@ -145,9 +149,9 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
Impl.isEmpty_erase t.wf
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
Impl.isEmpty_eq_isEmpty_erase_and_not_containsKey t.wf k
|
||||
Impl.isEmpty_eq_isEmpty_erase_and_not_contains t.wf k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransCmp cmp] {k : α}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
|
|
@ -2977,7 +2981,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he k
|
|||
|
||||
theorem minKey_insert [TransCmp cmp] {k v} :
|
||||
(t.insert k v).minKey isEmpty_insert =
|
||||
(t.minKey?).elim k fun k' => if cmp k k'|>.isLE then k else k' :=
|
||||
t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k' :=
|
||||
Impl.minKey_insert t.wf
|
||||
|
||||
theorem minKey_insert_le_minKey [TransCmp cmp] {k v he} :
|
||||
|
|
@ -3087,6 +3091,7 @@ theorem minKey_modify_eq_minKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
|
|||
(modify t k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
Impl.Const.minKey_modify_eq_minKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKey_modify_eq [TransCmp cmp] {k f he} :
|
||||
cmp (modify t k f |>.minKey he)
|
||||
(t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
|
||||
|
|
@ -3099,6 +3104,138 @@ theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.minKey? = some t.minKey! :=
|
||||
Impl.minKey?_eq_some_minKey! t.wf he
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
Impl.minKey!_eq_default t.wf he
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKey!_eq_iff_getKey?_eq_self_and_forall t.wf he
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKey!_eq_some_iff_mem_and_forall t.wf he
|
||||
|
||||
theorem minKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insert k v |>.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') :=
|
||||
Impl.minKey!_insert t.wf
|
||||
|
||||
theorem minKey!_insert_le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insert k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
Impl.minKey!_insert_le_minKey! t.wf he
|
||||
|
||||
theorem minKey!_insert_le_self [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp (t.insert k v |>.minKey!) k |>.isLE :=
|
||||
Impl.minKey!_insert_le_self t.wf
|
||||
|
||||
theorem contains_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.minKey! :=
|
||||
Impl.contains_minKey! t.wf he
|
||||
|
||||
theorem minKey!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.minKey! ∈ t :=
|
||||
Impl.minKey!_mem t.wf he
|
||||
|
||||
theorem minKey!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
Impl.minKey!_le_of_contains t.wf hc
|
||||
|
||||
theorem minKey!_le_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
Impl.minKey!_le_of_mem t.wf hc
|
||||
|
||||
theorem le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.minKey!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKey! t.wf he
|
||||
|
||||
theorem getKey?_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey? t.minKey! = some t.minKey! :=
|
||||
Impl.getKey?_minKey! t.wf he
|
||||
|
||||
theorem getKey_minKey! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey! :=
|
||||
Impl.getKey_minKey! t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKey_minKey!_eq_minKey [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey (isEmpty_eq_false_of_contains hc) :=
|
||||
Impl.getKey_minKey!_eq_minKey t.wf
|
||||
|
||||
theorem getKey!_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey! t.minKey! = t.minKey! :=
|
||||
Impl.getKey!_minKey! t.wf he
|
||||
|
||||
theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.minKey! fallback = t.minKey! :=
|
||||
Impl.getKeyD_minKey! t.wf he
|
||||
|
||||
theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.minKey! = .eq) :
|
||||
(t.erase k |>.minKey!) = t.minKey! :=
|
||||
Impl.minKey!_erase_eq_of_not_compare_minKey!_eq t.wf he heq
|
||||
|
||||
theorem minKey!_le_minKey!_erase [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.minKey! (t.erase k |>.minKey!) |>.isLE :=
|
||||
Impl.minKey!_le_minKey!_erase t.wf he
|
||||
|
||||
theorem minKey!_insertIfNew [TransCmp cmp] [Inhabited α] {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 minKey!_insertIfNew_le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
Impl.minKey!_insertIfNew_le_minKey! t.wf he
|
||||
|
||||
theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
|
||||
Impl.minKey!_insertIfNew_le_self t.wf
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(t.modify k f |>.minKey!) = t.minKey! :=
|
||||
Impl.minKey!_modify t.wf
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f}
|
||||
(he : (t.alter k f).isEmpty = false) :
|
||||
(t.alter k f |>.minKey!) = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKey!_alter_eq_self t.wf he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : DTreeMap α β cmp}
|
||||
|
||||
theorem minKey!_modify [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
|
||||
Impl.Const.minKey!_modify t.wf he
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(modify t k f |>.minKey!) = t.minKey! :=
|
||||
Impl.Const.minKey!_modify_eq_minKey! t.wf
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
|
||||
cmp (modify t k f |> minKey!) t.minKey! = .eq :=
|
||||
Impl.Const.compare_minKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f |>.minKey!) = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKey!_alter_eq_self t.wf he
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -73,6 +73,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
Impl.isEmpty_eq_false_iff_exists_mem h
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] (h : t.WF) {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
Impl.isEmpty_eq_false_of_contains h hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
Impl.isEmpty_iff_forall_contains h
|
||||
|
|
@ -146,7 +150,7 @@ theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
Impl.isEmpty_erase! h
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
Impl.isEmpty_eq_isEmpty_erase!_and_not_containsKey h k
|
||||
|
||||
|
|
@ -2964,6 +2968,135 @@ theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.minKey? = some t.minKey! :=
|
||||
Impl.minKey?_eq_some_minKey! h he
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
Impl.minKey!_eq_default h he
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem minKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v |>.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') :=
|
||||
Impl.minKey!_insert! h
|
||||
|
||||
theorem minKey!_insert_le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v} :
|
||||
cmp (t.insert k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
Impl.minKey!_insert!_le_minKey! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKey!_insert_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp (t.insert k v |>.minKey!) k |>.isLE :=
|
||||
Impl.minKey!_insert!_le_self h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem contains_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.minKey! :=
|
||||
Impl.contains_minKey! h he
|
||||
|
||||
theorem minKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.minKey! ∈ t :=
|
||||
Impl.minKey!_mem h he
|
||||
|
||||
theorem minKey!_le_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
Impl.minKey!_le_of_contains h hc
|
||||
|
||||
theorem minKey!_le_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
Impl.minKey!_le_of_mem h hc
|
||||
|
||||
theorem le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.minKey!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKey! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem getKey?_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey? t.minKey! = some t.minKey! :=
|
||||
Impl.getKey?_minKey! h he
|
||||
|
||||
theorem getKey_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey! :=
|
||||
Impl.getKey_minKey! h
|
||||
|
||||
theorem getKey!_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey! t.minKey! = t.minKey! :=
|
||||
Impl.getKey!_minKey! h he
|
||||
|
||||
theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.minKey! fallback = t.minKey! :=
|
||||
Impl.getKeyD_minKey! h he
|
||||
|
||||
theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.minKey! = .eq) :
|
||||
(t.erase k |>.minKey!) = t.minKey! :=
|
||||
Impl.minKey!_erase!_eq_of_not_compare_minKey!_eq h he heq
|
||||
|
||||
theorem minKey!_le_minKey!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.minKey! (t.erase k |>.minKey!) |>.isLE :=
|
||||
Impl.minKey!_le_minKey!_erase! h he
|
||||
|
||||
theorem minKey!_insertIfNew [TransCmp cmp] [Inhabited α] (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 minKey!_insertIfNew_le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
Impl.minKey!_insertIfNew!_le_minKey! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
|
||||
Impl.minKey!_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(t.modify k f |>.minKey!) = t.minKey! :=
|
||||
Impl.minKey!_modify h
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (t.alter k f).isEmpty = false) :
|
||||
(t.alter k f |>.minKey!) = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKey!_alter!_eq_self h he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Raw α β cmp}
|
||||
|
||||
theorem minKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
|
||||
Impl.Const.minKey!_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(modify t k f |>.minKey!) = t.minKey! :=
|
||||
Impl.Const.minKey!_modify_eq_minKey! h
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
cmp (modify t k f |> minKey!) t.minKey! = .eq :=
|
||||
Impl.Const.compare_minKey!_modify_eq h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f |>.minKey!) = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKey!_alter!_eq_self h he
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -4945,6 +4945,192 @@ theorem minKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α
|
|||
|
||||
end Const
|
||||
|
||||
/-- Returns the smallest key in an associative list or panics if the list is empty. -/
|
||||
def minKey! [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) : α :=
|
||||
minKey? xs |>.get!
|
||||
|
||||
theorem minKey!_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
|
||||
minKey! l = minKey! l' := by
|
||||
simp [minKey!, minKey?_of_perm hd hp]
|
||||
|
||||
theorem minKey!_eq_get!_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} :
|
||||
minKey! l = (minKey? l).get! :=
|
||||
rfl
|
||||
|
||||
theorem minKey_eq_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} {he} :
|
||||
minKey l he = minKey! l := by
|
||||
simp [minKey_eq_get_minKey?, minKey!_eq_get!_minKey?, Option.get_eq_get!]
|
||||
|
||||
theorem minKey?_eq_some_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (he : l.isEmpty = false) :
|
||||
minKey? l = some (minKey! l) := by
|
||||
simp [← minKey_eq_minKey! (he := he), minKey_eq_get_minKey?]
|
||||
|
||||
theorem minKey!_eq_default [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (h : l.isEmpty) :
|
||||
minKey! l = default := by
|
||||
simp [minKey!, minKey?_eq_none_iff_isEmpty.mpr h]
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km} :
|
||||
minKey! l = km ↔ getKey? km l = some km ∧ ∀ k, containsKey k l → (compare km k).isLE := by
|
||||
simpa [minKey_eq_minKey!] using minKey_eq_iff_getKey?_eq_self_and_forall hd (he := he)
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(he : l.isEmpty = false) {km} :
|
||||
minKey! l = km ↔ containsKey km l ∧ ∀ k, containsKey k l → (compare km k).isLE := by
|
||||
simpa [minKey_eq_minKey!] using minKey_eq_some_iff_mem_and_forall hd (he := he)
|
||||
|
||||
theorem minKey!_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
(insertEntry k v l |> minKey!) =
|
||||
((minKey? l).elim k fun k' => if compare k k'|>.isLE then k else k') := by
|
||||
simpa [minKey_eq_minKey!] using minKey_insertEntry hd
|
||||
|
||||
theorem minKey!_insertEntry_le_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v} :
|
||||
compare (insertEntry k v l |> minKey!) (minKey! l) |>.isLE := by
|
||||
simpa [minKey_eq_minKey!] using minKey_insertEntry_le_minKey hd (he := he)
|
||||
|
||||
theorem minKey!_insertEntry_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare (insertEntry k v l |> minKey!) k |>.isLE := by
|
||||
simpa [minKey_eq_minKey!] using minKey_insertEntry_le_self hd
|
||||
|
||||
theorem containsKey_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
containsKey (minKey! l) l := by
|
||||
simpa [minKey_eq_minKey!] using containsKey_minKey hd (he := he)
|
||||
|
||||
theorem minKey!_le_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (hc : containsKey k l) :
|
||||
compare (minKey! l) k |>.isLE := by
|
||||
simpa [minKey_eq_minKey!] using minKey_le_of_containsKey hd hc
|
||||
|
||||
theorem le_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k} :
|
||||
(compare k (minKey! l)).isLE ↔ (∀ k', containsKey k' l → (compare k k').isLE) := by
|
||||
simpa [minKey_eq_minKey!] using le_minKey hd (he := he)
|
||||
|
||||
theorem getKey?_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
getKey? (minKey! l) l = some (minKey! l) := by
|
||||
simpa [minKey_eq_minKey!] using getKey?_minKey hd (he := he)
|
||||
|
||||
theorem getKey_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey (minKey! l) l he = minKey! l := by
|
||||
simpa [minKey_eq_minKey!] using getKey_minKey hd (he := isEmpty_eq_false_of_containsKey he)
|
||||
|
||||
theorem getKey_minKey!_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey (minKey! l) l he = minKey l (isEmpty_eq_false_of_containsKey he) := by
|
||||
simpa [minKey_eq_minKey!] using getKey_minKey hd (he := isEmpty_eq_false_of_containsKey he)
|
||||
|
||||
theorem getKey!_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
getKey! (minKey! l) l = minKey! l := by
|
||||
simpa [minKey_eq_minKey!] using getKey!_minKey hd (he := he)
|
||||
|
||||
theorem getKeyD_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback} :
|
||||
getKeyD (minKey! l) l fallback = minKey! l := by
|
||||
simpa [minKey_eq_minKey!] using getKeyD_minKey hd (he := he)
|
||||
|
||||
theorem minKey!_eraseKey_eq_iff_beq_minKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> minKey!) = minKey! l ↔ (k == (minKey! l)) = false := by
|
||||
simpa [minKey_eq_minKey!] using minKey_eraseKey_eq_iff_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKey!_eraseKey_eq_iff_beq_minKey!_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> minKey!) = minKey! l ↔ (k == (minKey! l)) = false := by
|
||||
simpa [minKey_eq_minKey!] using minKey_eraseKey_eq_iff_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKey!_eraseKey_eq_of_beq_minKey!_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) : (heq : (k == minKey! l) = false) →
|
||||
(eraseKey k l |> minKey!) = minKey! l := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_eraseKey_eq_of_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKey!_le_minKey!_erase [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (he : (eraseKey k l).isEmpty = false) :
|
||||
compare (minKey! l) (eraseKey k l |> minKey!) |>.isLE := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_le_minKey_erase hd (he := he)
|
||||
|
||||
theorem minKey!_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
(insertEntryIfNew k v l |> minKey!) =
|
||||
(minKey? l).elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_insertEntryIfNew hd
|
||||
|
||||
theorem minKey!_insertEntryIfNew_le_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v} :
|
||||
compare (insertEntryIfNew k v l |> minKey!) (minKey! l) |>.isLE := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_insertEntryIfNew_le_minKey hd (he := he)
|
||||
|
||||
theorem minKey!_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare (insertEntryIfNew k v l |> minKey!) k |>.isLE := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_insertEntryIfNew_le_self hd
|
||||
|
||||
theorem minKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> minKey!) = minKey! l := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKey!] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKey!_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f}
|
||||
(he : (alterKey k f l).isEmpty = false) :
|
||||
(alterKey k f l |> minKey!) = k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_alterKey_eq_self hd (he := he)
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
theorem minKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (modifyKey k f l).isEmpty = false) :
|
||||
(modifyKey k f l |> minKey!) = if (minKey! l) == k then k else (minKey! l) := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_modifyKey hd (he := he)
|
||||
|
||||
theorem minKey!_modifyKey_eq_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
[Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> minKey!) = minKey! l := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey_eq_minKey hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKey!] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKey!_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> minKey!) == (minKey! l) := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey_beq hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKey!] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKey!_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (alterKey k f l).isEmpty = false) :
|
||||
(alterKey k f l |> minKey!) = k ↔
|
||||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simpa only [minKey_eq_minKey!] using minKey_alterKey_eq_self hd (he := he)
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.Internal.List
|
||||
|
|
|
|||
|
|
@ -69,6 +69,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
DTreeMap.isEmpty_eq_false_iff_exists_mem
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
DTreeMap.isEmpty_eq_false_of_contains hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
DTreeMap.isEmpty_iff_forall_contains
|
||||
|
|
@ -142,9 +146,9 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
DTreeMap.isEmpty_erase
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
DTreeMap.isEmpty_eq_isEmpty_erase_and_not_containsKey k
|
||||
DTreeMap.isEmpty_eq_isEmpty_erase_and_not_contains k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransCmp cmp] {k : α}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
|
|
@ -1930,7 +1934,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he k
|
|||
|
||||
theorem minKey_insert [TransCmp cmp] {k v} :
|
||||
(t.insert k v).minKey isEmpty_insert =
|
||||
(t.minKey?).elim k fun k' => if cmp k k'|>.isLE then k else k' :=
|
||||
t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k' :=
|
||||
DTreeMap.minKey_insert
|
||||
|
||||
theorem minKey_insert_le_minKey [TransCmp cmp] {k v he} :
|
||||
|
|
@ -2036,6 +2040,122 @@ theorem minKey_alter_eq_self [TransCmp cmp] {k f he} :
|
|||
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Const.minKey_alter_eq_self
|
||||
|
||||
theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.minKey? = some t.minKey! :=
|
||||
DTreeMap.minKey?_eq_some_minKey! he
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
DTreeMap.minKey!_eq_default he
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKey!_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem minKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insert k v |>.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') :=
|
||||
DTreeMap.minKey!_insert
|
||||
|
||||
theorem minKey!_insert_le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insert k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
DTreeMap.minKey!_insert_le_minKey! he
|
||||
|
||||
theorem minKey!_insert_le_self [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp (t.insert k v |>.minKey!) k |>.isLE :=
|
||||
DTreeMap.minKey!_insert_le_self
|
||||
|
||||
theorem contains_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.minKey! :=
|
||||
DTreeMap.contains_minKey! he
|
||||
|
||||
theorem minKey!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.minKey! ∈ t :=
|
||||
DTreeMap.minKey!_mem he
|
||||
|
||||
theorem minKey!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
DTreeMap.minKey!_le_of_contains hc
|
||||
|
||||
theorem minKey!_le_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
DTreeMap.minKey!_le_of_mem hc
|
||||
|
||||
theorem le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.minKey!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.le_minKey! he
|
||||
|
||||
theorem getKey?_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey? t.minKey! = some t.minKey! :=
|
||||
DTreeMap.getKey?_minKey! he
|
||||
|
||||
theorem getKey_minKey! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey! :=
|
||||
DTreeMap.getKey_minKey!
|
||||
|
||||
@[simp]
|
||||
theorem getKey_minKey!_eq_minKey [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey (isEmpty_eq_false_of_contains hc) :=
|
||||
DTreeMap.getKey_minKey!_eq_minKey
|
||||
|
||||
theorem getKey!_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey! t.minKey! = t.minKey! :=
|
||||
DTreeMap.getKey!_minKey! he
|
||||
|
||||
theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.minKey! fallback = t.minKey! :=
|
||||
DTreeMap.getKeyD_minKey! he
|
||||
|
||||
theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.minKey! = .eq) :
|
||||
(t.erase k |>.minKey!) = t.minKey! :=
|
||||
DTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq he heq
|
||||
|
||||
theorem minKey!_le_minKey!_erase [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.minKey! (t.erase k |>.minKey!) |>.isLE :=
|
||||
DTreeMap.minKey!_le_minKey!_erase he
|
||||
|
||||
theorem minKey!_insertIfNew [TransCmp cmp] [Inhabited α] {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 minKey!_insertIfNew_le_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
DTreeMap.minKey!_insertIfNew_le_minKey! he
|
||||
|
||||
theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
|
||||
DTreeMap.minKey!_insertIfNew_le_self
|
||||
|
||||
theorem minKey!_modify [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
|
||||
DTreeMap.Const.minKey!_modify he
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(modify t k f |>.minKey!) = t.minKey! :=
|
||||
DTreeMap.Const.minKey!_modify_eq_minKey!
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
|
||||
cmp (modify t k f |> minKey!) t.minKey! = .eq :=
|
||||
DTreeMap.Const.compare_minKey!_modify_eq
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f |>.minKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Const.minKey!_alter_eq_self he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap
|
||||
|
|
|
|||
|
|
@ -70,6 +70,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] (h : t.WF) {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
DTreeMap.Raw.isEmpty_eq_false_of_contains h hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
DTreeMap.Raw.isEmpty_iff_forall_contains h
|
||||
|
|
@ -143,9 +147,9 @@ theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
DTreeMap.Raw.isEmpty_erase h
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
DTreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_containsKey h k
|
||||
DTreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_contains h k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransCmp cmp] (h : t.WF) {k : α}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
|
|
@ -1921,6 +1925,119 @@ theorem minKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
|
|||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Raw.Const.minKey?_alter_eq_self h
|
||||
|
||||
theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.minKey? = some t.minKey! :=
|
||||
DTreeMap.Raw.minKey?_eq_some_minKey! h he
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
DTreeMap.Raw.minKey!_eq_default h he
|
||||
|
||||
theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.minKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem minKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v |>.minKey!) =
|
||||
(t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') :=
|
||||
DTreeMap.Raw.minKey!_insert h
|
||||
|
||||
theorem minKey!_insert_le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v} :
|
||||
cmp (t.insert k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insert_le_minKey! h he
|
||||
|
||||
theorem minKey!_insert_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp (t.insert k v |>.minKey!) k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insert_le_self h
|
||||
|
||||
theorem contains_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.minKey! :=
|
||||
DTreeMap.Raw.contains_minKey! h he
|
||||
|
||||
theorem minKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.minKey! ∈ t :=
|
||||
DTreeMap.Raw.minKey!_mem h he
|
||||
|
||||
theorem minKey!_le_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_of_contains h hc
|
||||
|
||||
theorem minKey!_le_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp t.minKey! k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_of_mem h hc
|
||||
|
||||
theorem le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.minKey!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.Raw.le_minKey! h he
|
||||
|
||||
theorem getKey?_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey? t.minKey! = some t.minKey! :=
|
||||
DTreeMap.Raw.getKey?_minKey! h he
|
||||
|
||||
theorem getKey_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.getKey t.minKey! hc = t.minKey! :=
|
||||
DTreeMap.Raw.getKey_minKey! h
|
||||
|
||||
theorem getKey!_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey! t.minKey! = t.minKey! :=
|
||||
DTreeMap.Raw.getKey!_minKey! h he
|
||||
|
||||
theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.minKey! fallback = t.minKey! :=
|
||||
DTreeMap.Raw.getKeyD_minKey! h he
|
||||
|
||||
theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.minKey! = .eq) :
|
||||
(t.erase k |>.minKey!) = t.minKey! :=
|
||||
DTreeMap.Raw.minKey!_erase_eq_of_not_compare_minKey!_eq h he heq
|
||||
|
||||
theorem minKey!_le_minKey!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.minKey! (t.erase k |>.minKey!) |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_minKey!_erase h he
|
||||
|
||||
theorem minKey!_insertIfNew [TransCmp cmp] [Inhabited α] (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 minKey!_insertIfNew_le_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) t.minKey! |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew_le_minKey! h he
|
||||
|
||||
theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew_le_self h
|
||||
|
||||
theorem minKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
|
||||
DTreeMap.Raw.Const.minKey!_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem minKey!_modify_eq_minKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(modify t k f |>.minKey!) = t.minKey! :=
|
||||
DTreeMap.Raw.Const.minKey!_modify_eq_minKey! h
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
cmp (modify t k f |> minKey!) t.minKey! = .eq :=
|
||||
DTreeMap.Raw.Const.compare_minKey!_modify_eq h
|
||||
|
||||
theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f |>.minKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Raw.Const.minKey!_alter_eq_self h he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -69,6 +69,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
DTreeMap.isEmpty_eq_false_iff_exists_mem
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
DTreeMap.isEmpty_eq_false_of_contains hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
DTreeMap.isEmpty_iff_forall_contains
|
||||
|
|
@ -148,9 +152,9 @@ theorem isEmpty_erase [TransCmp cmp] {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
TreeMap.isEmpty_erase
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
DTreeMap.isEmpty_eq_isEmpty_erase_and_not_containsKey k
|
||||
DTreeMap.isEmpty_eq_isEmpty_erase_and_not_contains k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransCmp cmp] {k : α}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
|
|
@ -868,6 +872,88 @@ theorem min_le_min_erase [TransCmp cmp] {k he} :
|
|||
(t.erase k |>.min he) |>.isLE :=
|
||||
DTreeMap.minKey_le_minKey_erase
|
||||
|
||||
theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.min? = some t.min! :=
|
||||
DTreeMap.minKey?_eq_some_minKey! he
|
||||
|
||||
theorem min!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.min! = default :=
|
||||
DTreeMap.minKey!_eq_default he
|
||||
|
||||
theorem min!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.min! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem min!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.min! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKey!_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem min!_insert [TransCmp cmp] [Inhabited α] {k} :
|
||||
(t.insert k |>.min!) =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.minKey!_insertIfNew
|
||||
|
||||
theorem min!_insert_le_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
cmp (t.insert k |>.min!) t.min! |>.isLE :=
|
||||
DTreeMap.minKey!_insertIfNew_le_minKey! he
|
||||
|
||||
theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] {k} :
|
||||
cmp (t.insert k |>.min!) k |>.isLE :=
|
||||
DTreeMap.minKey!_insertIfNew_le_self
|
||||
|
||||
theorem contains_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.min! :=
|
||||
DTreeMap.contains_minKey! he
|
||||
|
||||
theorem min!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.min! ∈ t :=
|
||||
DTreeMap.minKey!_mem he
|
||||
|
||||
theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp t.min! k |>.isLE :=
|
||||
DTreeMap.minKey!_le_of_contains hc
|
||||
|
||||
theorem min!_le_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp t.min! k |>.isLE :=
|
||||
DTreeMap.minKey!_le_of_mem hc
|
||||
|
||||
theorem le_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.min!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.le_minKey! he
|
||||
|
||||
theorem get?_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.get? t.min! = some t.min! :=
|
||||
DTreeMap.getKey?_minKey! he
|
||||
|
||||
theorem get_min! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.get t.min! hc = t.min! :=
|
||||
DTreeMap.getKey_minKey!
|
||||
|
||||
@[simp]
|
||||
theorem get_min!_eq_min [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.get t.min! hc = t.min (isEmpty_eq_false_of_contains hc) :=
|
||||
DTreeMap.getKey_minKey!_eq_minKey
|
||||
|
||||
theorem get!_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.get! t.min! = t.min! :=
|
||||
DTreeMap.getKey!_minKey! he
|
||||
|
||||
theorem getD_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getD t.min! fallback = t.min! :=
|
||||
DTreeMap.getKeyD_minKey! he
|
||||
|
||||
theorem min!_erase_eq_of_not_compare_min!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.min! = .eq) :
|
||||
(t.erase k |>.min!) = t.min! :=
|
||||
DTreeMap.minKey!_erase_eq_of_not_compare_minKey!_eq he heq
|
||||
|
||||
theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.min! (t.erase k |>.min!) |>.isLE :=
|
||||
DTreeMap.minKey!_le_minKey!_erase he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeSet
|
||||
|
|
|
|||
|
|
@ -70,6 +70,10 @@ theorem isEmpty_eq_false_iff_exists_mem [TransCmp cmp] (h : t.WF) :
|
|||
t.isEmpty = false ↔ ∃ a, a ∈ t :=
|
||||
DTreeMap.Raw.isEmpty_eq_false_iff_exists_mem h
|
||||
|
||||
theorem isEmpty_eq_false_of_contains [TransCmp cmp] (h : t.WF) {a : α} (hc : t.contains a = true) :
|
||||
t.isEmpty = false :=
|
||||
TreeMap.Raw.isEmpty_eq_false_of_contains h hc
|
||||
|
||||
theorem isEmpty_iff_forall_contains [TransCmp cmp] (h : t.WF) :
|
||||
t.isEmpty = true ↔ ∀ a, t.contains a = false :=
|
||||
DTreeMap.Raw.isEmpty_iff_forall_contains h
|
||||
|
|
@ -149,9 +153,9 @@ theorem isEmpty_erase [TransCmp cmp] (h : t.WF) {k : α} :
|
|||
(t.erase k).isEmpty = (t.isEmpty || (t.size == 1 && t.contains k)) :=
|
||||
TreeMap.Raw.isEmpty_erase h
|
||||
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_containsKey [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
theorem isEmpty_eq_isEmpty_erase_and_not_contains [TransCmp cmp] (h : t.WF) (k : α) :
|
||||
t.isEmpty = ((t.erase k).isEmpty && !(t.contains k)) :=
|
||||
TreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_containsKey h k
|
||||
TreeMap.Raw.isEmpty_eq_isEmpty_erase_and_not_contains h k
|
||||
|
||||
theorem isEmpty_eq_false_of_isEmpty_erase_eq_false [TransCmp cmp] (h : t.WF) {k : α}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
|
|
@ -778,6 +782,84 @@ theorem min?_le_min?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
TreeMap.Raw.minKey?_le_minKey?_erase h
|
||||
|
||||
theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.min? = some t.min! :=
|
||||
DTreeMap.Raw.minKey?_eq_some_minKey! h he
|
||||
|
||||
theorem min!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.min! = default :=
|
||||
DTreeMap.Raw.minKey!_eq_default h he
|
||||
|
||||
theorem min!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.min! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem min!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.min! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem min!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
|
||||
(t.insert k |>.min!) =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew h
|
||||
|
||||
theorem min!_insert_le_min! [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k} :
|
||||
cmp (t.insert k |>.min!) t.min! |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew_le_minKey! h he
|
||||
|
||||
theorem min!_insert_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
|
||||
cmp (t.insert k |>.min!) k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew_le_self h
|
||||
|
||||
theorem contains_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.min! :=
|
||||
DTreeMap.Raw.contains_minKey! h he
|
||||
|
||||
theorem min!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.min! ∈ t :=
|
||||
DTreeMap.Raw.minKey!_mem h he
|
||||
|
||||
theorem min!_le_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp t.min! k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_of_contains h hc
|
||||
|
||||
theorem min!_le_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp t.min! k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_of_mem h hc
|
||||
|
||||
theorem le_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp k t.min!).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.Raw.le_minKey! h he
|
||||
|
||||
theorem get?_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.get? t.min! = some t.min! :=
|
||||
DTreeMap.Raw.getKey?_minKey! h he
|
||||
|
||||
theorem get_min! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.get t.min! hc = t.min! :=
|
||||
DTreeMap.Raw.getKey_minKey! h
|
||||
|
||||
theorem get!_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.get! t.min! = t.min! :=
|
||||
DTreeMap.Raw.getKey!_minKey! h he
|
||||
|
||||
theorem getD_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getD t.min! fallback = t.min! :=
|
||||
DTreeMap.Raw.getKeyD_minKey! h he
|
||||
|
||||
theorem min!_erase_eq_of_not_compare_min!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.min! = .eq) :
|
||||
(t.erase k |>.min!) = t.min! :=
|
||||
DTreeMap.Raw.minKey!_erase_eq_of_not_compare_minKey!_eq h he heq
|
||||
|
||||
theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp t.min! (t.erase k |>.min!) |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_minKey!_erase h he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeSet.Raw
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue