From e9fda1a3e4df006efb2f54fc18b42718eee1df25 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Wed, 26 Mar 2025 17:13:15 +0100 Subject: [PATCH] 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 --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 236 +++++++++++++++++- src/Std/Data/DTreeMap/Internal/Model.lean | 4 + src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 4 + src/Std/Data/DTreeMap/Lemmas.lean | 172 +++++++++++-- src/Std/Data/DTreeMap/Raw/Lemmas.lean | 161 ++++++++++-- src/Std/Data/Internal/List/Associative.lean | 212 ++++++++++++++++ src/Std/Data/TreeMap/Lemmas.lean | 151 ++++++++++- src/Std/Data/TreeMap/Raw/Lemmas.lean | 141 ++++++++++- src/Std/Data/TreeSet/Lemmas.lean | 109 +++++++- src/Std/Data/TreeSet/Raw/Lemmas.lean | 82 ++++++ 10 files changed, 1201 insertions(+), 71 deletions(-) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index fa9b153f81..47f6c36a58 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean index 9db993de01..51be2c5175 100644 --- a/src/Std/Data/DTreeMap/Internal/Model.lean +++ b/src/Std/Data/DTreeMap/Internal/Model.lean @@ -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!, diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 53eedb0e4b..5490696b74 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 65ff43fd73..598ee161ef 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -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 diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index c7bfad4ae6..222a611d28 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -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 diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 6cd81fb2d0..bd85a75036 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -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 diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index b089408ef2..045511ef53 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index cfd8f4bb24..c59eb9331a 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index b9b783cbb0..71a8bbcc0a 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -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 diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 9fd6334204..ba0414e2e2 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -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