feat: tree map lemmas for maxKey! (#7686)
This PR provides lemmas for the tree map function `maxKey!` 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
5ad6edc8d0
commit
e9fda1a3e4
10 changed files with 1201 additions and 71 deletions
|
|
@ -101,7 +101,8 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
|
|||
⟨`minKey!, (``minKey!_eq_minKey!, #[``(minKey!_of_perm _)])⟩,
|
||||
⟨`minKeyD, (``minKeyD_eq_minKeyD, #[``(minKeyD_of_perm _)])⟩,
|
||||
⟨`maxKey?, (``maxKey?_eq_maxKey?, #[``(maxKey?_of_perm _)])⟩,
|
||||
⟨`maxKey, (``maxKey_eq_maxKey, #[``(maxKey_of_perm _)])⟩]
|
||||
⟨`maxKey, (``maxKey_eq_maxKey, #[``(maxKey_of_perm _)])⟩,
|
||||
⟨`maxKey!, (``maxKey!_eq_maxKey!, #[``(maxKey!_of_perm _)])⟩]
|
||||
|
||||
/-- Internal implementation detail of the tree map -/
|
||||
scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
|
||||
|
|
@ -4692,7 +4693,7 @@ theorem minKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
|||
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.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
|
||||
|
||||
|
|
@ -4703,7 +4704,7 @@ theorem minKey!_insert_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
|||
|
||||
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
|
||||
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} :
|
||||
|
|
@ -4711,7 +4712,7 @@ theorem minKey!_insert_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
|||
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
|
||||
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) :
|
||||
|
|
@ -4767,7 +4768,7 @@ theorem minKey!_erase_eq_iff_not_compare_minKey!_eq [TransOrd α] [Inhabited α]
|
|||
|
||||
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! ↔
|
||||
(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
|
||||
|
||||
|
|
@ -4779,7 +4780,7 @@ theorem minKey!_erase_eq_of_not_compare_minKey!_eq [TransOrd α] [Inhabited α]
|
|||
|
||||
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
|
||||
(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) :
|
||||
|
|
@ -4789,7 +4790,7 @@ theorem minKey!_le_minKey!_erase [TransOrd α] [Inhabited α] (h : t.WF) :
|
|||
|
||||
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
|
||||
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},
|
||||
|
|
@ -4798,7 +4799,7 @@ theorem minKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k v},
|
|||
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.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
|
||||
|
||||
|
|
@ -4809,7 +4810,7 @@ theorem minKey!_insertIfNew_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
|||
|
||||
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
|
||||
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},
|
||||
|
|
@ -4817,7 +4818,7 @@ theorem minKey!_insertIfNew_le_self [TransOrd α] [Inhabited α] (h : t.WF) :
|
|||
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
|
||||
compare (t.insertIfNew! k v).minKey! k |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_le_self h
|
||||
|
||||
theorem minKey!_eq_head!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
|
|
@ -4825,7 +4826,7 @@ theorem minKey!_eq_head!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
|
|||
simp_to_model [minKey!, keys] using List.minKey!_eq_head!_keys h.ordered
|
||||
|
||||
theorem minKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
|
||||
(t.modify k f |>.minKey!) = t.minKey! := by
|
||||
(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) :
|
||||
|
|
@ -4836,7 +4837,7 @@ theorem minKey!_alter_eq_self [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h :
|
|||
|
||||
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 ↔
|
||||
(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
|
||||
|
||||
|
|
@ -5495,6 +5496,217 @@ theorem maxKey_alter_eq_self [TransOrd α] (h : t.WF) {k f he} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem maxKey_eq_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) {he} :
|
||||
t.maxKey he = t.maxKey! := by
|
||||
simp_to_model [maxKey, maxKey!] using List.maxKey_eq_maxKey!
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.maxKey? = some t.maxKey! := by
|
||||
simp_to_model [maxKey?, maxKey!, isEmpty] using List.maxKey?_eq_some_maxKey!
|
||||
|
||||
theorem maxKey!_eq_default [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty) → t.maxKey! = default := by
|
||||
simp_to_model [maxKey!, isEmpty] using List.maxKey!_eq_default
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km},
|
||||
t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (compare k km).isLE := by
|
||||
simp_to_model [maxKey!, getKey?, contains, isEmpty] using
|
||||
List.maxKey!_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [TransOrd α]
|
||||
[LawfulEqOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km},
|
||||
t.maxKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (compare k km).isLE := by
|
||||
simp_to_model [maxKey!, contains, isEmpty] using List.maxKey!_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem maxKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v h.balanced |>.impl.maxKey!) =
|
||||
(t.maxKey?.elim k fun k' => if compare k' k |>.isLE then k else k') := by
|
||||
simp_to_model [maxKey!, maxKey?, insert] using List.maxKey!_insertEntry
|
||||
|
||||
theorem maxKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert! k v).maxKey! =
|
||||
(t.maxKey?.elim k fun k' => if compare k' k |>.isLE then k else k') := by
|
||||
simpa [insert_eq_insert!] using maxKey!_insert h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare t.maxKey! (t.insert k v h.balanced |>.impl.maxKey!) |>.isLE := by
|
||||
simp_to_model [maxKey!, isEmpty, insert] using List.maxKey!_le_maxKey!_insertEntry
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare t.maxKey! (t.insert! k v).maxKey! |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using maxKey!_le_maxKey!_insert h
|
||||
|
||||
theorem self_le_maxKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare k (t.insert k v h.balanced |>.impl.maxKey!) |>.isLE := by
|
||||
simp_to_model [maxKey!, insert] using List.self_le_maxKey!_insertEntry
|
||||
|
||||
theorem self_le_maxKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare k (t.insert! k v).maxKey! |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using self_le_maxKey!_insert h
|
||||
|
||||
theorem contains_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.contains t.maxKey! := by
|
||||
simp_to_model [maxKey!, isEmpty, contains] using List.containsKey_maxKey!
|
||||
|
||||
theorem maxKey!_mem [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.maxKey! ∈ t :=
|
||||
contains_maxKey! h
|
||||
|
||||
theorem le_maxKey!_of_contains [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (hc : t.contains k) →
|
||||
compare k t.maxKey! |>.isLE := by
|
||||
simp_to_model [maxKey!, contains] using List.le_maxKey!_of_containsKey
|
||||
|
||||
theorem le_maxKey!_of_mem [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (hc : k ∈ t) →
|
||||
compare k t.maxKey! |>.isLE :=
|
||||
le_maxKey!_of_contains h
|
||||
|
||||
theorem maxKey!_le [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k},
|
||||
(compare t.maxKey! k).isLE ↔ (∀ k', k' ∈ t → (compare k' k).isLE) := by
|
||||
simp_to_model [maxKey!, contains, isEmpty] using List.maxKey!_le
|
||||
|
||||
theorem getKey?_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) →
|
||||
t.getKey? t.maxKey! = some t.maxKey! := by
|
||||
simp_to_model [maxKey!, getKey?, isEmpty] using List.getKey?_maxKey!
|
||||
|
||||
theorem getKey_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {he},
|
||||
t.getKey t.maxKey! he = t.maxKey! := by
|
||||
simp_to_model [maxKey!, contains, isEmpty, getKey] using List.getKey_maxKey!
|
||||
|
||||
theorem getKey_maxKey!_eq_maxKey [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {hc},
|
||||
t.getKey t.maxKey! hc = t.maxKey (isEmpty_eq_false_of_contains h hc) := by
|
||||
simp_to_model [maxKey!, maxKey, contains, isEmpty, getKey] using List.getKey_maxKey!_eq_maxKey
|
||||
|
||||
theorem getKey!_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → t.getKey! t.maxKey! = t.maxKey! := by
|
||||
simp_to_model [maxKey!, isEmpty, getKey!] using List.getKey!_maxKey!
|
||||
|
||||
theorem getKeyD_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback},
|
||||
t.getKeyD t.maxKey! fallback = t.maxKey! := by
|
||||
simp_to_model [maxKey!, getKeyD, isEmpty] using List.getKeyD_maxKey!
|
||||
|
||||
theorem maxKey!_erase_eq_iff_not_compare_maxKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
(t.erase k h.balanced |>.impl.maxKey!) = t.maxKey! ↔
|
||||
¬ compare k t.maxKey! = .eq := by
|
||||
simp_to_model [maxKey!, isEmpty, erase] using List.maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false
|
||||
|
||||
theorem maxKey!_erase!_eq_iff_not_compare_maxKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) →
|
||||
(t.erase! k).maxKey! = t.maxKey! ↔
|
||||
¬ compare k t.maxKey! = .eq := by
|
||||
simpa only [erase_eq_erase!] using maxKey!_erase_eq_iff_not_compare_maxKey!_eq h
|
||||
|
||||
theorem maxKey!_erase_eq_of_not_compare_maxKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) → (heq : ¬ compare k t.maxKey! = .eq) →
|
||||
(t.erase k h.balanced |>.impl.maxKey!) = t.maxKey! := by
|
||||
simp_to_model [maxKey!, isEmpty, erase] using
|
||||
List.maxKey!_eraseKey_eq_of_beq_maxKey!_eq_false
|
||||
|
||||
theorem maxKey!_erase!_eq_of_not_compare_maxKey!_eq [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) → (heq : ¬ compare k t.maxKey! = .eq) →
|
||||
(t.erase! k).maxKey! = t.maxKey! := by
|
||||
simpa only [erase_eq_erase!] using maxKey!_erase_eq_of_not_compare_maxKey!_eq h
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
compare (t.erase k h.balanced |>.impl.maxKey!) t.maxKey! |>.isLE := by
|
||||
simp_to_model [maxKey!, isEmpty, erase] using List.maxKey!_erase_le_maxKey!
|
||||
|
||||
theorem maxKey!_erase!_le_maxKey! [TransOrd α] [Inhabited α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) →
|
||||
compare (t.erase! k).maxKey! t.maxKey! |>.isLE := by
|
||||
simpa only [erase_eq_erase!] using maxKey!_erase_le_maxKey! h
|
||||
|
||||
theorem maxKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k v},
|
||||
(t.insertIfNew k v h.balanced |>.impl.maxKey!) =
|
||||
t.maxKey?.elim k fun k' => if compare k' k = .lt then k else k' := by
|
||||
simp_to_model [maxKey!, maxKey?, insertIfNew] using List.maxKey!_insertEntryIfNew
|
||||
|
||||
theorem maxKey!_insertIfNew! [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew! k v).maxKey! =
|
||||
t.maxKey?.elim k fun k' => if compare k' k = .lt then k else k' := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using maxKey!_insertIfNew h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare t.maxKey! (t.insertIfNew k v h.balanced |>.impl.maxKey!) |>.isLE := by
|
||||
simp_to_model [maxKey!, isEmpty, insertIfNew] using List.maxKey!_le_maxKey!_insertEntryIfNew
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew! [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v},
|
||||
compare t.maxKey! (t.insertIfNew! k v).maxKey! |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using maxKey!_le_maxKey!_insertIfNew h
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k v},
|
||||
compare k (t.insertIfNew k v h.balanced |>.impl.maxKey!) |>.isLE := by
|
||||
simp_to_model [maxKey!, insertIfNew] using List.self_le_maxKey!_insertEntryIfNew
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew! [TransOrd α] [Inhabited α] (h : t.WF) {k v} :
|
||||
compare k (t.insertIfNew! k v).maxKey! |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using self_le_maxKey!_insertIfNew h
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
t.maxKey! = t.keys.getLast! := by
|
||||
simp_to_model [maxKey!, keys] using List.maxKey!_eq_getLast!_keys h.ordered.distinctKeys h.ordered
|
||||
|
||||
theorem maxKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
|
||||
(t.modify k f).maxKey! = t.maxKey! := by
|
||||
simp_to_model [maxKey!, modify] using List.maxKey!_modifyKey
|
||||
|
||||
theorem maxKey!_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.maxKey!) = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simp_to_model [maxKey!, alter, isEmpty, contains, get?] using List.maxKey!_alterKey_eq_self
|
||||
|
||||
theorem maxKey!_alter!_eq_self [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) {k f} :
|
||||
(he : (t.alter! k f).isEmpty = false) →
|
||||
(t.alter! k f).maxKey! = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simpa only [alter_eq_alter!] using maxKey!_alter_eq_self h
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Impl α β}
|
||||
|
||||
theorem maxKey!_modify [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (he : (modify k f t).isEmpty = false) →
|
||||
(modify k f t |> maxKey!) = if compare t.maxKey! k = .eq then k else t.maxKey! := by
|
||||
simp_to_model [maxKey!, maxKey, isEmpty, Const.modify] using List.Const.maxKey!_modifyKey
|
||||
|
||||
theorem maxKey!_modify_eq_maxKey! [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) :
|
||||
∀ {k f}, (modify k f t |> maxKey!) = t.maxKey! := by
|
||||
simp_to_model [maxKey!, Const.modify] using List.Const.maxKey!_modifyKey_eq_maxKey!
|
||||
|
||||
theorem compare_maxKey!_modify_eq [TransOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
|
||||
compare (Const.modify k f t |> maxKey!) t.maxKey! = .eq := by
|
||||
simp_to_model [maxKey!, Const.modify] using List.Const.maxKey!_modifyKey_beq
|
||||
|
||||
theorem maxKey!_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.maxKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simp_to_model [maxKey!, Const.alter, contains, isEmpty, Const.get?] using
|
||||
List.Const.maxKey!_alterKey_eq_self
|
||||
|
||||
theorem maxKey!_alter!_eq_self [TransOrd α] [Inhabited α] (h : t.WF) {k f} :
|
||||
(he : (alter! k f t).isEmpty = false) →
|
||||
(alter! k f t |>.maxKey!) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simpa only [alter_eq_alter!] using maxKey!_alter_eq_self h
|
||||
|
||||
end Const
|
||||
|
||||
|
||||
|
||||
end Max
|
||||
|
||||
|
|
|
|||
|
|
@ -501,6 +501,10 @@ theorem maxKey_eq_get_maxKey? [Ord α] {l : Impl α β} {he} :
|
|||
l.maxKey he = l.maxKey?.get (by simp [← some_maxKey_eq_maxKey? (he := he)]) := by
|
||||
simp [← some_maxKey_eq_maxKey? (he := he)]
|
||||
|
||||
theorem maxKey!_eq_get!_maxKey? [Ord α] [Inhabited α] {l : Impl α β} :
|
||||
l.maxKey! = l.maxKey?.get! := by
|
||||
induction l using maxKey!.induct <;> simp_all only [maxKey!, maxKey?] <;> 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!,
|
||||
|
|
|
|||
|
|
@ -1860,4 +1860,8 @@ theorem maxKey_eq_maxKey [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Ordere
|
|||
t.maxKey he = List.maxKey t.toListModel (isEmpty_eq_isEmpty ▸ he) := by
|
||||
simp only [List.maxKey_eq_get_maxKey?, maxKey_eq_get_maxKey?, maxKey?_eq_maxKey? hlo]
|
||||
|
||||
theorem maxKey!_eq_maxKey! [Ord α] [TransOrd α] [Inhabited α] {t : Impl α β} (hlo : t.Ordered) :
|
||||
t.maxKey! = List.maxKey! t.toListModel := by
|
||||
simp only [List.maxKey!_eq_get!_maxKey?, maxKey!_eq_get!_maxKey?, maxKey?_eq_maxKey? hlo]
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -3140,6 +3140,10 @@ theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty =
|
|||
t.minKey? = some t.minKey! :=
|
||||
Impl.minKey?_eq_some_minKey! t.wf he
|
||||
|
||||
theorem minKey_eq_minKey! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.minKey he = t.minKey! :=
|
||||
Impl.minKey_eq_minKey! t.wf
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
Impl.minKey!_eq_default t.wf he
|
||||
|
|
@ -3155,16 +3159,16 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh
|
|||
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.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 :=
|
||||
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 :=
|
||||
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) :
|
||||
|
|
@ -3210,25 +3214,25 @@ theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {
|
|||
|
||||
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! :=
|
||||
(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 :=
|
||||
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.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 :=
|
||||
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 :=
|
||||
cmp (t.insertIfNew k v).minKey! k |>.isLE :=
|
||||
Impl.minKey!_insertIfNew_le_self t.wf
|
||||
|
||||
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
|
||||
|
|
@ -3237,12 +3241,12 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
|
|||
|
||||
@[simp]
|
||||
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(t.modify k f |>.minKey!) = t.minKey! :=
|
||||
(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 :=
|
||||
(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
|
||||
|
|
@ -3251,22 +3255,22 @@ 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! :=
|
||||
(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! :=
|
||||
(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 :=
|
||||
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 ↔
|
||||
(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
|
||||
|
||||
|
|
@ -3761,6 +3765,146 @@ theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.maxKey? = some t.maxKey! :=
|
||||
Impl.maxKey?_eq_some_maxKey! t.wf he
|
||||
|
||||
theorem maxKey_eq_maxKey! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.maxKey he = t.maxKey! :=
|
||||
Impl.maxKey_eq_maxKey! t.wf
|
||||
|
||||
theorem maxKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.maxKey! = default :=
|
||||
Impl.maxKey!_eq_default t.wf he
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
Impl.maxKey!_eq_iff_getKey?_eq_self_and_forall t.wf he
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
Impl.maxKey!_eq_some_iff_mem_and_forall t.wf he
|
||||
|
||||
theorem maxKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insert k v).maxKey! =
|
||||
(t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') :=
|
||||
Impl.maxKey!_insert t.wf
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insert k v).maxKey! |>.isLE :=
|
||||
Impl.maxKey!_le_maxKey!_insert t.wf he
|
||||
|
||||
theorem self_le_maxKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp k (t.insert k v).maxKey! |>.isLE :=
|
||||
Impl.self_le_maxKey!_insert t.wf
|
||||
|
||||
theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.maxKey! :=
|
||||
Impl.contains_maxKey! t.wf he
|
||||
|
||||
theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.maxKey! ∈ t :=
|
||||
Impl.maxKey!_mem t.wf he
|
||||
|
||||
theorem le_maxKey!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
Impl.le_maxKey!_of_contains t.wf hc
|
||||
|
||||
theorem le_maxKey!_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
Impl.le_maxKey!_of_mem t.wf hc
|
||||
|
||||
theorem maxKey!_le [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp t.maxKey! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
Impl.maxKey!_le t.wf he
|
||||
|
||||
theorem getKey?_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey? t.maxKey! = some t.maxKey! :=
|
||||
Impl.getKey?_maxKey! t.wf he
|
||||
|
||||
theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey! :=
|
||||
Impl.getKey_maxKey! t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKey_maxKey!_eq_maxKey [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey (isEmpty_eq_false_of_contains hc) :=
|
||||
Impl.getKey_maxKey!_eq_maxKey t.wf
|
||||
|
||||
theorem getKey!_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey! t.maxKey! = t.maxKey! :=
|
||||
Impl.getKey!_maxKey! t.wf he
|
||||
|
||||
theorem getKeyD_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.maxKey! fallback = t.maxKey! :=
|
||||
Impl.getKeyD_maxKey! t.wf he
|
||||
|
||||
theorem maxKey!_erase_eq_of_not_compare_maxKey!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.maxKey! = .eq) :
|
||||
(t.erase k).maxKey! = t.maxKey! :=
|
||||
Impl.maxKey!_erase_eq_of_not_compare_maxKey!_eq t.wf he heq
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k).maxKey! t.maxKey! |>.isLE :=
|
||||
Impl.maxKey!_erase_le_maxKey! t.wf he
|
||||
|
||||
theorem maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insertIfNew k v).maxKey! =
|
||||
t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
Impl.maxKey!_insertIfNew t.wf
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
Impl.maxKey!_le_maxKey!_insertIfNew t.wf he
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp k (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
Impl.self_le_maxKey!_insertIfNew t.wf
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] :
|
||||
t.maxKey! = t.keys.getLast! :=
|
||||
Impl.maxKey!_eq_getLast!_keys t.wf
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(t.modify k f).maxKey! = t.maxKey! :=
|
||||
Impl.maxKey!_modify t.wf
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f}
|
||||
(he : (t.alter k f).isEmpty = false) :
|
||||
(t.alter k f).maxKey! = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.maxKey!_alter_eq_self t.wf he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : DTreeMap α β cmp}
|
||||
|
||||
theorem maxKey!_modify [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
|
||||
Impl.Const.maxKey!_modify t.wf he
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(modify t k f).maxKey! = t.maxKey! :=
|
||||
Impl.Const.maxKey!_modify_eq_maxKey! t.wf
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
|
||||
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
|
||||
Impl.Const.compare_maxKey!_modify_eq t.wf (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f).maxKey! = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.Const.maxKey!_alter_eq_self t.wf he
|
||||
|
||||
end Const
|
||||
|
||||
end Max
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -3015,17 +3015,17 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh
|
|||
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.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 :=
|
||||
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 :=
|
||||
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) :
|
||||
|
|
@ -3066,26 +3066,26 @@ theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty
|
|||
|
||||
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! :=
|
||||
(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 :=
|
||||
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.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 :=
|
||||
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 :=
|
||||
cmp (t.insertIfNew k v).minKey! k |>.isLE :=
|
||||
Impl.minKey!_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
|
|
@ -3094,12 +3094,12 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
|||
|
||||
@[simp]
|
||||
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(t.modify k f |>.minKey!) = t.minKey! :=
|
||||
(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 :=
|
||||
(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
|
||||
|
|
@ -3108,22 +3108,22 @@ 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! :=
|
||||
(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! :=
|
||||
(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 :=
|
||||
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 ↔
|
||||
(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
|
||||
|
||||
|
|
@ -3472,6 +3472,139 @@ theorem maxKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.maxKey? = some t.maxKey! :=
|
||||
Impl.maxKey?_eq_some_maxKey! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem maxKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.maxKey! = default :=
|
||||
Impl.maxKey!_eq_default h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
Impl.maxKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
Impl.maxKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v).maxKey! =
|
||||
(t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') :=
|
||||
Impl.maxKey!_insert! h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v} :
|
||||
cmp t.maxKey! (t.insert k v).maxKey! |>.isLE :=
|
||||
Impl.maxKey!_le_maxKey!_insert! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem self_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp k (t.insert k v).maxKey! |>.isLE :=
|
||||
Impl.self_le_maxKey!_insert! h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.maxKey! :=
|
||||
Impl.contains_maxKey! h he
|
||||
|
||||
theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.maxKey! ∈ t :=
|
||||
Impl.maxKey!_mem h he
|
||||
|
||||
theorem le_maxKey!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
Impl.le_maxKey!_of_contains h hc
|
||||
|
||||
theorem le_maxKey!_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
Impl.le_maxKey!_of_mem h hc
|
||||
|
||||
theorem maxKey!_le [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp t.maxKey! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
Impl.maxKey!_le h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem getKey?_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey? t.maxKey! = some t.maxKey! :=
|
||||
Impl.getKey?_maxKey! h he
|
||||
|
||||
theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey! :=
|
||||
Impl.getKey_maxKey! h
|
||||
|
||||
theorem getKey!_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey! t.maxKey! = t.maxKey! :=
|
||||
Impl.getKey!_maxKey! h he
|
||||
|
||||
theorem getKeyD_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.maxKey! fallback = t.maxKey! :=
|
||||
Impl.getKeyD_maxKey! h he
|
||||
|
||||
theorem maxKey!_erase_eq_of_not_compare_maxKey!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.maxKey! = .eq) :
|
||||
(t.erase k).maxKey! = t.maxKey! :=
|
||||
Impl.maxKey!_erase!_eq_of_not_compare_maxKey!_eq h he heq
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k).maxKey! t.maxKey! |>.isLE :=
|
||||
Impl.maxKey!_erase!_le_maxKey! h he
|
||||
|
||||
theorem maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).maxKey! =
|
||||
t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
Impl.maxKey!_insertIfNew! h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
Impl.maxKey!_le_maxKey!_insertIfNew! h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp k (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
Impl.self_le_maxKey!_insertIfNew! h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.maxKey! = t.keys.getLast! :=
|
||||
Impl.maxKey!_eq_getLast!_keys h (instOrd := ⟨cmp⟩)
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(t.modify k f).maxKey! = t.maxKey! :=
|
||||
Impl.maxKey!_modify h
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (t.alter k f).isEmpty = false) :
|
||||
(t.alter k f).maxKey! = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.maxKey!_alter!_eq_self h he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Raw α β cmp}
|
||||
|
||||
theorem maxKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
|
||||
Impl.Const.maxKey!_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(modify t k f).maxKey! = t.maxKey! :=
|
||||
Impl.Const.maxKey!_modify_eq_maxKey! h
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
|
||||
Impl.Const.compare_maxKey!_modify_eq h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f).maxKey! = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.Const.maxKey!_alter!_eq_self h he
|
||||
|
||||
end Const
|
||||
|
||||
end Max
|
||||
|
||||
end Std.DTreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -5840,6 +5840,218 @@ theorem maxKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α
|
|||
|
||||
end Const
|
||||
|
||||
/-- Given a proof that the list is nonempty, returns the smallest key in an associative list. -/
|
||||
def maxKey! [Ord α] [Inhabited α] (xs : List ((a : α) × β a)) : α :=
|
||||
maxKey? xs |>.get!
|
||||
|
||||
theorem maxKey!_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l l' : List ((a : α) × β a)} (hd : DistinctKeys l) (hp : l.Perm l') :
|
||||
maxKey! l = maxKey! l' :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_of_perm hd hp
|
||||
|
||||
theorem maxKey!_eq_get!_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} :
|
||||
maxKey! l = (maxKey? l).get! :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eq_get!_minKey?
|
||||
|
||||
theorem maxKey_eq_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} {he} :
|
||||
maxKey l he = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_eq_minKey!
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (he : l.isEmpty = false) :
|
||||
maxKey? l = some (maxKey! l) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey?_eq_some_minKey! he
|
||||
|
||||
theorem maxKey!_eq_default [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (h : l.isEmpty) :
|
||||
maxKey! l = default :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eq_default h
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km} :
|
||||
maxKey! l = km ↔ getKey? km l = some km ∧ ∀ k, containsKey k l → (compare k km).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eq_iff_getKey?_eq_self_and_forall hd he
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[LawfulEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(he : l.isEmpty = false) {km} :
|
||||
maxKey! l = km ↔ containsKey km l ∧ ∀ k, containsKey k l → (compare k km).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eq_some_iff_mem_and_forall hd he
|
||||
|
||||
theorem maxKey!_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
(insertEntry k v l |> maxKey!) =
|
||||
((maxKey? l).elim k fun k' => if compare k' k |>.isLE then k else k') :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntry hd
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v} :
|
||||
compare (maxKey! l) (insertEntry k v l |> maxKey!) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntry_le_minKey! hd he
|
||||
|
||||
theorem self_le_maxKey!_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare k (insertEntry k v l |> maxKey!) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntry_le_self hd
|
||||
|
||||
theorem containsKey_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
containsKey (maxKey! l) l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
containsKey_minKey! hd he
|
||||
|
||||
theorem le_maxKey!_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (hc : containsKey k l) :
|
||||
compare k (maxKey! l) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_le_of_containsKey hd hc
|
||||
|
||||
theorem maxKey!_le [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k} :
|
||||
(compare (maxKey! l) k).isLE ↔ (∀ k', containsKey k' l → (compare k' k).isLE) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
le_minKey! hd he
|
||||
|
||||
theorem getKey?_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
getKey? (maxKey! l) l = some (maxKey! l) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey?_minKey! hd he
|
||||
|
||||
theorem getKey_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey (maxKey! l) l he = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey_minKey! hd
|
||||
|
||||
theorem getKey_maxKey!_eq_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey (maxKey! l) l he = maxKey l (isEmpty_eq_false_of_containsKey he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey_minKey!_eq_minKey hd
|
||||
|
||||
theorem getKey!_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) :
|
||||
getKey! (maxKey! l) l = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey!_minKey! hd he
|
||||
|
||||
theorem getKeyD_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback} :
|
||||
getKeyD (maxKey! l) l fallback = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKeyD_minKey! hd he
|
||||
|
||||
theorem maxKey!_eraseKey_eq_iff_beq_maxKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> maxKey!) = maxKey! l ↔ (k == (maxKey! l)) = false :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eraseKey_eq_iff_beq_minKey_eq_false hd he
|
||||
|
||||
theorem maxKey!_eraseKey_eq_iff_beq_maxKey!_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> maxKey!) = maxKey! l ↔ (k == (maxKey! l)) = false :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eraseKey_eq_iff_beq_minKey!_eq_false hd he
|
||||
|
||||
theorem maxKey!_eraseKey_eq_of_beq_maxKey!_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k}
|
||||
(he : (eraseKey k l).isEmpty = false) : (heq : (k == maxKey! l) = false) →
|
||||
(eraseKey k l |> maxKey!) = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_eraseKey_eq_of_beq_minKey!_eq_false hd he
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (he : (eraseKey k l).isEmpty = false) :
|
||||
compare (eraseKey k l |> maxKey!) (maxKey! l) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_le_minKey!_erase hd he
|
||||
|
||||
theorem maxKey!_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
(insertEntryIfNew k v l |> maxKey!) =
|
||||
(maxKey? l).elim k fun k' => if compare k' k = .lt then k else k' :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntryIfNew hd
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v} :
|
||||
compare (maxKey! l) (insertEntryIfNew k v l |> maxKey!) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntryIfNew_le_minKey! hd he
|
||||
|
||||
theorem self_le_maxKey!_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare k (insertEntryIfNew k v l |> maxKey!) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_insertEntryIfNew_le_self hd
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) :
|
||||
maxKey! l = (keys l).getLast! := by
|
||||
simp only [List.getLast!_eq_getLast?_getD, maxKey!_eq_get!_maxKey?,
|
||||
Option.get!_eq_getD, maxKey?_eq_getLast?_keys hd ho]
|
||||
|
||||
theorem maxKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> maxKey!) = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_modifyKey hd
|
||||
|
||||
theorem maxKey!_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 |> maxKey!) = k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_alterKey_eq_self hd he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
theorem maxKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (modifyKey k f l).isEmpty = false) :
|
||||
(modifyKey k f l |> maxKey!) = if (maxKey! l) == k then k else (maxKey! l) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_modifyKey hd he
|
||||
|
||||
theorem maxKey!_modifyKey_eq_maxKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
[Inhabited α] {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> maxKey!) = maxKey! l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_modifyKey_eq_minKey! hd
|
||||
|
||||
theorem maxKey!_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} :
|
||||
(modifyKey k f l |> maxKey!) == (maxKey! l) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_modifyKey_beq hd
|
||||
|
||||
theorem maxKey!_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 |> maxKey!) = k ↔
|
||||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey!_alterKey_eq_self hd he
|
||||
|
||||
end Const
|
||||
|
||||
end Max
|
||||
|
||||
end Std.Internal.List
|
||||
|
|
|
|||
|
|
@ -2073,6 +2073,10 @@ theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty =
|
|||
t.minKey? = some t.minKey! :=
|
||||
DTreeMap.minKey?_eq_some_minKey! he
|
||||
|
||||
theorem minKey_eq_minKey! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.minKey he = t.minKey! :=
|
||||
DTreeMap.minKey_eq_minKey!
|
||||
|
||||
theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.minKey! = default :=
|
||||
DTreeMap.minKey!_eq_default he
|
||||
|
|
@ -2088,16 +2092,16 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh
|
|||
DTreeMap.minKey!_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem minKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insert k v |>.minKey!) =
|
||||
(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 :=
|
||||
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 :=
|
||||
cmp (t.insert k v).minKey! k |>.isLE :=
|
||||
DTreeMap.minKey!_insert_le_self
|
||||
|
||||
theorem contains_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
|
|
@ -2143,25 +2147,25 @@ theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {
|
|||
|
||||
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! :=
|
||||
(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 :=
|
||||
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.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 :=
|
||||
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 :=
|
||||
cmp (t.insertIfNew k v).minKey! k |>.isLE :=
|
||||
DTreeMap.minKey!_insertIfNew_le_self
|
||||
|
||||
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
|
||||
|
|
@ -2170,22 +2174,22 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
|
|||
|
||||
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! :=
|
||||
(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! :=
|
||||
(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 :=
|
||||
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 ↔
|
||||
(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
|
||||
|
||||
|
|
@ -2624,6 +2628,129 @@ theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
|
|||
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
DTreeMap.Const.maxKey_alter_eq_self
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.maxKey? = some t.maxKey! :=
|
||||
DTreeMap.maxKey?_eq_some_maxKey! he
|
||||
|
||||
theorem maxKey_eq_maxKey! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.maxKey he = t.maxKey! :=
|
||||
DTreeMap.maxKey_eq_maxKey!
|
||||
|
||||
theorem maxKey!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.maxKey! = default :=
|
||||
DTreeMap.maxKey!_eq_default he
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.maxKey!_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem maxKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insert k v).maxKey! =
|
||||
(t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') :=
|
||||
DTreeMap.maxKey!_insert
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insert k v).maxKey! |>.isLE :=
|
||||
DTreeMap.maxKey!_le_maxKey!_insert he
|
||||
|
||||
theorem self_le_maxKey!_insert [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp k (t.insert k v).maxKey! |>.isLE :=
|
||||
DTreeMap.self_le_maxKey!_insert
|
||||
|
||||
theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.maxKey! :=
|
||||
DTreeMap.contains_maxKey! he
|
||||
|
||||
theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.maxKey! ∈ t :=
|
||||
DTreeMap.maxKey!_mem he
|
||||
|
||||
theorem le_maxKey!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
DTreeMap.le_maxKey!_of_contains hc
|
||||
|
||||
theorem le_maxKey!_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
DTreeMap.le_maxKey!_of_mem hc
|
||||
|
||||
theorem maxKey!_le [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp t.maxKey! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
DTreeMap.maxKey!_le he
|
||||
|
||||
theorem getKey?_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey? t.maxKey! = some t.maxKey! :=
|
||||
DTreeMap.getKey?_maxKey! he
|
||||
|
||||
theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey! :=
|
||||
DTreeMap.getKey_maxKey!
|
||||
|
||||
@[simp]
|
||||
theorem getKey_maxKey!_eq_maxKey [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey (isEmpty_eq_false_of_contains hc) :=
|
||||
DTreeMap.getKey_maxKey!_eq_maxKey
|
||||
|
||||
theorem getKey!_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.getKey! t.maxKey! = t.maxKey! :=
|
||||
DTreeMap.getKey!_maxKey! he
|
||||
|
||||
theorem getKeyD_maxKey! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.maxKey! fallback = t.maxKey! :=
|
||||
DTreeMap.getKeyD_maxKey! he
|
||||
|
||||
theorem maxKey!_erase_eq_of_not_compare_maxKey!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.maxKey! = .eq) :
|
||||
(t.erase k).maxKey! = t.maxKey! :=
|
||||
DTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq he heq
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k).maxKey! t.maxKey! |>.isLE :=
|
||||
DTreeMap.maxKey!_erase_le_maxKey! he
|
||||
|
||||
theorem maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k v} :
|
||||
(t.insertIfNew k v).maxKey! =
|
||||
t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
DTreeMap.maxKey!_insertIfNew
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
DTreeMap.maxKey!_le_maxKey!_insertIfNew he
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] {k v} :
|
||||
cmp k (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
DTreeMap.self_le_maxKey!_insertIfNew
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] :
|
||||
t.maxKey! = t.keys.getLast! :=
|
||||
DTreeMap.maxKey!_eq_getLast!_keys
|
||||
|
||||
theorem maxKey!_modify [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
|
||||
DTreeMap.Const.maxKey!_modify he
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
|
||||
(modify t k f).maxKey! = t.maxKey! :=
|
||||
DTreeMap.Const.maxKey!_modify_eq_maxKey!
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] {k f} :
|
||||
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
|
||||
DTreeMap.Const.compare_maxKey!_modify_eq
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f).maxKey! = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
DTreeMap.Const.maxKey!_alter_eq_self he
|
||||
|
||||
end Max
|
||||
|
||||
|
|
|
|||
|
|
@ -1968,17 +1968,17 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh
|
|||
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.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 :=
|
||||
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 :=
|
||||
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) :
|
||||
|
|
@ -2019,26 +2019,26 @@ theorem getKeyD_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty
|
|||
|
||||
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! :=
|
||||
(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 :=
|
||||
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.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 :=
|
||||
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 :=
|
||||
cmp (t.insertIfNew k v).minKey! k |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_insertIfNew_le_self h
|
||||
|
||||
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
|
|
@ -2047,22 +2047,22 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
|||
|
||||
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! :=
|
||||
(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! :=
|
||||
(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 :=
|
||||
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 ↔
|
||||
(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
|
||||
|
||||
|
|
@ -2372,6 +2372,123 @@ theorem maxKey?_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.maxKey?_alter_eq_self h
|
||||
|
||||
theorem maxKey?_eq_some_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.maxKey? = some t.maxKey! :=
|
||||
DTreeMap.Raw.maxKey?_eq_some_maxKey! h he
|
||||
|
||||
theorem maxKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.maxKey! = default :=
|
||||
DTreeMap.Raw.maxKey!_eq_default h he
|
||||
|
||||
theorem maxKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.Raw.maxKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem maxKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.maxKey! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.Raw.maxKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insert k v).maxKey! =
|
||||
(t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') :=
|
||||
DTreeMap.Raw.maxKey!_insert h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v} :
|
||||
cmp t.maxKey! (t.insert k v).maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.maxKey!_le_maxKey!_insert h he
|
||||
|
||||
theorem self_le_maxKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp k (t.insert k v).maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.self_le_maxKey!_insert h
|
||||
|
||||
theorem contains_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.maxKey! :=
|
||||
DTreeMap.Raw.contains_maxKey! h he
|
||||
|
||||
theorem maxKey!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.maxKey! ∈ t :=
|
||||
DTreeMap.Raw.maxKey!_mem h he
|
||||
|
||||
theorem le_maxKey!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.le_maxKey!_of_contains h hc
|
||||
|
||||
theorem le_maxKey!_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp k t.maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.le_maxKey!_of_mem h hc
|
||||
|
||||
theorem maxKey!_le [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp t.maxKey! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
DTreeMap.Raw.maxKey!_le h he
|
||||
|
||||
theorem getKey?_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey? t.maxKey! = some t.maxKey! :=
|
||||
DTreeMap.Raw.getKey?_maxKey! h he
|
||||
|
||||
theorem getKey_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.getKey t.maxKey! hc = t.maxKey! :=
|
||||
DTreeMap.Raw.getKey_maxKey! h
|
||||
|
||||
theorem getKey!_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.getKey! t.maxKey! = t.maxKey! :=
|
||||
DTreeMap.Raw.getKey!_maxKey! h he
|
||||
|
||||
theorem getKeyD_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKeyD t.maxKey! fallback = t.maxKey! :=
|
||||
DTreeMap.Raw.getKeyD_maxKey! h he
|
||||
|
||||
theorem maxKey!_erase_eq_of_not_compare_maxKey!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.maxKey! = .eq) :
|
||||
(t.erase k).maxKey! = t.maxKey! :=
|
||||
DTreeMap.Raw.maxKey!_erase_eq_of_not_compare_maxKey!_eq h he heq
|
||||
|
||||
theorem maxKey!_erase_le_maxKey! [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k).maxKey! t.maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.maxKey!_erase_le_maxKey! h he
|
||||
|
||||
theorem maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v).maxKey! =
|
||||
t.maxKey?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
DTreeMap.Raw.maxKey!_insertIfNew h
|
||||
|
||||
theorem maxKey!_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v} :
|
||||
cmp t.maxKey! (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.maxKey!_le_maxKey!_insertIfNew h he
|
||||
|
||||
theorem self_le_maxKey!_insertIfNew [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} :
|
||||
cmp k (t.insertIfNew k v).maxKey! |>.isLE :=
|
||||
DTreeMap.Raw.self_le_maxKey!_insertIfNew h
|
||||
|
||||
theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.maxKey! = t.keys.getLast! :=
|
||||
DTreeMap.Raw.maxKey!_eq_getLast!_keys h
|
||||
|
||||
theorem maxKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) :
|
||||
(modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! :=
|
||||
DTreeMap.Raw.Const.maxKey!_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem maxKey!_modify_eq_maxKey! [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
(modify t k f).maxKey! = t.maxKey! :=
|
||||
DTreeMap.Raw.Const.maxKey!_modify_eq_maxKey! h
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey!_modify_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} :
|
||||
cmp (modify t k f).maxKey! t.maxKey! = .eq :=
|
||||
DTreeMap.Raw.Const.compare_maxKey!_modify_eq h
|
||||
|
||||
theorem maxKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) :
|
||||
(alter t k f).maxKey! = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
DTreeMap.Raw.Const.maxKey!_alter_eq_self h he
|
||||
|
||||
end Max
|
||||
|
||||
end Std.TreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -800,6 +800,10 @@ theorem min?_le_min?_erase [TransCmp cmp] {k km kme} :
|
|||
cmp km kme |>.isLE :=
|
||||
TreeMap.minKey?_le_minKey?_erase
|
||||
|
||||
theorem min?_eq_head?_toList [TransCmp cmp] :
|
||||
t.min? = t.toList.head? :=
|
||||
TreeMap.minKey?_eq_head?_keys
|
||||
|
||||
theorem min_eq_get_min? [TransCmp cmp] {he} :
|
||||
t.min he = t.min?.get (isSome_min?_iff_isEmpty_eq_false.mpr he) :=
|
||||
TreeMap.minKey_eq_get_minKey?
|
||||
|
|
@ -888,14 +892,18 @@ theorem min_le_min_erase [TransCmp cmp] {k he} :
|
|||
(t.erase k |>.min he) |>.isLE :=
|
||||
DTreeMap.minKey_le_minKey_erase
|
||||
|
||||
theorem min?_eq_head?_toList [TransCmp cmp] :
|
||||
t.min? = t.toList.head? :=
|
||||
TreeMap.minKey?_eq_head?_keys
|
||||
theorem min_eq_head_toList [TransCmp cmp] {he} :
|
||||
t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
|
||||
DTreeMap.minKey_eq_head_keys
|
||||
|
||||
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_min! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.min he = t.min! :=
|
||||
DTreeMap.minKey_eq_minKey!
|
||||
|
||||
theorem min!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.min! = default :=
|
||||
DTreeMap.minKey!_eq_default he
|
||||
|
|
@ -1060,10 +1068,6 @@ theorem minD_le_minD_erase [TransCmp cmp] {k}
|
|||
cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
|
||||
TreeMap.minKeyD_le_minKeyD_erase he
|
||||
|
||||
theorem min_eq_head_toList [TransCmp cmp] {he} :
|
||||
t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
|
||||
DTreeMap.minKey_eq_head_keys
|
||||
|
||||
theorem minD_eq_headD_toList [TransCmp cmp] {fallback} :
|
||||
t.minD fallback = t.toList.headD fallback :=
|
||||
TreeMap.minKeyD_eq_headD_keys
|
||||
|
|
@ -1294,6 +1298,97 @@ theorem max_eq_getLast_toList [TransCmp cmp] {he} :
|
|||
t.max he = t.toList.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
|
||||
TreeMap.maxKey_eq_getLast_keys
|
||||
|
||||
theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.max? = some t.max! :=
|
||||
DTreeMap.maxKey?_eq_some_maxKey! he
|
||||
|
||||
theorem max_eq_max! [TransCmp cmp] [Inhabited α] {he : t.isEmpty = false} :
|
||||
t.max he = t.max! :=
|
||||
DTreeMap.maxKey_eq_maxKey!
|
||||
|
||||
theorem max!_eq_default [TransCmp cmp] [Inhabited α] (he : t.isEmpty) :
|
||||
t.max! = default :=
|
||||
DTreeMap.maxKey!_eq_default he
|
||||
|
||||
theorem max!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.max! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.maxKey!_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem max!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α]
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.max! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.maxKey!_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem max!_insert [TransCmp cmp] [Inhabited α] {k} :
|
||||
(t.insert k |>.max!) =
|
||||
t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
DTreeMap.maxKey!_insertIfNew
|
||||
|
||||
theorem max!_le_max!_insert [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
cmp t.max! (t.insert k |>.max!) |>.isLE :=
|
||||
DTreeMap.maxKey!_le_maxKey!_insertIfNew he
|
||||
|
||||
theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] {k} :
|
||||
cmp k (t.insert k |>.max!) |>.isLE :=
|
||||
DTreeMap.self_le_maxKey!_insertIfNew
|
||||
|
||||
theorem contains_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.contains t.max! :=
|
||||
DTreeMap.contains_maxKey! he
|
||||
|
||||
theorem max!_mem [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.max! ∈ t :=
|
||||
DTreeMap.maxKey!_mem he
|
||||
|
||||
theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] {k} (hc : t.contains k) :
|
||||
cmp k t.max! |>.isLE :=
|
||||
DTreeMap.le_maxKey!_of_contains hc
|
||||
|
||||
theorem le_max!_of_mem [TransCmp cmp] [Inhabited α] {k} (hc : k ∈ t) :
|
||||
cmp k t.max! |>.isLE :=
|
||||
DTreeMap.le_maxKey!_of_mem hc
|
||||
|
||||
theorem max!_le [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {k} :
|
||||
(cmp t.max! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
DTreeMap.maxKey!_le he
|
||||
|
||||
theorem get?_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.get? t.max! = some t.max! :=
|
||||
DTreeMap.getKey?_maxKey! he
|
||||
|
||||
theorem get_max! [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.get t.max! hc = t.max! :=
|
||||
DTreeMap.getKey_maxKey!
|
||||
|
||||
@[simp]
|
||||
theorem get_max!_eq_max [TransCmp cmp] [Inhabited α] {hc} :
|
||||
t.get t.max! hc = t.max (isEmpty_eq_false_of_contains hc) :=
|
||||
DTreeMap.getKey_maxKey!_eq_maxKey
|
||||
|
||||
theorem get!_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
|
||||
t.get! t.max! = t.max! :=
|
||||
DTreeMap.getKey!_maxKey! he
|
||||
|
||||
theorem getD_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getD t.max! fallback = t.max! :=
|
||||
DTreeMap.getKeyD_maxKey! he
|
||||
|
||||
theorem max!_erase_eq_of_not_compare_max!_eq [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.max! = .eq) :
|
||||
(t.erase k |>.max!) = t.max! :=
|
||||
DTreeMap.maxKey!_erase_eq_of_not_compare_maxKey!_eq he heq
|
||||
|
||||
theorem max!_erase_le_max! [TransCmp cmp] [Inhabited α] {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k |>.max!) t.max! |>.isLE :=
|
||||
DTreeMap.maxKey!_erase_le_maxKey! he
|
||||
|
||||
theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] :
|
||||
t.max! = t.toList.getLast! :=
|
||||
TreeMap.maxKey!_eq_getLast!_keys
|
||||
|
||||
|
||||
end Max
|
||||
|
||||
end Std.TreeSet
|
||||
|
|
|
|||
|
|
@ -1104,6 +1104,88 @@ theorem max?_eq_head?_toList [TransCmp cmp] (h : t.WF) :
|
|||
t.max? = t.toList.getLast? :=
|
||||
TreeMap.Raw.maxKey?_eq_getLast?_keys h
|
||||
|
||||
theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.max? = some t.max! :=
|
||||
DTreeMap.Raw.maxKey?_eq_some_maxKey! h he
|
||||
|
||||
theorem max!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) :
|
||||
t.max! = default :=
|
||||
DTreeMap.Raw.maxKey!_eq_default h he
|
||||
|
||||
theorem max!_eq_iff_get?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.max! = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.Raw.maxKey!_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem max!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km} :
|
||||
t.max! = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp k km).isLE :=
|
||||
DTreeMap.Raw.maxKey!_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem max!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
|
||||
(t.insert k |>.max!) =
|
||||
t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
DTreeMap.Raw.maxKey!_insertIfNew h
|
||||
|
||||
theorem max!_le_max!_insert [TransCmp cmp] [Inhabited α] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k} :
|
||||
cmp t.max! (t.insert k |>.max!) |>.isLE :=
|
||||
DTreeMap.Raw.maxKey!_le_maxKey!_insertIfNew h he
|
||||
|
||||
theorem self_le_max!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k} :
|
||||
cmp k (t.insert k |>.max!) |>.isLE :=
|
||||
DTreeMap.Raw.self_le_maxKey!_insertIfNew h
|
||||
|
||||
theorem contains_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.contains t.max! :=
|
||||
DTreeMap.Raw.contains_maxKey! h he
|
||||
|
||||
theorem max!_mem [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.max! ∈ t :=
|
||||
DTreeMap.Raw.maxKey!_mem h he
|
||||
|
||||
theorem le_max!_of_contains [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : t.contains k) :
|
||||
cmp k t.max! |>.isLE :=
|
||||
DTreeMap.Raw.le_maxKey!_of_contains h hc
|
||||
|
||||
theorem le_max!_of_mem [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
cmp k t.max! |>.isLE :=
|
||||
DTreeMap.Raw.le_maxKey!_of_mem h hc
|
||||
|
||||
theorem max!_le [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {k} :
|
||||
(cmp t.max! k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
DTreeMap.Raw.maxKey!_le h he
|
||||
|
||||
theorem get?_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.get? t.max! = some t.max! :=
|
||||
DTreeMap.Raw.getKey?_maxKey! h he
|
||||
|
||||
theorem get_max! [TransCmp cmp] [Inhabited α] (h : t.WF) {hc} :
|
||||
t.get t.max! hc = t.max! :=
|
||||
DTreeMap.Raw.getKey_maxKey! h
|
||||
|
||||
theorem get!_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
|
||||
t.get! t.max! = t.max! :=
|
||||
DTreeMap.Raw.getKey!_maxKey! h he
|
||||
|
||||
theorem getD_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getD t.max! fallback = t.max! :=
|
||||
DTreeMap.Raw.getKeyD_maxKey! h he
|
||||
|
||||
theorem max!_erase_eq_of_not_compare_max!_eq [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k t.max! = .eq) :
|
||||
(t.erase k |>.max!) = t.max! :=
|
||||
DTreeMap.Raw.maxKey!_erase_eq_of_not_compare_maxKey!_eq h he heq
|
||||
|
||||
theorem max!_erase_le_max! [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) :
|
||||
cmp (t.erase k |>.max!) t.max! |>.isLE :=
|
||||
DTreeMap.Raw.maxKey!_erase_le_maxKey! h he
|
||||
|
||||
theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.max! = t.toList.getLast! :=
|
||||
TreeMap.Raw.maxKey!_eq_getLast!_keys h
|
||||
|
||||
end Max
|
||||
|
||||
end Std.TreeSet.Raw
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue