fix: fix maxKey/maxEntry tree map functions and add lemmas for maxKey (#7664)
This PR fixes a bug in the definition of the tree map functions `maxKey` and `maxEntry`. Moreover, it provides lemmas for this function and its interactions with other function for which lemmas already exist. --------- Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert
GitHub
parent
0d1d8b6944
commit
b2da85971d
8 changed files with 724 additions and 11 deletions
|
|
@ -100,7 +100,8 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
|
|||
⟨`minKey, (``minKey_eq_minKey, #[``(minKey_of_perm _)])⟩,
|
||||
⟨`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 _)])⟩]
|
||||
|
||||
/-- Internal implementation detail of the tree map -/
|
||||
scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
|
||||
|
|
@ -5361,6 +5362,140 @@ theorem maxKey?_alter!_eq_self [TransOrd α] (h : t.WF) {k f} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem maxKey?_eq_some_maxKey [TransOrd α] (h : t.WF) {he} :
|
||||
t.maxKey? = some (t.maxKey he) := by
|
||||
simp_to_model [maxKey, maxKey?] using List.maxKey?_eq_some_maxKey
|
||||
|
||||
theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) {he km} :
|
||||
t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE := by
|
||||
simp_to_model [maxKey, getKey?, contains] using List.maxKey_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem maxKey_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.WF) {he km} :
|
||||
t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE := by
|
||||
simp_to_model [maxKey, contains] using List.maxKey_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem maxKey_insert [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insert k v h.balanced).impl.maxKey (isEmpty_insert h) =
|
||||
t.maxKey?.elim k fun k' => if compare k' k |>.isLE then k else k' := by
|
||||
simp_to_model [insert, maxKey, maxKey?] using List.maxKey_insertEntry
|
||||
|
||||
theorem maxKey_le_maxKey_insert [TransOrd α] (h : t.WF) {k v he} :
|
||||
compare (t.maxKey he) (t.insert k v h.balanced |>.impl.maxKey <| isEmpty_insert h) |>.isLE := by
|
||||
simp_to_model [maxKey, insert] using List.maxKey_le_maxKey_insertEntry
|
||||
|
||||
theorem self_le_maxKey_insert [TransOrd α] (h : t.WF) {k v} :
|
||||
compare k (t.insert k v h.balanced |>.impl.maxKey <| isEmpty_insert h) |>.isLE := by
|
||||
simp_to_model [maxKey, insert] using List.self_le_maxKey_insertEntry
|
||||
|
||||
theorem contains_maxKey [TransOrd α] (h : t.WF) {he} :
|
||||
t.contains (t.maxKey he) := by
|
||||
simp_to_model [maxKey, contains] using List.containsKey_maxKey
|
||||
|
||||
theorem maxKey_mem [TransOrd α] (h : t.WF) {he} :
|
||||
t.maxKey he ∈ t :=
|
||||
contains_maxKey h
|
||||
|
||||
theorem le_maxKey_of_contains [TransOrd α] (h : t.WF) {k} :
|
||||
(hc : t.contains k) →
|
||||
compare k (t.maxKey <| (isEmpty_eq_false_iff_exists_contains_eq_true h).mpr ⟨k, hc⟩) |>.isLE := by
|
||||
simp_to_model [maxKey, contains] using le_maxKey_of_containsKey
|
||||
|
||||
theorem le_maxKey_of_mem [TransOrd α] (h : t.WF) {k} (hc : k ∈ t) :
|
||||
compare k (t.maxKey <| (isEmpty_eq_false_iff_exists_contains_eq_true h).mpr ⟨k, hc⟩) |>.isLE :=
|
||||
le_maxKey_of_contains h hc
|
||||
|
||||
theorem maxKey_le [TransOrd α] (h : t.WF) {k he} :
|
||||
(compare (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (compare k' k).isLE) := by
|
||||
simp_to_model [maxKey, contains] using List.maxKey_le
|
||||
|
||||
theorem getKey?_maxKey [TransOrd α] (h : t.WF) {he} :
|
||||
t.getKey? (t.maxKey he) = some (t.maxKey he) := by
|
||||
simp_to_model [getKey?, maxKey] using List.getKey?_maxKey
|
||||
|
||||
theorem getKey_maxKey [TransOrd α] (h : t.WF) {he hc} :
|
||||
t.getKey (t.maxKey he) hc = t.maxKey he := by
|
||||
simp_to_model [getKey, maxKey] using List.getKey_maxKey
|
||||
|
||||
theorem getKey!_maxKey [TransOrd α] [Inhabited α] (h : t.WF) {he} :
|
||||
t.getKey! (t.maxKey he) = t.maxKey he := by
|
||||
simp_to_model [getKey!, maxKey] using List.getKey!_maxKey
|
||||
|
||||
theorem getKeyD_maxKey [TransOrd α] (h : t.WF) {he fallback} :
|
||||
t.getKeyD (t.maxKey he) fallback = t.maxKey he := by
|
||||
simp_to_model [getKeyD, maxKey] using List.getKeyD_maxKey
|
||||
|
||||
theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransOrd α] (h : t.WF) {k he} :
|
||||
(t.erase k h.balanced |>.impl.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he) ↔
|
||||
¬ compare k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false h he) = .eq := by
|
||||
simp_to_model [maxKey, erase] using List.maxKey_eraseKey_eq_iff_beq_maxKey_eq_false
|
||||
|
||||
theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransOrd α] (h : t.WF) {k he} :
|
||||
(hc : ¬ compare k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he)) = .eq) →
|
||||
(t.erase k h.balanced |>.impl.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false h he) := by
|
||||
simp_to_model [maxKey, erase] using List.maxKey_eraseKey_eq_of_beq_maxKey_eq_false
|
||||
|
||||
theorem maxKey_erase_le_maxKey [TransOrd α] (h : t.WF) {k he} :
|
||||
compare (t.erase k h.balanced |>.impl.maxKey he)
|
||||
(t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false h he) |>.isLE := by
|
||||
simp_to_model [maxKey, erase] using List.maxKey_eraseKey_le_maxKey
|
||||
|
||||
theorem maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v} :
|
||||
(t.insertIfNew k v h.balanced).impl.maxKey (isEmpty_insertIfNew h) =
|
||||
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_le_maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v he} :
|
||||
compare (t.maxKey he)
|
||||
(t.insertIfNew k v h.balanced |>.impl.maxKey <| isEmpty_insertIfNew h) |>.isLE := by
|
||||
simp_to_model [maxKey, insertIfNew] using List.maxKey_le_maxKey_insertEntryIfNew
|
||||
|
||||
theorem self_le_maxKey_insertIfNew [TransOrd α] (h : t.WF) {k v} :
|
||||
compare k (t.insertIfNew k v h.balanced |>.impl.maxKey <| isEmpty_insertIfNew h) |>.isLE := by
|
||||
simp_to_model [maxKey, insertIfNew] using List.self_le_maxKey_insertEntryIfNew
|
||||
|
||||
theorem maxKey_eq_getLast_keys [TransOrd α] (h : t.WF) {he} :
|
||||
t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
|
||||
simp_to_model [maxKey, keys] using List.maxKey_eq_getLast_keys h.ordered.distinctKeys h.ordered
|
||||
|
||||
theorem maxKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
|
||||
(t.modify k f).maxKey he = t.maxKey (isEmpty_modify h ▸ he):= by
|
||||
simp_to_model [maxKey, modify] using List.maxKey_modifyKey
|
||||
|
||||
theorem maxKey_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
|
||||
(t.alter k f h.balanced).impl.maxKey he = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simp_to_model [maxKey, alter, get?, contains] using List.maxKey_alterKey_eq_self
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Impl α β}
|
||||
|
||||
theorem maxKey_modify [TransOrd α] (h : t.WF) {k f he} :
|
||||
(modify k f t).maxKey he =
|
||||
if compare (t.maxKey <| isEmpty_modify h ▸ he) k = .eq then
|
||||
k
|
||||
else
|
||||
(t.maxKey <| Const.isEmpty_modify h ▸ he) := by
|
||||
simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey
|
||||
|
||||
theorem maxKey_modify_eq_maxKey [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
|
||||
(modify k f t).maxKey he = t.maxKey (isEmpty_modify h ▸ he) := by
|
||||
simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey_eq_maxKey
|
||||
|
||||
theorem compare_maxKey_modify_eq [TransOrd α] (h : t.WF) {k f he} :
|
||||
compare (modify k f t |>.maxKey he) (t.maxKey <| isEmpty_modify h ▸ he) = .eq := by
|
||||
simp_to_model [maxKey, Const.modify] using List.Const.maxKey_modifyKey_beq
|
||||
|
||||
theorem maxKey_alter_eq_self [TransOrd α] (h : t.WF) {k f he} :
|
||||
(alter k f t h.balanced).impl.maxKey he = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by
|
||||
simp_to_model [maxKey, Const.alter, contains, Const.get?] using List.Const.maxKey_alterKey_eq_self
|
||||
|
||||
end Const
|
||||
|
||||
|
||||
end Max
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -493,6 +493,14 @@ theorem maxKey?_eq_minKey?_reverse [Ord α] {l : Impl α β} :
|
|||
l.maxKey? = (letI : Ord α := .opposite inferInstance; (reverse l).minKey?) := by
|
||||
induction l using maxKey?.induct <;> simp_all only [minKey?, maxKey?, reverse]
|
||||
|
||||
theorem some_maxKey_eq_maxKey? [Ord α] {l : Impl α β} {he} :
|
||||
some (l.maxKey he) = l.maxKey? := by
|
||||
induction l, he using maxKey.induct <;> simp_all [maxKey, maxKey?]
|
||||
|
||||
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 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!,
|
||||
|
|
|
|||
|
|
@ -307,8 +307,8 @@ def maxEntry? : Impl α β → Option ((a : α) × β a)
|
|||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxEntry : (t : Impl α β) → (h : t.isEmpty = false) → (a : α) × β a
|
||||
| .inner _ k v .leaf _, _ => ⟨k, v⟩
|
||||
| .inner _ _ _ l@(.inner ..) _, h => l.maxEntry (by simp_all [isEmpty])
|
||||
| .inner _ k v _ .leaf, _ => ⟨k, v⟩
|
||||
| .inner _ _ _ _ l@(.inner ..), h => l.maxEntry (by simp_all [isEmpty])
|
||||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxEntry! [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a
|
||||
|
|
@ -353,8 +353,8 @@ def maxKey? : Impl α β → Option α
|
|||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxKey : (t : Impl α β) → (h : t.isEmpty = false) → α
|
||||
| .inner _ k _ .leaf _, _ => k
|
||||
| .inner _ _ _ l@(.inner ..) _, h => l.maxKey (by simp_all [isEmpty])
|
||||
| .inner _ k _ _ .leaf, _ => k
|
||||
| .inner _ _ _ _ l@(.inner ..), h => l.maxKey (by simp_all [isEmpty])
|
||||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxKey! [Inhabited α] : Impl α β → α
|
||||
|
|
@ -756,8 +756,8 @@ def maxEntry? : Impl α β → Option (α × β)
|
|||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxEntry : (t : Impl α β) → (h : t.isEmpty = false) → α × β
|
||||
| .inner _ k v .leaf _, _ => ⟨k, v⟩
|
||||
| .inner _ _ _ l@(.inner ..) _, h => maxEntry l (by simp_all [isEmpty])
|
||||
| .inner _ k v _ .leaf, _ => ⟨k, v⟩
|
||||
| .inner _ _ _ _ l@(.inner ..), h => maxEntry l (by simp_all [isEmpty])
|
||||
|
||||
/-- Implementation detail of the tree map -/
|
||||
def maxEntry! [Inhabited (α × β)] : Impl α β → α × β
|
||||
|
|
|
|||
|
|
@ -1856,4 +1856,8 @@ theorem maxKey?_eq_maxKey? [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Orde
|
|||
rw [maxKey?_of_perm hlo.distinctKeys (List.reverse_perm t.toListModel).symm, List.maxKey?]
|
||||
rw [maxKey?_eq_minKey?_reverse, minKey?_eq_minKey? hlo.reverse, toListModel_reverse]
|
||||
|
||||
theorem maxKey_eq_maxKey [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Ordered) {he} :
|
||||
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]
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -3615,6 +3615,152 @@ theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem maxKey_eq_get_maxKey? [TransCmp cmp] {he} :
|
||||
t.maxKey he = t.maxKey?.get (isSome_maxKey?_iff_isEmpty_eq_false.mpr he) :=
|
||||
letI : Ord α := ⟨cmp⟩
|
||||
Impl.maxKey_eq_get_maxKey?
|
||||
|
||||
theorem maxKey?_eq_some_maxKey [TransCmp cmp] {he} :
|
||||
t.maxKey? = some (t.maxKey he) :=
|
||||
Impl.maxKey?_eq_some_maxKey t.wf
|
||||
|
||||
theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
|
||||
t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
Impl.maxKey_eq_iff_getKey?_eq_self_and_forall t.wf
|
||||
|
||||
theorem maxKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
|
||||
t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
Impl.maxKey_eq_some_iff_mem_and_forall t.wf
|
||||
|
||||
theorem maxKey_insert [TransCmp cmp] {k v} :
|
||||
(t.insert k v).maxKey isEmpty_insert =
|
||||
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] {k v he} :
|
||||
cmp (t.maxKey he) (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
|
||||
Impl.maxKey_le_maxKey_insert t.wf
|
||||
|
||||
theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
|
||||
cmp k (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
|
||||
Impl.self_le_maxKey_insert t.wf
|
||||
|
||||
theorem contains_maxKey [TransCmp cmp] {he} :
|
||||
t.contains (t.maxKey he) :=
|
||||
Impl.contains_maxKey t.wf
|
||||
|
||||
theorem maxKey_mem [TransCmp cmp] {he} :
|
||||
t.maxKey he ∈ t :=
|
||||
Impl.maxKey_mem t.wf
|
||||
|
||||
theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
|
||||
cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
Impl.le_maxKey_of_contains t.wf hc
|
||||
|
||||
theorem le_maxKey_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
|
||||
cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
Impl.le_maxKey_of_mem t.wf hc
|
||||
|
||||
theorem maxKey_le [TransCmp cmp] {k he} :
|
||||
(cmp (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
Impl.maxKey_le t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKey?_maxKey [TransCmp cmp] {he} :
|
||||
t.getKey? (t.maxKey he) = some (t.maxKey he) :=
|
||||
Impl.getKey?_maxKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKey_maxKey [TransCmp cmp] {he hc} :
|
||||
t.getKey (t.maxKey he) hc = t.maxKey he :=
|
||||
Impl.getKey_maxKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKey!_maxKey [TransCmp cmp] [Inhabited α] {he} :
|
||||
t.getKey! (t.maxKey he) = t.maxKey he :=
|
||||
Impl.getKey!_maxKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem getKeyD_maxKey [TransCmp cmp] {he fallback} :
|
||||
t.getKeyD (t.maxKey he) fallback = t.maxKey he :=
|
||||
Impl.getKeyD_maxKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransCmp cmp] {k he} :
|
||||
(t.erase k |>.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
|
||||
¬ cmp k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
|
||||
Impl.maxKey_erase_eq_iff_not_compare_eq_maxKey t.wf
|
||||
|
||||
theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransCmp cmp] {k he} :
|
||||
(hc : ¬ cmp k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
|
||||
(t.erase k |>.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
|
||||
Impl.maxKey_erase_eq_of_not_compare_eq_maxKey t.wf
|
||||
|
||||
theorem maxKey_erase_le_maxKey [TransCmp cmp] {k he} :
|
||||
cmp (t.erase k |>.maxKey he)
|
||||
(t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
|
||||
Impl.maxKey_erase_le_maxKey t.wf
|
||||
|
||||
theorem maxKey_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).maxKey isEmpty_insertIfNew =
|
||||
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] {k v he} :
|
||||
cmp (t.maxKey he)
|
||||
(t.insertIfNew k v |>.maxKey isEmpty_insertIfNew) |>.isLE :=
|
||||
Impl.maxKey_le_maxKey_insertIfNew t.wf
|
||||
|
||||
theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
|
||||
cmp k (t.insertIfNew k v |>.maxKey <| isEmpty_insertIfNew) |>.isLE :=
|
||||
Impl.self_le_maxKey_insertIfNew t.wf
|
||||
|
||||
theorem maxKey_eq_getLast_keys [TransCmp cmp] {he} :
|
||||
t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
|
||||
Impl.maxKey_eq_getLast_keys t.wf
|
||||
|
||||
@[simp]
|
||||
theorem maxKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
|
||||
(t.modify k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
Impl.maxKey_modify t.wf
|
||||
|
||||
theorem maxKey_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
|
||||
(t.alter k f).maxKey he = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.maxKey_alter_eq_self t.wf
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : DTreeMap α β cmp}
|
||||
|
||||
theorem maxKey_modify [TransCmp cmp] {k f he} :
|
||||
(modify t k f).maxKey he =
|
||||
if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
|
||||
k
|
||||
else
|
||||
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
Impl.Const.maxKey_modify t.wf
|
||||
|
||||
@[simp]
|
||||
theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
|
||||
(modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
Impl.Const.maxKey_modify_eq_maxKey t.wf
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
|
||||
cmp (modify t k f |>.maxKey he)
|
||||
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
|
||||
Impl.Const.compare_maxKey_modify_eq t.wf
|
||||
|
||||
theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
|
||||
(alter t k f).maxKey he = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
Impl.Const.maxKey_alter_eq_self t.wf
|
||||
|
||||
end Const
|
||||
|
||||
end Max
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -5647,6 +5647,199 @@ theorem maxKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
|
|||
|
||||
end Const
|
||||
|
||||
/-- Given a proof that the list is nonempty, returns the largest key in an associative list. -/
|
||||
abbrev maxKey [Ord α] (xs : List ((a : α) × β a)) (h : xs.isEmpty = false) : α :=
|
||||
letI : Ord α := .opposite inferInstance; minKey xs h
|
||||
|
||||
theorem maxKey_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)}
|
||||
{hl} (hd : DistinctKeys l) (hp : l.Perm l') :
|
||||
maxKey l hl = maxKey l' (hp.isEmpty_eq ▸ hl) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_of_perm hd hp
|
||||
|
||||
theorem maxKey_eq_get_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {he} :
|
||||
maxKey l he = (maxKey? l |>.get (by simp [isSome_maxKey?_eq_not_isEmpty, he])) :=
|
||||
rfl
|
||||
|
||||
theorem maxKey?_eq_some_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {he} :
|
||||
maxKey? l = some (maxKey l he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey?_eq_some_minKey
|
||||
|
||||
theorem maxKey_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
|
||||
maxKey l he = 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
|
||||
|
||||
theorem maxKey_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
|
||||
maxKey l he = km ↔ containsKey km l ∧ ∀ k, containsKey k l → (compare k km).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_eq_some_iff_mem_and_forall hd
|
||||
|
||||
theorem maxKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)}
|
||||
(hd : DistinctKeys l) {k v} :
|
||||
(insertEntry k v l |> maxKey <| isEmpty_insertEntry) =
|
||||
((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 α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v he} :
|
||||
compare (maxKey l he) (insertEntry k v l |> maxKey <| isEmpty_insertEntry) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_insertEntry_le_minKey hd
|
||||
|
||||
theorem self_le_maxKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare k (insertEntry k v l |> maxKey <| isEmpty_insertEntry) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_insertEntry_le_self hd
|
||||
|
||||
theorem containsKey_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
containsKey (maxKey l he) l :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
containsKey_minKey hd
|
||||
|
||||
theorem le_maxKey_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (hc : containsKey k l) :
|
||||
compare k (maxKey l <| isEmpty_eq_false_iff_exists_containsKey.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_le_of_containsKey hd hc
|
||||
|
||||
theorem maxKey_le [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
|
||||
(compare (maxKey l he) k).isLE ↔ (∀ k', containsKey k' l → (compare k' k).isLE) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
le_minKey hd
|
||||
|
||||
theorem getKey?_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey? (maxKey l he) l = some (maxKey l he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey?_minKey hd
|
||||
|
||||
theorem getKey_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey (maxKey l he) l (containsKey_maxKey hd) = maxKey l he :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey_minKey hd
|
||||
|
||||
theorem getKey!_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
getKey! (maxKey l he) l = maxKey l he :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKey!_minKey hd
|
||||
|
||||
theorem getKeyD_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he fallback} :
|
||||
getKeyD (maxKey l he) l fallback = maxKey l he :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
getKeyD_minKey hd
|
||||
|
||||
theorem maxKey_eraseKey_eq_iff_beq_maxKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
|
||||
(eraseKey k l |> maxKey <| he) =
|
||||
maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) ↔
|
||||
(k == (maxKey l <| isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he)) = false :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_eraseKey_eq_iff_beq_minKey_eq_false hd
|
||||
|
||||
theorem maxKey_eraseKey_eq_of_beq_maxKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
|
||||
(hc : (k == (maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he))) = false) →
|
||||
(eraseKey k l |> maxKey <| he) =
|
||||
maxKey l (isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_eraseKey_eq_of_beq_minKey_eq_false hd
|
||||
|
||||
theorem maxKey_eraseKey_le_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k he} :
|
||||
compare (eraseKey k l |> maxKey <| he)
|
||||
(maxKey l <| isEmpty_eq_false_of_isEmpty_eraseKey_eq_false hd he) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_le_minKey_erase hd
|
||||
|
||||
theorem maxKey_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
(insertEntryIfNew k v l |> maxKey <| isEmpty_insertEntryIfNew) =
|
||||
(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 α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v he} :
|
||||
compare (maxKey l he)
|
||||
(insertEntryIfNew k v l |> maxKey <| isEmpty_insertEntryIfNew) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_insertEntryIfNew_le_minKey hd
|
||||
|
||||
theorem self_le_maxKey_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} :
|
||||
compare k (insertEntryIfNew k v l |> maxKey <| isEmpty_insertEntryIfNew) |>.isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_insertEntryIfNew_le_self hd
|
||||
|
||||
theorem maxKey_eq_getLast_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {he} :
|
||||
maxKey l he = (keys l).getLast (by simp_all [keys_eq_map, List.isEmpty_eq_false_iff]) := by
|
||||
simp only [List.getLast_eq_head_reverse, reverse_keys, maxKey_of_perm hd (List.reverse_perm l).symm]
|
||||
letI : Ord α := .opposite inferInstance
|
||||
exact minKey_eq_head_keys (List.pairwise_reverse.mpr ho)
|
||||
|
||||
theorem maxKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
|
||||
(modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he):=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_modifyKey hd
|
||||
|
||||
theorem maxKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f he} :
|
||||
(alterKey k f l |> maxKey <| he) = k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_alterKey_eq_self hd
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
theorem maxKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
|
||||
(modifyKey k f l |> maxKey <| he) =
|
||||
if (maxKey l <| isEmpty_modifyKey k f l ▸ he) == k then
|
||||
k
|
||||
else
|
||||
(maxKey l <| isEmpty_modifyKey k f l ▸ he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_modifyKey hd
|
||||
|
||||
theorem maxKey_modifyKey_eq_maxKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
|
||||
(modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_modifyKey_eq_minKey hd
|
||||
|
||||
theorem maxKey_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
|
||||
(modifyKey k f l |> maxKey <| he) == (maxKey l <| isEmpty_modifyKey k f l ▸ he) :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_modifyKey_beq hd
|
||||
|
||||
theorem maxKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f he} :
|
||||
(alterKey k f l |> maxKey <| he) = k ↔
|
||||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE :=
|
||||
letI : Ord α := .opposite inferInstance
|
||||
minKey_alterKey_eq_self hd
|
||||
|
||||
end Const
|
||||
|
||||
end Max
|
||||
|
||||
end Std.Internal.List
|
||||
|
|
|
|||
|
|
@ -2010,13 +2010,13 @@ theorem getKeyD_minKey [TransCmp cmp] {he fallback} :
|
|||
DTreeMap.getKeyD_minKey
|
||||
|
||||
@[simp]
|
||||
theorem minKey_erase_eq_iff_not_cmp_eq_minKey [TransCmp cmp] {k he} :
|
||||
theorem minKey_erase_eq_iff_not_compare_eq_minKey [TransCmp cmp] {k he} :
|
||||
(t.erase k |>.minKey he) =
|
||||
t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
|
||||
¬ cmp k (t.minKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
|
||||
DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey
|
||||
|
||||
theorem minKey_erase_eq_of_not_cmp_eq_minKey [TransCmp cmp] {k he} :
|
||||
theorem minKey_erase_eq_of_not_compare_eq_minKey [TransCmp cmp] {k he} :
|
||||
(hc : ¬ cmp k (t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
|
||||
(t.erase k |>.minKey he) =
|
||||
t.minKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
|
||||
|
|
@ -2058,6 +2058,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) :=
|
||||
DTreeMap.Const.minKey_modify_eq_minKey
|
||||
|
||||
@[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 :=
|
||||
|
|
@ -2494,6 +2495,136 @@ theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} :
|
|||
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
DTreeMap.Const.maxKey?_alter_eq_self
|
||||
|
||||
theorem maxKey_eq_get_maxKey? [TransCmp cmp] {he} :
|
||||
t.maxKey he = t.maxKey?.get (isSome_maxKey?_iff_isEmpty_eq_false.mpr he) :=
|
||||
DTreeMap.maxKey_eq_get_maxKey?
|
||||
|
||||
theorem maxKey?_eq_some_maxKey [TransCmp cmp] {he} :
|
||||
t.maxKey? = some (t.maxKey he) :=
|
||||
DTreeMap.maxKey?_eq_some_maxKey
|
||||
|
||||
theorem maxKey_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
|
||||
t.maxKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
DTreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem maxKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
|
||||
t.maxKey he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
DTreeMap.maxKey_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem maxKey_insert [TransCmp cmp] {k v} :
|
||||
(t.insert k v).maxKey isEmpty_insert =
|
||||
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] {k v he} :
|
||||
cmp (t.maxKey he) (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
|
||||
DTreeMap.maxKey_le_maxKey_insert
|
||||
|
||||
theorem self_le_maxKey_insert [TransCmp cmp] {k v} :
|
||||
cmp k (t.insert k v |>.maxKey isEmpty_insert) |>.isLE :=
|
||||
DTreeMap.self_le_maxKey_insert
|
||||
|
||||
theorem contains_maxKey [TransCmp cmp] {he} :
|
||||
t.contains (t.maxKey he) :=
|
||||
DTreeMap.contains_maxKey
|
||||
|
||||
theorem maxKey_mem [TransCmp cmp] {he} :
|
||||
t.maxKey he ∈ t :=
|
||||
DTreeMap.maxKey_mem
|
||||
|
||||
theorem le_maxKey_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
|
||||
cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
DTreeMap.le_maxKey_of_contains hc
|
||||
|
||||
theorem le_maxKey_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
|
||||
cmp k (t.maxKey <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
DTreeMap.le_maxKey_of_mem hc
|
||||
|
||||
theorem maxKey_le [TransCmp cmp] {k he} :
|
||||
(cmp (t.maxKey he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
DTreeMap.maxKey_le
|
||||
|
||||
@[simp]
|
||||
theorem getKey?_maxKey [TransCmp cmp] {he} :
|
||||
t.getKey? (t.maxKey he) = some (t.maxKey he) :=
|
||||
DTreeMap.getKey?_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem getKey_maxKey [TransCmp cmp] {he hc} :
|
||||
t.getKey (t.maxKey he) hc = t.maxKey he :=
|
||||
DTreeMap.getKey_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem getKey!_maxKey [TransCmp cmp] [Inhabited α] {he} :
|
||||
t.getKey! (t.maxKey he) = t.maxKey he :=
|
||||
DTreeMap.getKey!_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem getKeyD_maxKey [TransCmp cmp] {he fallback} :
|
||||
t.getKeyD (t.maxKey he) fallback = t.maxKey he :=
|
||||
DTreeMap.getKeyD_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem maxKey_erase_eq_iff_not_compare_eq_maxKey [TransCmp cmp] {k he} :
|
||||
(t.erase k |>.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
|
||||
¬ cmp k (t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
|
||||
DTreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey
|
||||
|
||||
theorem maxKey_erase_eq_of_not_compare_eq_maxKey [TransCmp cmp] {k he} :
|
||||
(hc : ¬ cmp k (t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
|
||||
(t.erase k |>.maxKey he) =
|
||||
t.maxKey (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
|
||||
DTreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey
|
||||
|
||||
theorem maxKey_erase_le_maxKey [TransCmp cmp] {k he} :
|
||||
cmp (t.erase k |>.maxKey he)
|
||||
(t.maxKey <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
|
||||
DTreeMap.maxKey_erase_le_maxKey
|
||||
|
||||
theorem maxKey_insertIfNew [TransCmp cmp] {k v} :
|
||||
(t.insertIfNew k v).maxKey isEmpty_insertIfNew =
|
||||
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] {k v he} :
|
||||
cmp (t.maxKey he)
|
||||
(t.insertIfNew k v |>.maxKey isEmpty_insertIfNew) |>.isLE :=
|
||||
DTreeMap.maxKey_le_maxKey_insertIfNew (t := t.inner) (he := he)
|
||||
|
||||
theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} :
|
||||
cmp k (t.insertIfNew k v |>.maxKey <| isEmpty_insertIfNew) |>.isLE :=
|
||||
DTreeMap.self_le_maxKey_insertIfNew
|
||||
|
||||
theorem maxKey_eq_getLast_keys [TransCmp cmp] {he} :
|
||||
t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
|
||||
DTreeMap.maxKey_eq_getLast_keys
|
||||
|
||||
theorem maxKey_modify [TransCmp cmp] {k f he} :
|
||||
(modify t k f).maxKey he =
|
||||
if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
|
||||
k
|
||||
else
|
||||
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
DTreeMap.Const.maxKey_modify
|
||||
|
||||
@[simp]
|
||||
theorem maxKey_modify_eq_maxKey [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
|
||||
(modify t k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) :=
|
||||
DTreeMap.Const.maxKey_modify_eq_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem compare_maxKey_modify_eq [TransCmp cmp] {k f he} :
|
||||
cmp (modify t k f |>.maxKey he)
|
||||
(t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) = .eq :=
|
||||
DTreeMap.Const.compare_maxKey_modify_eq
|
||||
|
||||
theorem maxKey_alter_eq_self [TransCmp cmp] {k f he} :
|
||||
(alter t k f).maxKey he = k ↔
|
||||
(f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE :=
|
||||
DTreeMap.Const.maxKey_alter_eq_self
|
||||
|
||||
|
||||
end Max
|
||||
|
||||
end Std.TreeMap
|
||||
|
|
|
|||
|
|
@ -871,13 +871,13 @@ theorem getD_min [TransCmp cmp] {he fallback} :
|
|||
DTreeMap.getKeyD_minKey
|
||||
|
||||
@[simp]
|
||||
theorem min_erase_eq_iff_not_cmp_eq_min [TransCmp cmp] {k he} :
|
||||
theorem min_erase_eq_iff_not_compare_eq_min [TransCmp cmp] {k he} :
|
||||
(t.erase k |>.min he) =
|
||||
t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
|
||||
¬ cmp k (t.min <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
|
||||
DTreeMap.minKey_erase_eq_iff_not_compare_eq_minKey
|
||||
|
||||
theorem min_erase_eq_of_not_cmp_eq_min [TransCmp cmp] {k he} :
|
||||
theorem min_erase_eq_of_not_compare_eq_min [TransCmp cmp] {k he} :
|
||||
(hc : ¬ cmp k (t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
|
||||
(t.erase k |>.min he) =
|
||||
t.min (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
|
||||
|
|
@ -1198,6 +1198,102 @@ theorem max?_erase_le_max? [TransCmp cmp] {k km kme} :
|
|||
cmp kme km |>.isLE :=
|
||||
TreeMap.maxKey?_erase_le_maxKey?
|
||||
|
||||
theorem max?_eq_getLast?_toList [TransCmp cmp] :
|
||||
t.max? = t.toList.getLast? :=
|
||||
TreeMap.maxKey?_eq_getLast?_keys
|
||||
|
||||
theorem max_eq_get_max? [TransCmp cmp] {he} :
|
||||
t.max he = t.max?.get (isSome_max?_iff_isEmpty_eq_false.mpr he) :=
|
||||
TreeMap.maxKey_eq_get_maxKey?
|
||||
|
||||
theorem max?_eq_some_max [TransCmp cmp] {he} :
|
||||
t.max? = some (t.max he) :=
|
||||
TreeMap.maxKey?_eq_some_maxKey
|
||||
|
||||
theorem max_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] {he km} :
|
||||
t.max he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
TreeMap.maxKey_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem max_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he km} :
|
||||
t.max he = km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE :=
|
||||
TreeMap.maxKey_eq_some_iff_mem_and_forall
|
||||
|
||||
theorem max_insert [TransCmp cmp] {k} :
|
||||
(t.insert k).max isEmpty_insert =
|
||||
t.max?.elim k fun k' => if cmp k' k = .lt then k else k' :=
|
||||
TreeMap.maxKey_insertIfNew
|
||||
|
||||
theorem max_le_max_insert [TransCmp cmp] {k he} :
|
||||
cmp (t.max he)
|
||||
(t.insert k |>.max isEmpty_insert) |>.isLE :=
|
||||
TreeMap.maxKey_le_maxKey_insertIfNew
|
||||
|
||||
theorem self_le_max_insert [TransCmp cmp] {k} :
|
||||
cmp k (t.insert k |>.max <| isEmpty_insert) |>.isLE :=
|
||||
TreeMap.self_le_maxKey_insertIfNew
|
||||
|
||||
theorem contains_max [TransCmp cmp] {he} :
|
||||
t.contains (t.max he) :=
|
||||
TreeMap.contains_maxKey
|
||||
|
||||
theorem max_mem [TransCmp cmp] {he} :
|
||||
t.max he ∈ t :=
|
||||
TreeMap.maxKey_mem
|
||||
|
||||
theorem le_max_of_contains [TransCmp cmp] {k} (hc : t.contains k) :
|
||||
cmp k (t.max <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
TreeMap.le_maxKey_of_contains hc
|
||||
|
||||
theorem le_max_of_mem [TransCmp cmp] {k} (hc : k ∈ t) :
|
||||
cmp k (t.max <| isEmpty_eq_false_iff_exists_contains_eq_true.mpr ⟨k, hc⟩) |>.isLE :=
|
||||
TreeMap.le_maxKey_of_mem hc
|
||||
|
||||
theorem max_le [TransCmp cmp] {k he} :
|
||||
(cmp (t.max he) k).isLE ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) :=
|
||||
TreeMap.maxKey_le
|
||||
|
||||
@[simp]
|
||||
theorem get?_max [TransCmp cmp] {he} :
|
||||
t.get? (t.max he) = some (t.max he) :=
|
||||
TreeMap.getKey?_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem get_max [TransCmp cmp] {he hc} :
|
||||
t.get (t.max he) hc = t.max he :=
|
||||
TreeMap.getKey_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem get!_max [TransCmp cmp] [Inhabited α] {he} :
|
||||
t.get! (t.max he) = t.max he :=
|
||||
TreeMap.getKey!_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem getD_max [TransCmp cmp] {he fallback} :
|
||||
t.getD (t.max he) fallback = t.max he :=
|
||||
TreeMap.getKeyD_maxKey
|
||||
|
||||
@[simp]
|
||||
theorem max_erase_eq_iff_not_compare_eq_max [TransCmp cmp] {k he} :
|
||||
(t.erase k |>.max he) =
|
||||
t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he) ↔
|
||||
¬ cmp k (t.max <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) = .eq :=
|
||||
TreeMap.maxKey_erase_eq_iff_not_compare_eq_maxKey
|
||||
|
||||
theorem max_erase_eq_of_not_compare_eq_max [TransCmp cmp] {k he} :
|
||||
(hc : ¬ cmp k (t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he)) = .eq) →
|
||||
(t.erase k |>.max he) =
|
||||
t.max (isEmpty_eq_false_of_isEmpty_erase_eq_false he) :=
|
||||
TreeMap.maxKey_erase_eq_of_not_compare_eq_maxKey
|
||||
|
||||
theorem max_erase_le_max [TransCmp cmp] {k he} :
|
||||
cmp (t.erase k |>.max he)
|
||||
(t.max <| isEmpty_eq_false_of_isEmpty_erase_eq_false he) |>.isLE :=
|
||||
TreeMap.maxKey_erase_le_maxKey
|
||||
|
||||
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
|
||||
|
||||
end Max
|
||||
|
||||
end Std.TreeSet
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue