From 7f4e4557a71e68607ef6980f88fbccdff7acd595 Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Tue, 25 Mar 2025 13:41:46 +0100 Subject: [PATCH] feat: tree map lemmas for maxKey? (#7657) This PR provides lemmas for the tree map function `maxKey?` and its interations with other functions for which lemmas already exist. --------- Co-authored-by: Paul Reichert --- src/Std/Classes/Ord.lean | 33 ++ src/Std/Data/DTreeMap/Internal/Lemmas.lean | 289 +++++++++++++++++- src/Std/Data/DTreeMap/Internal/Model.lean | 9 + src/Std/Data/DTreeMap/Internal/Queries.lean | 72 ++--- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 16 +- src/Std/Data/DTreeMap/Lemmas.lean | 213 ++++++++++++- src/Std/Data/DTreeMap/Raw/Lemmas.lean | 241 +++++++++++++-- src/Std/Data/Internal/List/Associative.lean | 273 ++++++++++++++++- src/Std/Data/TreeMap/Lemmas.lean | 192 +++++++++++- src/Std/Data/TreeMap/Raw/Lemmas.lean | 190 +++++++++++- src/Std/Data/TreeSet/Lemmas.lean | 130 ++++++++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 134 ++++++++ 12 files changed, 1715 insertions(+), 77 deletions(-) diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean index da7d79bd69..11fc932429 100644 --- a/src/Std/Classes/Ord.lean +++ b/src/Std/Classes/Ord.lean @@ -69,6 +69,13 @@ variable {α : Type u} {cmp : α → α → Ordering} instance [OrientedCmp cmp] : ReflCmp cmp where compare_self := Ordering.eq_eq_of_eq_swap OrientedCmp.eq_swap +instance OrientedCmp.opposite [OrientedCmp cmp] : OrientedCmp fun a b => cmp b a where + eq_swap := OrientedCmp.eq_swap (cmp := cmp) + +instance OrientedOrd.opposite [Ord α] [OrientedOrd α] : + letI : Ord α := .opposite inferInstance; OrientedOrd α := + OrientedCmp.opposite (cmp := compare) + theorem OrientedCmp.gt_iff_lt [OrientedCmp cmp] {a b : α} : cmp a b = .gt ↔ cmp b a = .lt := by rw [OrientedCmp.eq_swap (cmp := cmp) (a := a) (b := b)] cases cmp b a <;> simp @@ -155,6 +162,13 @@ theorem TransCmp.isGE_trans [TransCmp cmp] {a b c : α} (h₁ : (cmp a b).isGE) rw [OrientedCmp.isGE_iff_isLE] at * exact TransCmp.isLE_trans h₂ h₁ +instance TransCmp.opposite [TransCmp cmp] : TransCmp fun a b => cmp b a where + isLE_trans := flip TransCmp.isLE_trans + +instance TransOrd.opposite [Ord α] [TransOrd α] : + letI : Ord α := .opposite inferInstance; TransOrd α := + TransCmp.opposite (cmp := compare) + theorem TransCmp.lt_of_lt_of_eq [TransCmp cmp] {a b c : α} (hab : cmp a b = .lt) (hbc : cmp b c = .eq) : cmp a c = .lt := by apply OrientedCmp.lt_of_not_isLE @@ -281,6 +295,16 @@ abbrev LawfulEqOrd (α : Type u) [Ord α] := LawfulEqCmp (compare : α → α variable {α : Type u} {cmp : α → α → Ordering} [LawfulEqCmp cmp] +instance LawfulEqCmp.opposite [OrientedCmp cmp] [LawfulEqCmp cmp] : + LawfulEqCmp (fun a b => cmp b a) where + eq_of_compare := by + simp only [OrientedCmp.eq_comm (cmp := cmp)] + exact LawfulEqCmp.eq_of_compare + +instance LawfulEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulEqOrd α] : + letI : Ord α := .opposite inferInstance; LawfulEqOrd α := + LawfulEqCmp.opposite (cmp := compare) + @[simp] theorem compare_eq_iff_eq {a b : α} : cmp a b = .eq ↔ a = b := ⟨LawfulEqCmp.eq_of_compare, by rintro rfl; exact ReflCmp.compare_self⟩ @@ -360,6 +384,15 @@ instance LawfulBEqCmp.lawfulBEqCmp [inst : LawfulBEqCmp cmp] [LawfulBEq α] : La theorem LawfulBEqOrd.lawfulBEqOrd [Ord α] [LawfulBEqOrd α] [LawfulBEq α] : LawfulEqOrd α := LawfulBEqCmp.lawfulBEqCmp +instance LawfulBEqCmp.opposite [OrientedCmp cmp] [LawfulBEqCmp cmp] : + LawfulBEqCmp (fun a b => cmp b a) where + compare_eq_iff_beq := by + simp [OrientedCmp.eq_comm (cmp := cmp), LawfulBEqCmp.compare_eq_iff_beq] + +instance LawfulBEqOrd.opposite [Ord α] [OrientedOrd α] [LawfulBEqOrd α] : + letI : Ord α := .opposite inferInstance; LawfulBEqOrd α := + LawfulBEqCmp.opposite (cmp := compare) + end LawfulBEq namespace Internal diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index ebee4cce6e..0f3d99890b 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -99,7 +99,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 _)])⟩, ⟨`minKey!, (``minKey!_eq_minKey!, #[``(minKey!_of_perm _)])⟩, - ⟨`minKeyD, (``minKeyD_eq_minKeyD, #[``(minKeyD_of_perm _)])⟩] + ⟨`minKeyD, (``minKeyD_eq_minKeyD, #[``(minKeyD_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 @@ -4289,12 +4290,12 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransOrd α] (h : t.WF) : theorem minKey?_insert [TransOrd α] (h : t.WF) {k v} : (t.insert k v h.balanced).impl.minKey? = - some (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + some (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simp_to_model [insert] using List.minKey?_insertEntry theorem minKey?_insert! [TransOrd α] (h : t.WF) {k v} : (t.insert! k v).minKey? = - some (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + some (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simpa only [insert_eq_insert!] using minKey?_insert h theorem isSome_minKey?_insert [TransOrd α] (h : t.WF) {k v} : @@ -4541,7 +4542,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t. theorem minKey_insert [TransOrd α] (h : t.WF) {k v} : (t.insert k v h.balanced).impl.minKey (isEmpty_insert h) = - t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k' := by + t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k' := by simp_to_model [insert, minKey, minKey?] using List.minKey_insertEntry theorem minKey_insert_le_minKey [TransOrd α] (h : t.WF) {k v he} : @@ -4686,12 +4687,12 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransOrd α] theorem minKey!_insert [TransOrd α] [Inhabited α] (h : t.WF) {k v} : (t.insert k v h.balanced |>.impl.minKey!) = - (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simp_to_model [minKey!, minKey?, insert] using List.minKey!_insertEntry theorem minKey!_insert! [TransOrd α] [Inhabited α] (h : t.WF) {k v} : (t.insert! k v |>.minKey!) = - (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simpa [insert_eq_insert!] using minKey!_insert h theorem minKey!_insert_le_minKey! [TransOrd α] [Inhabited α] (h : t.WF) : @@ -4900,12 +4901,12 @@ theorem minKeyD_eq_some_iff_mem_and_forall [TransOrd α] theorem minKeyD_insert [TransOrd α] (h : t.WF) {k v fallback} : (t.insert k v h.balanced |>.impl.minKeyD <| fallback) = - (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simp_to_model [minKeyD, minKey?, insert] using List.minKeyD_insertEntry theorem minKeyD_insert! [TransOrd α] (h : t.WF) {k v fallback} : (t.insert! k v |>.minKeyD fallback) = - (t.minKey?.elim k fun k' => if compare k k'|>.isLE then k else k') := by + (t.minKey?.elim k fun k' => if compare k k' |>.isLE then k else k') := by simpa [insert_eq_insert!] using minKeyD_insert h theorem minKeyD_insert_le_minKeyD [TransOrd α] (h : t.WF) : @@ -5090,4 +5091,276 @@ end Const end Min +section Max + +theorem maxKey?_empty : + (empty : Impl α β).maxKey? = none := by + unfold maxKey?; rfl + +theorem maxKey?_of_isEmpty [TransOrd α] (h : t.WF) : + (he : t.isEmpty) → t.maxKey? = none := by + simp_to_model using List.maxKey?_of_isEmpty + +theorem maxKey?_eq_none_iff [TransOrd α] (h : t.WF) : + t.maxKey? = none ↔ t.isEmpty := by + simp_to_model using List.maxKey?_eq_none_iff_isEmpty + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) {km} : + t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare k km).isLE := by + simp_to_model using List.maxKey?_eq_some_iff_getKey?_eq_self_and_forall + +theorem maxKey?_eq_some_iff_mem_and_forall [TransOrd α] [LawfulEqOrd α] (h : t.WF) {km} : + t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (compare k km).isLE := by + simp_to_model using List.maxKey?_eq_some_iff_mem_and_forall + +theorem isNone_maxKey?_eq_isEmpty [TransOrd α] (h : t.WF) : + t.maxKey?.isNone = t.isEmpty := by + simp_to_model using List.isNone_maxKey?_eq_isEmpty + +theorem isSome_maxKey?_eq_not_isEmpty [TransOrd α] (h : t.WF) : + t.maxKey?.isSome = !t.isEmpty := by + simp_to_model using List.isSome_maxKey?_eq_not_isEmpty + +theorem isSome_maxKey?_iff_isEmpty_eq_false [TransOrd α] (h : t.WF) : + t.maxKey?.isSome ↔ t.isEmpty = false := by + simp [isSome_maxKey?_eq_not_isEmpty h] + +theorem maxKey?_insert [TransOrd α] (h : t.WF) {k v} : + (t.insert k v h.balanced).impl.maxKey? = + some (t.maxKey?.elim k fun k' => if compare k' k|>.isLE then k else k') := by + simp_to_model [insert] using List.maxKey?_insertEntry + +theorem maxKey?_insert! [TransOrd α] (h : t.WF) {k v} : + (t.insert! k v).maxKey? = + some (t.maxKey?.elim k fun k' => if compare k' k|>.isLE then k else k') := by + simpa only [insert_eq_insert!] using maxKey?_insert h + +theorem isSome_maxKey?_insert [TransOrd α] (h : t.WF) {k v} : + (t.insert k v h.balanced).impl.maxKey?.isSome := by + simp_to_model [insert] using List.isSome_maxKey?_insertEntry + +theorem isSome_maxKey?_insert! [TransOrd α] (h : t.WF) {k v} : + (t.insert! k v).maxKey?.isSome := by + simpa only [insert_eq_insert!] using isSome_maxKey?_insert h + +theorem maxKey?_le_maxKey?_insert [TransOrd α] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert k v h.balanced |>.impl.maxKey? |>.get <| isSome_maxKey?_insert h) = kmi) → + compare km kmi |>.isLE := by + simp_to_model [insert] using List.maxKey?_le_maxKey?_insertEntry + +theorem maxKey?_le_maxKey?_insert! [TransOrd α] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert! k v |>.maxKey? |>.get <| isSome_maxKey?_insert! h) = kmi) → + compare km kmi |>.isLE := by + simpa only [insert_eq_insert!] using maxKey?_le_maxKey?_insert h + +theorem self_le_maxKey?_insert [TransOrd α] (h : t.WF) {k v kmi} : + (hkmi : (t.insert k v h.balanced |>.impl.maxKey?.get <| isSome_maxKey?_insert h) = kmi) → + compare k kmi |>.isLE := by + simp_to_model [insert] using List.self_le_maxKey?_insertEntry + +theorem self_le_maxKey?_insert! [TransOrd α] (h : t.WF) {k v kmi} : + (hkmi : (t.insert! k v |>.maxKey?.get <| isSome_maxKey?_insert! h) = kmi) → + compare k kmi |>.isLE := by + simpa only [insert_eq_insert!] using self_le_maxKey?_insert h + +theorem contains_maxKey? [TransOrd α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → + t.contains km := by + simp_to_model using List.containsKey_maxKey? + +theorem maxKey?_mem [TransOrd α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → + km ∈ t := by + simp_to_model using List.containsKey_maxKey? + +theorem isSome_maxKey?_of_contains [TransOrd α] (h : t.WF) {k} : + (hc : t.contains k) → t.maxKey?.isSome := by + simp_to_model using List.isSome_maxKey?_of_containsKey + +theorem isSome_maxKey?_of_mem [TransOrd α] (h : t.WF) {k} : + k ∈ t → t.maxKey?.isSome := + isSome_maxKey?_of_contains h + +theorem le_maxKey?_of_contains [TransOrd α] (h : t.WF) {k km} : + (hc : t.contains k) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_contains h hc) = km) → + compare k km |>.isLE := by + simp_to_model using maxKey?_le_of_containsKey + +theorem le_maxKey?_of_mem [TransOrd α] (h : t.WF) {k km} : + (hc : k ∈ t) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_mem h hc) = km) → + compare k km |>.isLE := + le_maxKey?_of_contains h + +theorem maxKey?_le [TransOrd α] {k} (h : t.WF) : + (∀ k', t.maxKey? = some k' → (compare k' k).isLE) ↔ + (∀ k', k' ∈ t → (compare k' k).isLE) := by + simp_to_model using List.maxKey?_le + +theorem getKey?_maxKey? [TransOrd α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey? km = some km := by + simp_to_model using List.getKey?_maxKey? + +theorem getKey_maxKey? [TransOrd α] (h : t.WF) {km hc} : + (hkm : t.maxKey?.get (isSome_maxKey?_of_contains h hc) = km) → t.getKey km hc = km := by + simp_to_model using List.getKey_maxKey? + +theorem getKey!_maxKey? [TransOrd α] [Inhabited α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey! km = km := by + simp_to_model using List.getKey!_maxKey? + +theorem getKeyD_maxKey? [TransOrd α] (h : t.WF) {km fallback} : + (hkm : t.maxKey? = some km) → t.getKeyD km fallback = km := by + simp_to_model using List.getKeyD_maxKey? + +@[simp] +theorem maxKey?_bind_getKey? [TransOrd α] (h : t.WF) : + t.maxKey?.bind t.getKey? = t.maxKey? := by + change (t.maxKey?.bind fun k => t.getKey? k) = t.maxKey? + simp_to_model using List.maxKey?_bind_getKey? + +theorem maxKey?_erase_eq_iff_not_compare_eq_maxKey? [TransOrd α] (h : t.WF) {k} : + (t.erase k h.balanced |>.impl.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ compare k km = .eq := by + simp_to_model [erase] using maxKey?_eraseKey_eq_iff_beq_maxKey?_eq_false + +theorem maxKey?_erase!_eq_iff_not_compare_eq_maxKey? [TransOrd α] (h : t.WF) {k} : + (t.erase! k |>.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ compare k km = .eq := by + simpa only [erase_eq_erase!] using maxKey?_erase_eq_iff_not_compare_eq_maxKey? h + +theorem maxKey?_erase_eq_of_not_compare_eq_maxKey? [TransOrd α] (h : t.WF) {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ compare k km = .eq) → + (t.erase k h.balanced |>.impl.maxKey?) = t.maxKey? := by + simp_to_model [erase] using maxKey?_eraseKey_eq_of_beq_maxKey?_eq_false + +theorem maxKey?_erase!_eq_of_not_compare_eq_maxKey? [TransOrd α] (h : t.WF) {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ compare k km = .eq) → + (t.erase! k |>.maxKey?) = t.maxKey? := by + simpa only [erase_eq_erase!] using maxKey?_erase_eq_of_not_compare_eq_maxKey? h + +theorem isSome_maxKey?_of_isSome_maxKey?_erase [TransOrd α] (h : t.WF) {k} : + (hs : t.erase k h.balanced |>.impl.maxKey?.isSome) → + t.maxKey?.isSome := by + simp_to_model [erase] using isSome_maxKey?_of_isSome_maxKey?_eraseKey + +theorem isSome_maxKey?_of_isSome_maxKey?_erase! [TransOrd α] (h : t.WF) {k} : + (hs : t.erase! k |>.maxKey?.isSome) → + t.maxKey?.isSome := by + simpa only [erase_eq_erase!] using isSome_maxKey?_of_isSome_maxKey?_erase h + +theorem maxKey?_erase_le_maxKey? [TransOrd α] (h : t.WF) {k km kme} : + (hkme : (t.erase k h.balanced |>.impl.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase h <| hkme ▸ Option.isSome_some) = km) → + compare kme km |>.isLE := by + simp_to_model [erase] using maxKey?_eraseKey_le_maxKey? + +theorem maxKey?_erase!_le_maxKey? [TransOrd α] (h : t.WF) {k km kme} : + (hkme : (t.erase! k |>.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase! h <| hkme ▸ Option.isSome_some) = km) → + compare kme km |>.isLE := by + simpa only [erase_eq_erase!] using maxKey?_erase_le_maxKey? h + +theorem maxKey?_insertIfNew [TransOrd α] (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 [insertIfNew] using List.maxKey?_insertEntryIfNew + +theorem maxKey?_insertIfNew! [TransOrd α] (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 isSome_maxKey?_insertIfNew [TransOrd α] (h : t.WF) {k v} : + (t.insertIfNew k v h.balanced).impl.maxKey?.isSome := by + simp_to_model [insertIfNew] using List.isSome_maxKey?_insertEntryIfNew + +theorem isSome_maxKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v} : + (t.insertIfNew! k v).maxKey?.isSome := by + simpa only [insertIfNew_eq_insertIfNew!] using isSome_maxKey?_insertIfNew h + +theorem maxKey?_le_maxKey?_insertIfNew [TransOrd α] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew k v h.balanced |>.impl.maxKey? |>.get <| isSome_maxKey?_insertIfNew h) = kmi) → + compare km kmi |>.isLE := by + simp_to_model [insertIfNew] using List.maxKey?_le_maxKey?_insertEntryIfNew + +theorem maxKey?_le_maxKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew! k v |>.maxKey? |>.get <| isSome_maxKey?_insertIfNew! h) = kmi) → + compare km kmi |>.isLE := by + simpa only [insertIfNew_eq_insertIfNew!] using maxKey?_le_maxKey?_insertIfNew h + +theorem self_le_maxKey?_insertIfNew [TransOrd α] (h : t.WF) {k v kmi} : + (hkmi : (t.insertIfNew k v h.balanced |>.impl.maxKey?.get <| isSome_maxKey?_insertIfNew h) = kmi) → + compare k kmi |>.isLE := by + simp_to_model [insertIfNew] using List.self_le_maxKey?_insertEntryIfNew + +theorem self_le_maxKey?_insertIfNew! [TransOrd α] (h : t.WF) {k v kmi} : + (hkmi : (t.insertIfNew! k v |>.maxKey?.get <| isSome_maxKey?_insertIfNew! h) = kmi) → + compare k kmi |>.isLE := by + simpa only [insertIfNew_eq_insertIfNew!] using self_le_maxKey?_insertIfNew h + +theorem maxKey?_eq_getLast?_keys [TransOrd α] (h : t.WF) : + t.maxKey? = t.keys.getLast? := by + simp_to_model [maxKey?, keys] using List.maxKey?_eq_getLast?_keys _ h.ordered + +theorem maxKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) : + (t.modify k f).maxKey? = t.maxKey? := by + simp_to_model [modify] using List.maxKey?_modifyKey + +theorem maxKey?_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} : + (t.alter k f h.balanced).impl.maxKey? = some k ↔ + (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by + simp_to_model [alter] using List.maxKey?_alterKey_eq_self + +theorem maxKey?_alter!_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} : + (t.alter! k f).maxKey? = some 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 α] (h : t.WF) {k f} : + (Const.modify k f t).maxKey? = t.maxKey?.map fun km => if compare km k = .eq then k else km := by + simp_to_model [Const.modify] using List.Const.maxKey?_modifyKey + +theorem maxKey?_modify_eq_maxKey? [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f} : + (Const.modify k f t).maxKey? = t.maxKey? := by + simp_to_model [Const.modify] using List.Const.maxKey?_modifyKey_eq_maxKey? + +theorem isSome_maxKey?_modify [TransOrd α] {k f} (h : t.WF) : + (Const.modify k f t).maxKey?.isSome = !t.isEmpty := by + simp_to_model [Const.modify] using List.Const.isSome_maxKey?_modifyKey + +theorem isSome_maxKey?_modify_eq_isSome [TransOrd α] (h : t.WF) {k f} : + (Const.modify k f t).maxKey?.isSome = t.maxKey?.isSome := by + simp_to_model [Const.modify] using List.Const.isSome_maxKey?_modifyKey_eq_isSome + +theorem compare_maxKey?_modify_eq [TransOrd α] (h : t.WF) {k f km kmm} : + (hkm : t.maxKey? = some km) → + (hkmm : (Const.modify k f t |>.maxKey? |>.get <| + (isSome_maxKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) → + compare kmm km = .eq := by + simp_to_model [Const.modify] using List.Const.maxKey?_modifyKey_beq + +theorem maxKey?_alter_eq_self [TransOrd α] (h : t.WF) {k f} : + (Const.alter k f t h.balanced).impl.maxKey? = some k ↔ + (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by + simp_to_model [Const.alter] using List.Const.maxKey?_alterKey_eq_self + +theorem maxKey?_alter!_eq_self [TransOrd α] (h : t.WF) {k f} : + (Const.alter! k f t).maxKey? = some k ↔ + (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k' k).isLE := by + simpa [alter_eq_alter!] using maxKey?_alter_eq_self h + +end Const + +end Max + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean index 7b2c30495a..dc68f07e1e 100644 --- a/src/Std/Data/DTreeMap/Internal/Model.lean +++ b/src/Std/Data/DTreeMap/Internal/Model.lean @@ -272,6 +272,11 @@ def minEntry?ₘ' [Ord α] (l : Impl α β) : Option ((a : α) × β a) := def minEntry?ₘ [Ord α] (l : Impl α β) : Option ((a : α) × β a) := applyPartition (fun (_ : α) => .lt) l fun _ _ _ r => r.head? +/-- Internal implementation detail of the tree map -/ +def reverse : Impl α β → Impl α β + | .leaf => .leaf + | .inner sz k v l r => .inner sz k v (reverse r) (reverse l) + /-- Model implementation of the `insert` function. Internal implementation detail of the tree map @@ -484,6 +489,10 @@ theorem minKeyD_eq_getD_minKey? [Ord α] {l : Impl α β} {fallback} : l.minKeyD fallback = l.minKey?.getD fallback := by induction l, fallback using minKeyD.induct <;> simp_all only [minKeyD, minKey?] <;> rfl +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 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/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean index 1f3bd63744..48ab5fdb1e 100644 --- a/src/Std/Data/DTreeMap/Internal/Queries.lean +++ b/src/Std/Data/DTreeMap/Internal/Queries.lean @@ -277,93 +277,93 @@ variable {β : Type v} end Const /-- Implementation detail of the tree map -/ -def minEntry? [Ord α] : Impl α β → Option ((a : α) × β a) +def minEntry? : Impl α β → Option ((a : α) × β a) | .leaf => none | .inner _ k v .leaf _ => some ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _ => l.minEntry? /-- Implementation detail of the tree map -/ -def minEntry [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → (a : α) × β a +def minEntry : (t : Impl α β) → (h : t.isEmpty = false) → (a : α) × β a | .inner _ k v .leaf _, _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _, h => l.minEntry (by simp_all [isEmpty]) /-- Implementation detail of the tree map -/ -def minEntry! [Ord α] [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a +def minEntry! [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a | .leaf => panic! "Map is empty" | .inner _ k v .leaf _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _ => l.minEntry! /-- Implementation detail of the tree map -/ -def minEntryD [Ord α] : Impl α β → (a : α) × β a → (a : α) × β a +def minEntryD : Impl α β → (a : α) × β a → (a : α) × β a | .leaf, fallback => fallback | .inner _ k v .leaf _, _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _, fallback => l.minEntryD fallback /-- Implementation detail of the tree map -/ -def maxEntry? [Ord α] : Impl α β → Option ((a : α) × β a) +def maxEntry? : Impl α β → Option ((a : α) × β a) | .leaf => none | .inner _ k v _ .leaf => some ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..) => r.maxEntry? /-- Implementation detail of the tree map -/ -def maxEntry [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → (a : α) × β a +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]) /-- Implementation detail of the tree map -/ -def maxEntry! [Ord α] [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a +def maxEntry! [Inhabited ((a : α) × β a)] : Impl α β → (a : α) × β a | .leaf => panic! "Map is empty" | .inner _ k v _ .leaf => ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..) => r.maxEntry! /-- Implementation detail of the tree map -/ -def maxEntryD [Ord α] : Impl α β → (a : α) × β a → (a : α) × β a +def maxEntryD : Impl α β → (a : α) × β a → (a : α) × β a | .leaf, fallback => fallback | .inner _ k v _ .leaf, _ => ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..), fallback => r.maxEntryD fallback /-- Implementation detail of the tree map -/ -def minKey? [Ord α] : Impl α β → Option α +def minKey? : Impl α β → Option α | .leaf => none | .inner _ k _ .leaf _ => some k | .inner _ _ _ l@(inner ..) _ => l.minKey? /-- Implementation detail of the tree map -/ -def minKey [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → α +def minKey : (t : Impl α β) → (h : t.isEmpty = false) → α | .inner _ k _ .leaf _, _ => k | .inner _ _ _ l@(.inner ..) _, h => l.minKey (by simp_all [isEmpty]) /-- The smallest key of `t`. Returns the given fallback value if the map is empty. -/ -def minKey! [Ord α] [Inhabited α] : Impl α β → α +def minKey! [Inhabited α] : Impl α β → α | .leaf => panic! "Map is empty" | .inner _ k _ .leaf _ => k | .inner _ _ _ l@(.inner ..) _ => l.minKey! /-- Implementation detail of the tree map -/ -def minKeyD [Ord α] : Impl α β → α → α +def minKeyD : Impl α β → α → α | .leaf, fallback => fallback | .inner _ k _ .leaf _, _ => k | .inner _ _ _ l@(.inner ..) _, fallback => l.minKeyD fallback /-- Implementation detail of the tree map -/ -def maxKey? [Ord α] : Impl α β → Option α +def maxKey? : Impl α β → Option α | .leaf => none | .inner _ k _ _ .leaf => some k | .inner _ _ _ _ r@(.inner ..) => r.maxKey? /-- Implementation detail of the tree map -/ -def maxKey [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → α +def maxKey : (t : Impl α β) → (h : t.isEmpty = false) → α | .inner _ k _ .leaf _, _ => k | .inner _ _ _ l@(.inner ..) _, h => l.maxKey (by simp_all [isEmpty]) /-- Implementation detail of the tree map -/ -def maxKey! [Ord α] [Inhabited α] : Impl α β → α +def maxKey! [Inhabited α] : Impl α β → α | .leaf => panic! "Map is empty" | .inner _ k _ _ .leaf => k | .inner _ _ _ _ r@(.inner ..) => r.maxKey! /-- Implementation detail of the tree map -/ -def maxKeyD [Ord α] : Impl α β → α → α +def maxKeyD : Impl α β → α → α | .leaf, fallback => fallback | .inner _ k _ _ .leaf, _ => k | .inner _ _ _ _ r@(.inner ..), fallback => r.maxKeyD fallback @@ -371,7 +371,7 @@ def maxKeyD [Ord α] : Impl α β → α → α attribute [Std.Internal.tree_tac] Nat.compare_eq_gt Nat.compare_eq_lt Nat.compare_eq_eq /-- Implementation detail of the tree map -/ -def entryAtIdx [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → (a : α) × β a +def entryAtIdx : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → (a : α) × β a | .inner _ k v l' r', hl, n, h => match h : compare n l'.size with | .lt => l'.entryAtIdx hl.left n (by simpa only [Std.Internal.tree_tac] using h) @@ -379,7 +379,7 @@ def entryAtIdx [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) | .gt => r'.entryAtIdx hl.right (n - l'.size - 1) (by simp_all only [Std.Internal.tree_tac]; omega) /-- Implementation detail of the tree map -/ -def entryAtIdx? [Ord α] : Impl α β → Nat → Option ((a : α) × β a) +def entryAtIdx? : Impl α β → Nat → Option ((a : α) × β a) | .leaf, _ => none | .inner _ k v l r, n => match compare n l.size with @@ -388,7 +388,7 @@ def entryAtIdx? [Ord α] : Impl α β → Nat → Option ((a : α) × β a) | .gt => r.entryAtIdx? (n - l.size - 1) /-- Implementation detail of the tree map -/ -def entryAtIdx! [Ord α] [Inhabited ((a : α) × β a)] : Impl α β → Nat → (a : α) × β a +def entryAtIdx! [Inhabited ((a : α) × β a)] : Impl α β → Nat → (a : α) × β a | .leaf, _ => panic! "Out-of-bounds access" | .inner _ k v l r, n => match compare n l.size with @@ -397,7 +397,7 @@ def entryAtIdx! [Ord α] [Inhabited ((a : α) × β a)] : Impl α β → Nat → | .gt => r.entryAtIdx! (n - l.size - 1) /-- Implementation detail of the tree map -/ -def entryAtIdxD [Ord α] : Impl α β → Nat → (a : α) × β a → (a : α) × β a +def entryAtIdxD : Impl α β → Nat → (a : α) × β a → (a : α) × β a | .leaf, _, fallback => fallback | .inner _ k v l r, n, fallback => match compare n l.size with @@ -406,7 +406,7 @@ def entryAtIdxD [Ord α] : Impl α β → Nat → (a : α) × β a → (a : α) | .gt => r.entryAtIdxD (n - l.size - 1) fallback /-- Implementation detail of the tree map -/ -def keyAtIndex [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α +def keyAtIndex : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α | .inner _ k _ l' r', hl, n, h => match h : compare n l'.size with | .lt => keyAtIndex l' hl.left n (by simpa only [Std.Internal.tree_tac] using h) @@ -415,7 +415,7 @@ def keyAtIndex [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) keyAtIndex r' hl.right (n - l'.size - 1) (by simp_all only [Std.Internal.tree_tac]; omega) /-- Implementation detail of the tree map -/ -def keyAtIndex? [Ord α] : Impl α β → Nat → Option α +def keyAtIndex? : Impl α β → Nat → Option α | .leaf, _ => none | .inner _ k _ l r, n => match compare n l.size with @@ -424,7 +424,7 @@ def keyAtIndex? [Ord α] : Impl α β → Nat → Option α | .gt => keyAtIndex? r (n - l.size - 1) /-- Implementation detail of the tree map -/ -def keyAtIndex! [Ord α] [Inhabited α] : Impl α β → Nat → α +def keyAtIndex! [Inhabited α] : Impl α β → Nat → α | .leaf, _ => panic! "Out-of-bounds access" | .inner _ k _ l r, n => match compare n l.size with @@ -433,7 +433,7 @@ def keyAtIndex! [Ord α] [Inhabited α] : Impl α β → Nat → α | .gt => keyAtIndex! r (n - l.size - 1) /-- Implementation detail of the tree map -/ -def keyAtIndexD [Ord α] : Impl α β → Nat → α → α +def keyAtIndexD : Impl α β → Nat → α → α | .leaf, _, fallback => fallback | .inner _ k _ l r, n, fallback => match compare n l.size with @@ -726,54 +726,54 @@ namespace Const variable {β : Type v} /-- Implementation detail of the tree map -/ -def minEntry? [Ord α] : Impl α β → Option (α × β) +def minEntry? : Impl α β → Option (α × β) | .leaf => none | .inner _ k v .leaf _ => some ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _ => minEntry? l /-- Implementation detail of the tree map -/ -def minEntry [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → α × β +def minEntry : (t : Impl α β) → (h : t.isEmpty = false) → α × β | .inner _ k v .leaf _, _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _, h => minEntry l (by simp_all [isEmpty]) /-- Implementation detail of the tree map -/ -def minEntry! [Ord α] [Inhabited (α × β)] : Impl α β → α × β +def minEntry! [Inhabited (α × β)] : Impl α β → α × β | .leaf => panic! "Map is empty" | .inner _ k v .leaf _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _ => minEntry! l /-- Implementation detail of the tree map -/ -def minEntryD [Ord α] : Impl α β → α × β → α × β +def minEntryD : Impl α β → α × β → α × β | .leaf, fallback => fallback | .inner _ k v .leaf _, _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _, fallback => minEntryD l fallback /-- Implementation detail of the tree map -/ -def maxEntry? [Ord α] : Impl α β → Option (α × β) +def maxEntry? : Impl α β → Option (α × β) | .leaf => none | .inner _ k v _ .leaf => some ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..) => maxEntry? r /-- Implementation detail of the tree map -/ -def maxEntry [Ord α] : (t : Impl α β) → (h : t.isEmpty = false) → α × β +def maxEntry : (t : Impl α β) → (h : t.isEmpty = false) → α × β | .inner _ k v .leaf _, _ => ⟨k, v⟩ | .inner _ _ _ l@(.inner ..) _, h => maxEntry l (by simp_all [isEmpty]) /-- Implementation detail of the tree map -/ -def maxEntry! [Ord α] [Inhabited (α × β)] : Impl α β → α × β +def maxEntry! [Inhabited (α × β)] : Impl α β → α × β | .leaf => panic! "Map is empty" | .inner _ k v _ .leaf => ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..) => maxEntry! r /-- Implementation detail of the tree map -/ -def maxEntryD [Ord α] : Impl α β → α × β → α × β +def maxEntryD : Impl α β → α × β → α × β | .leaf, fallback => fallback | .inner _ k v _ .leaf, _ => ⟨k, v⟩ | .inner _ _ _ _ r@(.inner ..), fallback => maxEntryD r fallback /-- Implementation detail of the tree map -/ @[inline] -def entryAtIdx [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α × β +def entryAtIdx : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) → (h : n < t.size) → α × β | .inner _ k v l' r', hl, n, h => match h : compare n l'.size with | .lt => entryAtIdx l' hl.left n (by simpa only [Std.Internal.tree_tac] using h) @@ -782,7 +782,7 @@ def entryAtIdx [Ord α] : (t : Impl α β) → (hl : t.Balanced) → (n : Nat) entryAtIdx r' hl.right (n - l'.size - 1) (by simp_all only [Std.Internal.tree_tac]; omega) /-- Implementation detail of the tree map -/ -def entryAtIdx? [Ord α] : Impl α β → Nat → Option (α × β) +def entryAtIdx? : Impl α β → Nat → Option (α × β) | .leaf, _ => none | .inner _ k v l r, n => match compare n l.size with @@ -791,7 +791,7 @@ def entryAtIdx? [Ord α] : Impl α β → Nat → Option (α × β) | .gt => entryAtIdx? r (n - l.size - 1) /-- Implementation detail of the tree map -/ -def entryAtIdx! [Ord α] [Inhabited (α × β)] : Impl α β → Nat → α × β +def entryAtIdx! [Inhabited (α × β)] : Impl α β → Nat → α × β | .leaf, _ => panic! "Out-of-bounds access" | .inner _ k v l r, n => match compare n l.size with @@ -800,7 +800,7 @@ def entryAtIdx! [Ord α] [Inhabited (α × β)] : Impl α β → Nat → α × | .gt => entryAtIdx! r (n - l.size - 1) /-- Implementation detail of the tree map -/ -def entryAtIdxD [Ord α] : Impl α β → Nat → α × β → α × β +def entryAtIdxD : Impl α β → Nat → α × β → α × β | .leaf, _, fallback => fallback | .inner _ k v l r, n, fallback => match compare n l.size with diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index ced33037cd..049d0ac06c 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1824,7 +1824,7 @@ theorem minEntry?_eq_minEntry? [Ord α] [TransOrd α] {l : Impl α β} (hlo : l. l.minEntry? = List.minEntry? l.toListModel := by rw [minEntry?_eq_minEntry?ₘ, minEntry?ₘ_eq_minEntry? hlo] -theorem minKey?_eq_minKey? [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : +theorem minKey?_eq_minKey? {_ : Ord α} [TransOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey? = List.minKey? l.toListModel := by simp only [minKey?_eq_minEntry?_map_fst, minEntry?_eq_minEntry? hlo, List.minKey?] @@ -1842,4 +1842,18 @@ theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Orde l.minKeyD fallback = List.minKeyD l.toListModel fallback := by simp [Impl.minKeyD_eq_getD_minKey?, List.minKeyD_eq_getD_minKey?, minKey?_eq_minKey? hlo] +theorem toListModel_reverse {l : Impl α β} : + (reverse l).toListModel = l.toListModel.reverse := by + induction l <;> simp_all [reverse] + +theorem Ordered.reverse [Ord α] {t : Impl α β} (h : t.Ordered) : + letI : Ord α := .opposite inferInstance; t.reverse.Ordered := by + simp only [Ordered, toListModel_reverse] + exact List.pairwise_reverse.mpr h + +theorem maxKey?_eq_maxKey? [Ord α] [TransOrd α] {t : Impl α β} (hlo : t.Ordered) : + t.maxKey? = List.maxKey? t.toListModel := by + 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] + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 4e08ebaee9..df5e17b1b5 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -2828,7 +2828,7 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] : theorem minKey?_insert [TransCmp cmp] {k v} : (t.insert k v).minKey? = - some (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := Impl.minKey?_insert t.wf theorem isSome_minKey?_insert [TransCmp cmp] {k v} : @@ -3009,7 +3009,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he k theorem minKey_insert [TransCmp cmp] {k v} : (t.insert k v).minKey isEmpty_insert = - t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k' := + t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k' := Impl.minKey_insert t.wf theorem minKey_insert_le_minKey [TransCmp cmp] {k v he} : @@ -3156,7 +3156,7 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh theorem minKey!_insert [TransCmp cmp] [Inhabited α] {k v} : (t.insert k v |>.minKey!) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (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} : @@ -3296,7 +3296,7 @@ theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] theorem minKeyD_insert [TransCmp cmp] {k v fallback} : (t.insert k v |>.minKeyD fallback) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := Impl.minKeyD_insert t.wf theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (he : t.isEmpty = false) @@ -3412,4 +3412,209 @@ end Const end Min +section Max + +@[simp] +theorem maxKey?_emptyc : + (∅ : DTreeMap α β cmp).maxKey? = none := + Impl.maxKey?_empty + +theorem maxKey?_of_isEmpty [TransCmp cmp] : + (he : t.isEmpty) → t.maxKey? = none := + Impl.maxKey?_of_isEmpty t.wf + +@[simp] +theorem maxKey?_eq_none_iff [TransCmp cmp] : + t.maxKey? = none ↔ t.isEmpty := + Impl.maxKey?_eq_none_iff t.wf + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} : + t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + Impl.maxKey?_eq_some_iff_getKey?_eq_self_and_forall t.wf + +theorem maxKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} : + t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + Impl.maxKey?_eq_some_iff_mem_and_forall t.wf + +@[simp] +theorem isNone_maxKey?_eq_isEmpty [TransCmp cmp] : + t.maxKey?.isNone = t.isEmpty := + Impl.isNone_maxKey?_eq_isEmpty t.wf + +@[simp] +theorem isSome_maxKey?_eq_not_isEmpty [TransCmp cmp] : + t.maxKey?.isSome = !t.isEmpty := + Impl.isSome_maxKey?_eq_not_isEmpty t.wf + +theorem isSome_maxKey?_iff_isEmpty_eq_false [TransCmp cmp] : + t.maxKey?.isSome ↔ t.isEmpty = false := + Impl.isSome_maxKey?_iff_isEmpty_eq_false t.wf + +theorem maxKey?_insert [TransCmp cmp] {k v} : + (t.insert k v).maxKey? = + some (t.maxKey?.elim k fun k' => if cmp k' k|>.isLE then k else k') := + Impl.maxKey?_insert t.wf + +theorem isSome_maxKey?_insert [TransCmp cmp] {k v} : + (t.insert k v).maxKey?.isSome := + Impl.isSome_maxKey?_insert t.wf + +theorem maxKey?_le_maxKey?_insert [TransCmp cmp] {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert k v |>.maxKey? |>.get isSome_maxKey?_insert) = kmi) → + cmp km kmi |>.isLE := + Impl.maxKey?_le_maxKey?_insert t.wf + +theorem self_le_maxKey?_insert [TransCmp cmp] {k v kmi} : + (hkmi : (t.insert k v |>.maxKey?.get isSome_maxKey?_insert) = kmi) → + cmp k kmi |>.isLE := + Impl.self_le_maxKey?_insert t.wf + +theorem contains_maxKey? [TransCmp cmp] {km} : + (hkm : t.maxKey? = some km) → + t.contains km := + Impl.contains_maxKey? t.wf + +theorem maxKey?_mem [TransCmp cmp] {km} : + (hkm : t.maxKey? = some km) → + km ∈ t:= + Impl.maxKey?_mem t.wf + +theorem isSome_maxKey?_of_contains [TransCmp cmp] {k} : + (hc : t.contains k) → t.maxKey?.isSome := + Impl.isSome_maxKey?_of_contains t.wf + +theorem isSome_maxKey?_of_mem [TransCmp cmp] {k} : + k ∈ t → t.maxKey?.isSome := + Impl.isSome_maxKey?_of_mem t.wf + +theorem le_maxKey?_of_contains [TransCmp cmp] {k km} : + (hc : t.contains k) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_contains hc) = km) → + cmp k km |>.isLE := + Impl.le_maxKey?_of_contains t.wf + +theorem le_maxKey?_of_mem [TransCmp cmp] {k km} : + (hc : k ∈ t) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_mem hc) = km) → + cmp k km |>.isLE := + Impl.le_maxKey?_of_mem t.wf + +theorem maxKey?_le [TransCmp cmp] {k} : + (∀ k', t.maxKey? = some k' → (cmp k' k).isLE) ↔ + (∀ k', k' ∈ t → (cmp k' k).isLE) := + Impl.maxKey?_le t.wf + +theorem getKey?_maxKey? [TransCmp cmp] {km} : + (hkm : t.maxKey? = some km) → t.getKey? km = some km := + Impl.getKey?_maxKey? t.wf + +theorem getKey_maxKey? [TransCmp cmp] {km hc} : + (hkm : t.maxKey?.get (isSome_maxKey?_of_contains hc) = km) → t.getKey km hc = km := + Impl.getKey_maxKey? t.wf + +theorem getKey!_maxKey? [TransCmp cmp] [Inhabited α] {km} : + (hkm : t.maxKey? = some km) → t.getKey! km = km := + Impl.getKey!_maxKey? t.wf + +theorem getKeyD_maxKey? [TransCmp cmp] {km fallback} : + (hkm : t.maxKey? = some km) → t.getKeyD km fallback = km := + Impl.getKeyD_maxKey? t.wf + +@[simp] +theorem maxKey?_bind_getKey? [TransCmp cmp] : + t.maxKey?.bind t.getKey? = t.maxKey? := + Impl.maxKey?_bind_getKey? t.wf + +theorem maxKey?_erase_eq_iff_not_compare_eq_maxKey? [TransCmp cmp] {k} : + (t.erase k |>.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq := + Impl.maxKey?_erase_eq_iff_not_compare_eq_maxKey? t.wf + +theorem maxKey?_erase_eq_of_not_compare_eq_maxKey? [TransCmp cmp] {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.maxKey?) = t.maxKey? := + Impl.maxKey?_erase_eq_of_not_compare_eq_maxKey? t.wf + +theorem isSome_maxKey?_of_isSome_maxKey?_erase [TransCmp cmp] {k} : + (hs : t.erase k |>.maxKey?.isSome) → + t.maxKey?.isSome := + Impl.isSome_maxKey?_of_isSome_maxKey?_erase t.wf + +theorem maxKey?_erase_le_maxKey? [TransCmp cmp] {k km kme} : + (hkme : (t.erase k |>.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + Impl.maxKey?_erase_le_maxKey? t.wf + +theorem maxKey?_insertIfNew [TransCmp cmp] {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 isSome_maxKey?_insertIfNew [TransCmp cmp] {k v} : + (t.insertIfNew k v).maxKey?.isSome := + Impl.isSome_maxKey?_insertIfNew t.wf + +theorem maxKey?_le_maxKey?_insertIfNew [TransCmp cmp] {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew k v |>.maxKey? |>.get isSome_maxKey?_insertIfNew) = kmi) → + cmp km kmi |>.isLE := + Impl.maxKey?_le_maxKey?_insertIfNew t.wf + +theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} : + (hkmi : (t.insertIfNew k v |>.maxKey?.get isSome_maxKey?_insertIfNew) = kmi) → + cmp k kmi |>.isLE := + Impl.self_le_maxKey?_insertIfNew t.wf + +theorem maxKey?_eq_getLast?_keys [TransCmp cmp] : + t.maxKey? = t.keys.getLast? := + Impl.maxKey?_eq_getLast?_keys t.wf + +@[simp] +theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} : + (t.modify k f).maxKey? = t.maxKey? := + Impl.maxKey?_modify t.wf + +theorem maxKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f} : + (t.alter k f).maxKey? = some 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} : + (Const.modify t k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := + Impl.Const.maxKey?_modify t.wf + +@[simp] +theorem maxKey?_modify_eq_maxKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} : + (Const.modify t k f).maxKey? = t.maxKey? := + Impl.Const.maxKey?_modify_eq_maxKey? t.wf + +theorem isSome_maxKey?_modify [TransCmp cmp] {k f} : + (Const.modify t k f).maxKey?.isSome = !t.isEmpty := + Impl.Const.isSome_maxKey?_modify t.wf + +theorem isSome_maxKey?_modify_eq_isSome [TransCmp cmp] {k f} : + (Const.modify t k f).maxKey?.isSome = t.maxKey?.isSome := + Impl.Const.isSome_maxKey?_modify_eq_isSome t.wf + +theorem compare_maxKey?_modify_eq [TransCmp cmp] {k f km kmm} : + (hkm : t.maxKey? = some km) → + (hkmm : (Const.modify t k f |>.maxKey? |>.get <| + isSome_maxKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) → + cmp kmm km = .eq := + Impl.Const.compare_maxKey?_modify_eq t.wf + +theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} : + (Const.alter t k f).maxKey? = some k ↔ + (f (Const.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 diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 03cb990c11..c7bfad4ae6 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -2802,12 +2802,12 @@ theorem minKey?_emptyc : theorem minKey?_of_isEmpty [TransCmp cmp] (h : t.WF) : (he : t.isEmpty) → t.minKey? = none := - Impl.minKey?_of_isEmpty h + Impl.minKey?_of_isEmpty h (instOrd := ⟨cmp⟩) @[simp] theorem minKey?_eq_none_iff [TransCmp cmp] (h : t.WF) : t.minKey? = none ↔ t.isEmpty := - Impl.minKey?_eq_none_iff h + Impl.minKey?_eq_none_iff h (instOrd := ⟨cmp⟩) theorem minKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} : t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE := @@ -2820,20 +2820,20 @@ theorem minKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : @[simp] theorem isNone_minKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) : t.minKey?.isNone = t.isEmpty := - Impl.isNone_minKey?_eq_isEmpty h + Impl.isNone_minKey?_eq_isEmpty h (instOrd := ⟨cmp⟩) @[simp] theorem isSome_minKey?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) : t.minKey?.isSome = !t.isEmpty := - Impl.isSome_minKey?_eq_not_isEmpty h + Impl.isSome_minKey?_eq_not_isEmpty h (instOrd := ⟨cmp⟩) theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] (h : t.WF) : t.minKey?.isSome ↔ t.isEmpty = false := - Impl.isSome_minKey?_iff_isEmpty_eq_false h + Impl.isSome_minKey?_iff_isEmpty_eq_false h (instOrd := ⟨cmp⟩) theorem minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : (t.insert k v).minKey? = - some (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := Impl.minKey?_insert! h theorem isSome_minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : @@ -2882,7 +2882,7 @@ theorem minKey?_le_of_mem [TransCmp cmp] (h : t.WF) {k km} : theorem le_minKey? [TransCmp cmp] {k} (h : t.WF) : (∀ k', t.minKey? = some k' → (cmp k k').isLE) ↔ (∀ k', k' ∈ t → (cmp k k').isLE) := - Impl.le_minKey? h + Impl.le_minKey? h (instOrd := ⟨cmp⟩) theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} : (hkm : t.minKey? = some km) → t.getKey? km = some km := @@ -2913,7 +2913,7 @@ theorem minKey?_erase_eq_iff_not_compare_eq_minKey? [TransCmp cmp] (h : t.WF) {k theorem minKey?_erase_eq_of_not_compare_eq_minKey? [TransCmp cmp] (h : t.WF) {k} : (hc : ∀ {km}, t.minKey? = some km → ¬ cmp k km = .eq) → (t.erase k |>.minKey?) = t.minKey? := - Impl.minKey?_erase!_eq_of_not_compare_eq_minKey? h + Impl.minKey?_erase!_eq_of_not_compare_eq_minKey? h (instOrd := ⟨cmp⟩) theorem isSome_minKey?_of_isSome_minKey?_erase [TransCmp cmp] (h : t.WF) {k} : (hs : t.erase k |>.minKey?.isSome) → @@ -2949,7 +2949,7 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} : theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) : t.minKey? = t.keys.head? := - Impl.minKey?_eq_head?_keys h + Impl.minKey?_eq_head?_keys h (instOrd := ⟨cmp⟩) @[simp] theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) : @@ -2998,11 +2998,11 @@ end Const theorem minKey?_eq_some_minKey! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.minKey? = some t.minKey! := - Impl.minKey?_eq_some_minKey! h he + Impl.minKey?_eq_some_minKey! h he (instOrd := ⟨cmp⟩) theorem minKey!_eq_default [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty) : t.minKey! = default := - Impl.minKey!_eq_default h he + Impl.minKey!_eq_default h he (instOrd := ⟨cmp⟩) theorem minKey!_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {km} : @@ -3016,7 +3016,7 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh theorem minKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} : (t.insert k v |>.minKey!) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (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) @@ -3090,7 +3090,7 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) : t.minKey! = t.keys.head! := - Impl.minKey!_eq_head!_keys h + Impl.minKey!_eq_head!_keys h (instOrd := ⟨cmp⟩) @[simp] theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} : @@ -3131,15 +3131,15 @@ end Const theorem minKey?_eq_some_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} : t.minKey? = some (t.minKeyD fallback) := - Impl.minKey?_eq_some_minKeyD h he + Impl.minKey?_eq_some_minKeyD h he (instOrd := ⟨cmp⟩) theorem minKeyD_eq_fallback [TransCmp cmp] (h : t.WF) (he : t.isEmpty) {fallback} : t.minKeyD fallback = fallback := - Impl.minKeyD_eq_fallback h he + Impl.minKeyD_eq_fallback h he (instOrd := ⟨cmp⟩) theorem minKey!_eq_minKeyD_default [TransCmp cmp] [Inhabited α] (h : t.WF) : t.minKey! = t.minKeyD default := - Impl.minKey!_eq_minKeyD_default h + Impl.minKey!_eq_minKeyD_default h (instOrd := ⟨cmp⟩) theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {km fallback} : @@ -3153,7 +3153,7 @@ theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : theorem minKeyD_insert [TransCmp cmp] (h : t.WF) {k v fallback} : (t.insert k v |>.minKeyD fallback) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := Impl.minKeyD_insert! h theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) @@ -3227,7 +3227,7 @@ theorem minKeyD_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v fallback} : theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} : t.minKeyD fallback = t.keys.headD fallback := - Impl.minKeyD_eq_headD_keys h + Impl.minKeyD_eq_headD_keys h (instOrd := ⟨cmp⟩) @[simp] theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} : @@ -3269,4 +3269,209 @@ end Const end Min +section Max + +@[simp] +theorem maxKey?_emptyc : + (∅ : Raw α β cmp).maxKey? = none := + Impl.maxKey?_empty + +theorem maxKey?_of_isEmpty [TransCmp cmp] (h : t.WF) : + (he : t.isEmpty) → t.maxKey? = none := + Impl.maxKey?_of_isEmpty h (instOrd := ⟨cmp⟩) + +@[simp] +theorem maxKey?_eq_none_iff [TransCmp cmp] (h : t.WF) : + t.maxKey? = none ↔ t.isEmpty := + Impl.maxKey?_eq_none_iff h (instOrd := ⟨cmp⟩) + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} : + t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + Impl.maxKey?_eq_some_iff_getKey?_eq_self_and_forall h + +theorem maxKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} : + t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + Impl.maxKey?_eq_some_iff_mem_and_forall h + +@[simp] +theorem isNone_maxKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) : + t.maxKey?.isNone = t.isEmpty := + Impl.isNone_maxKey?_eq_isEmpty h (instOrd := ⟨cmp⟩) + +@[simp] +theorem isSome_maxKey?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) : + t.maxKey?.isSome = !t.isEmpty := + Impl.isSome_maxKey?_eq_not_isEmpty h (instOrd := ⟨cmp⟩) + +theorem isSome_maxKey?_iff_isEmpty_eq_false [TransCmp cmp] (h : t.WF) : + t.maxKey?.isSome ↔ t.isEmpty = false := + Impl.isSome_maxKey?_iff_isEmpty_eq_false h (instOrd := ⟨cmp⟩) + +theorem maxKey?_insert [TransCmp cmp] (h : t.WF) {k v} : + (t.insert k v).maxKey? = + some (t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') := + Impl.maxKey?_insert! h + +theorem isSome_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v} : + (t.insert k v).maxKey?.isSome := + Impl.isSome_maxKey?_insert! h + +theorem maxKey?_le_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert k v |>.maxKey? |>.get <| isSome_maxKey?_insert h) = kmi) → + cmp km kmi |>.isLE := + Impl.maxKey?_le_maxKey?_insert! h + +theorem self_le_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v kmi} : + (hkmi : (t.insert k v |>.maxKey?.get <| isSome_maxKey?_insert h) = kmi) → + cmp k kmi |>.isLE := + Impl.self_le_maxKey?_insert! h + +theorem contains_maxKey? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → + t.contains km := + Impl.contains_maxKey? h + +theorem maxKey?_mem [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → + km ∈ t:= + Impl.maxKey?_mem h + +theorem isSome_maxKey?_of_contains [TransCmp cmp] (h : t.WF) {k} : + (hc : t.contains k) → t.maxKey?.isSome := + Impl.isSome_maxKey?_of_contains h + +theorem isSome_maxKey?_of_mem [TransCmp cmp] (h : t.WF) {k} : + k ∈ t → t.maxKey?.isSome := + Impl.isSome_maxKey?_of_mem h + +theorem le_maxKey?_of_contains [TransCmp cmp] (h : t.WF) {k km} : + (hc : t.contains k) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_contains h hc) = km) → + cmp k km |>.isLE := + Impl.le_maxKey?_of_contains h + +theorem le_maxKey?_of_mem [TransCmp cmp] (h : t.WF) {k km} : + (hc : k ∈ t) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_mem h hc) = km) → + cmp k km |>.isLE := + Impl.le_maxKey?_of_mem h + +theorem maxKey?_le [TransCmp cmp] {k} (h : t.WF) : + (∀ k', t.maxKey? = some k' → (cmp k' k).isLE) ↔ + (∀ k', k' ∈ t → (cmp k' k).isLE) := + Impl.maxKey?_le h (instOrd := ⟨cmp⟩) + +theorem getKey?_maxKey? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey? km = some km := + Impl.getKey?_maxKey? h + +theorem getKey_maxKey? [TransCmp cmp] (h : t.WF) {km hc} : + (hkm : t.maxKey?.get (isSome_maxKey?_of_contains h hc) = km) → t.getKey km hc = km := + Impl.getKey_maxKey? h + +theorem getKey!_maxKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey! km = km := + Impl.getKey!_maxKey? h + +theorem getKeyD_maxKey? [TransCmp cmp] (h : t.WF) {km fallback} : + (hkm : t.maxKey? = some km) → t.getKeyD km fallback = km := + Impl.getKeyD_maxKey? h + +@[simp] +theorem maxKey?_bind_getKey? [TransCmp cmp] (h : t.WF) : + t.maxKey?.bind t.getKey? = t.maxKey? := + Impl.maxKey?_bind_getKey? h + +theorem maxKey?_erase_eq_iff_not_compare_eq_maxKey? [TransCmp cmp] (h : t.WF) {k} : + (t.erase k |>.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq := + Impl.maxKey?_erase!_eq_iff_not_compare_eq_maxKey? h + +theorem maxKey?_erase_eq_of_not_compare_eq_maxKey? [TransCmp cmp] (h : t.WF) {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.maxKey?) = t.maxKey? := + Impl.maxKey?_erase!_eq_of_not_compare_eq_maxKey? h (instOrd := ⟨cmp⟩) + +theorem isSome_maxKey?_of_isSome_maxKey?_erase [TransCmp cmp] (h : t.WF) {k} : + (hs : t.erase k |>.maxKey?.isSome) → + t.maxKey?.isSome := + Impl.isSome_maxKey?_of_isSome_maxKey?_erase! h + +theorem maxKey?_erase_le_maxKey? [TransCmp cmp] (h : t.WF) {k km kme} : + (hkme : (t.erase k |>.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase h <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + Impl.maxKey?_erase!_le_maxKey? h + +theorem maxKey?_insertIfNew [TransCmp cmp] (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 isSome_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} : + (t.insertIfNew k v).maxKey?.isSome := + Impl.isSome_maxKey?_insertIfNew! h + +theorem maxKey?_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew k v |>.maxKey? |>.get <| isSome_maxKey?_insertIfNew h) = kmi) → + cmp km kmi |>.isLE := + Impl.maxKey?_le_maxKey?_insertIfNew! h + +theorem self_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v kmi} : + (hkmi : (t.insertIfNew k v |>.maxKey?.get <| isSome_maxKey?_insertIfNew h) = kmi) → + cmp k kmi |>.isLE := + Impl.self_le_maxKey?_insertIfNew! h + +theorem maxKey?_eq_getLast?_keys [TransCmp cmp] (h : t.WF) : + t.maxKey? = t.keys.getLast? := + Impl.maxKey?_eq_getLast?_keys h (instOrd := ⟨cmp⟩) + +@[simp] +theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) : + (t.modify k f).maxKey? = t.maxKey? := + Impl.maxKey?_modify h + +theorem maxKey?_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} : + (t.alter k f).maxKey? = some k ↔ + (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE := + Impl.maxKey?_alter!_eq_self h + +namespace Const + +variable {β : Type v} {t : Raw α β cmp} + +theorem maxKey?_modify [TransCmp cmp] (h : t.WF) {k f} : + (Const.modify t k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := + Impl.Const.maxKey?_modify h + +@[simp] +theorem maxKey?_modify_eq_maxKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} : + (Const.modify t k f).maxKey? = t.maxKey? := + Impl.Const.maxKey?_modify_eq_maxKey? h + +theorem isSome_maxKey?_modify [TransCmp cmp] {k f} (h : t.WF) : + (Const.modify t k f).maxKey?.isSome = !t.isEmpty := + Impl.Const.isSome_maxKey?_modify h + +theorem isSome_maxKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} : + (Const.modify t k f).maxKey?.isSome = t.maxKey?.isSome := + Impl.Const.isSome_maxKey?_modify_eq_isSome h + +theorem compare_maxKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} : + (hkm : t.maxKey? = some km) → + (hkmm : (Const.modify t k f |>.maxKey? |>.get <| + (isSome_maxKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) → + cmp kmm km = .eq := + Impl.Const.compare_maxKey?_modify_eq h + +theorem maxKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} : + (Const.alter t k f).maxKey? = some k ↔ + (f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE := + Impl.Const.maxKey?_alter!_eq_self h + +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 8ccf75d491..f85f37ffea 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -4832,7 +4832,7 @@ theorem minKey_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [Lawfu theorem minKey_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} : (insertEntry k v l |> minKey <| isEmpty_insertEntry) = - ((minKey? l).elim k fun k' => if compare k k'|>.isLE then k else k') := by + ((minKey? l).elim k fun k' => if compare k k' |>.isLE then k else k') := by simp [minKey_eq_get_minKey?, Option.get_eq_iff_eq_some, minKey?_insertEntry hd] theorem minKey_insertEntry_le_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] @@ -5018,7 +5018,7 @@ theorem minKey!_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [Lawf theorem minKey!_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v} : (insertEntry k v l |> minKey!) = - ((minKey? l).elim k fun k' => if compare k k'|>.isLE then k else k') := by + ((minKey? l).elim k fun k' => if compare k k' |>.isLE then k else k') := by simpa [minKey_eq_minKey!] using minKey_insertEntry hd theorem minKey!_insertEntry_le_minKey! [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] @@ -5220,7 +5220,7 @@ theorem minKeyD_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [Lawf theorem minKeyD_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v fallback} : (insertEntry k v l |> minKeyD <| fallback) = - ((minKey? l).elim k fun k' => if compare k k'|>.isLE then k else k') := by + ((minKey? l).elim k fun k' => if compare k k' |>.isLE then k else k') := by simpa [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntry hd theorem minKeyD_insertEntry_le_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] @@ -5382,4 +5382,271 @@ end Const end Min +section Max + +/-- Returns the largest key in an associative list. -/ +abbrev maxKey? [Ord α] (xs : List ((a : α) × β a)) : Option α := + letI : Ord α := .opposite inferInstance + minKey? xs + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? l = some k ↔ getKey? k l = some k ∧ ∀ k' : α, containsKey k' l → (compare k' k).isLE := + letI : Ord α := .opposite inferInstance + minKey?_eq_some_iff_getKey?_eq_self_and_forall hd + +theorem maxKey?_eq_some_iff_mem_and_forall [Ord α] [LawfulEqOrd α] [TransOrd α] [BEq α] + [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? l = some k ↔ containsKey k l ∧ ∀ k' : α, containsKey k' l → (compare k' k).isLE := + letI : Ord α := .opposite inferInstance + minKey?_eq_some_iff_mem_and_forall hd + +theorem maxKey?_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l l' : List ((a : α) × β a)} + (hl : DistinctKeys l) (hp : l.Perm l') : + maxKey? l = maxKey? l' := + letI : Ord α := .opposite inferInstance + minKey?_of_perm hl hp + +theorem maxKey?_eq_none_iff_isEmpty [Ord α] {l : List ((a : α) × β a)} : + maxKey? l = none ↔ l.isEmpty := + letI : Ord α := .opposite inferInstance + minKey?_eq_none_iff_isEmpty + +theorem maxKey?_of_isEmpty [Ord α] [TransOrd α] {l : List ((a : α) × β a)} (he : l.isEmpty) : + maxKey? l = none := + letI : Ord α := .opposite inferInstance + minKey?_of_isEmpty he + +theorem isNone_maxKey?_eq_isEmpty [Ord α] {l : List ((a : α) × β a)} : + (maxKey? l).isNone = l.isEmpty := + letI : Ord α := .opposite inferInstance + isNone_minKey?_eq_isEmpty + +theorem isSome_maxKey?_eq_not_isEmpty [Ord α] {l : List ((a : α) × β a)} : + (maxKey? l).isSome = !l.isEmpty := + letI : Ord α := .opposite inferInstance + isSome_minKey?_eq_not_isEmpty + +theorem isSome_maxKey?_iff_isEmpty_eq_false [Ord α] {l : List ((a : α) × β a)} : + (maxKey? l).isSome ↔ l.isEmpty = false := + letI : Ord α := .opposite inferInstance + isSome_minKey?_iff_isEmpty_eq_false + +theorem maxKey?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (insertEntry k v l) = + some ((maxKey? l).elim k fun k' => if compare k' k |>.isLE then k else k') := + letI : Ord α := .opposite inferInstance + minKey?_insertEntry hd + +theorem isSome_maxKey?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (insertEntry k v l) |>.isSome := + letI : Ord α := .opposite inferInstance + isSome_minKey?_insertEntry hd + +theorem isSome_maxKey?_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} + {l : List ((a : α) × β a)} (hc : containsKey k l) : + maxKey? l |>.isSome := + letI : Ord α := .opposite inferInstance + isSome_minKey?_of_containsKey hc + +theorem getKey?_maxKey? [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} (hkm : maxKey? l = some km) : + getKey? km l = some km := + letI : Ord α := .opposite inferInstance + getKey?_minKey? hd hkm + +theorem getKey_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km hc} : + (hkm : (maxKey? l |>.get <| isSome_maxKey?_of_containsKey hc) = km) → getKey km l hc = km := + letI : Ord α := .opposite inferInstance + getKey_minKey? hd + +theorem getKey!_maxKey? [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} : + (hkm : maxKey? l = some km) → getKey! km l = km := + letI : Ord α := .opposite inferInstance + getKey!_minKey? hd + +theorem getKeyD_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback} : + (hkm : maxKey? l = some km) → getKeyD km l fallback = km := + letI : Ord α := .opposite inferInstance + getKeyD_minKey? hd + +theorem maxKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + (maxKey? l |>.bind fun k => getKey? k l) = maxKey? l := + letI : Ord α := .opposite inferInstance + minKey?_bind_getKey? hd + +theorem containsKey_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} + (hd : DistinctKeys l) {km} (hkm : maxKey? l = some km) : + containsKey km l := + letI : Ord α := .opposite inferInstance + containsKey_minKey? hd hkm + +theorem maxKey?_eraseKey_eq_iff_beq_maxKey?_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (eraseKey k l) = maxKey? l ↔ ∀ {km}, maxKey? l = some km → (k == km) = 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 α] + {k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) + (hc : ∀ {km}, maxKey? l = some km → (k == km) = false) : + maxKey? (eraseKey k l) = maxKey? l := + letI : Ord α := .opposite inferInstance + minKey?_eraseKey_eq_of_beq_minKey?_eq_false hd hc + +theorem maxKey?_le_maxKey?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} + {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi} (hkm : maxKey? l = some km) + (hkmi : (insertEntry k v l |> maxKey? |>.get <| isSome_maxKey?_insertEntry hd) = kmi) : + compare km kmi |>.isLE := + letI : Ord α := .opposite inferInstance + minKey?_insertEntry_le_minKey? hd hkm hkmi + +theorem self_le_maxKey?_insertEntry [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} + {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kmi} + (hkmi : (insertEntry k v l |> maxKey? |>.get <| isSome_maxKey?_insertEntry hd) = kmi) : + compare k kmi |>.isLE := + letI : Ord α := .opposite inferInstance + minKey?_insertEntry_le_self hd hkmi + +theorem maxKey?_le_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) (hc : containsKey k l) + (hkm : (maxKey? l |>.get <| isSome_maxKey?_of_containsKey hc) = km) : + compare k km |>.isLE := + letI : Ord α := .opposite inferInstance + (minKey?_le_of_containsKey hd hc hkm :) + +theorem maxKey?_le [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} {l : List ((a : α) × β a)} + (hd : DistinctKeys l) : + (∀ k', maxKey? l = some k' → (compare k' k).isLE) ↔ + (∀ k', containsKey k' l → (compare k' k).isLE) := + letI : Ord α := .opposite inferInstance + le_minKey? hd + +theorem isSome_maxKey?_of_isSome_maxKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} + {l : List ((a : α) × β a)} (hs : eraseKey k l |> maxKey? |>.isSome) : + maxKey? l |>.isSome := + letI : Ord α := .opposite inferInstance + isSome_minKey?_of_isSome_minKey?_eraseKey hs + +theorem containsKey_maxKey?_eraseKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) {kme} + (hkme : (eraseKey k l |> maxKey?) = some kme) : + containsKey kme l := by + apply containsKey_of_containsKey_eraseKey hd + apply containsKey_maxKey? hd.eraseKey hkme + +theorem maxKey?_eraseKey_le_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k km kme} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) + (hkme : (eraseKey k l |> maxKey?) = some kme) + (hkm : (maxKey? l |>.get <| + isSome_maxKey?_of_isSome_maxKey?_eraseKey <| hkme ▸ Option.isSome_some) = km) : + compare kme km |>.isLE := + letI : Ord α := .opposite inferInstance + (minKey?_le_minKey?_eraseKey hd hkme hkm :) + +theorem maxKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (insertEntryIfNew k v l) = + some ((maxKey? l).elim k fun k' => if compare k' k = .lt then k else k') := + letI : Ord α := .opposite inferInstance + minKey?_insertEntryIfNew hd + +theorem isSome_maxKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} + {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (insertEntryIfNew k v l) |>.isSome := + letI : Ord α := .opposite inferInstance + isSome_minKey?_insertEntryIfNew hd + +theorem maxKey?_le_maxKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} + {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {km kmi} (hkm : maxKey? l = some km) + (hkmi : (insertEntryIfNew k v l |> maxKey? |>.get <| isSome_maxKey?_insertEntryIfNew hd) = kmi) : + compare km kmi |>.isLE := + letI : Ord α := .opposite inferInstance + minKey?_insertEntryIfNew_le_minKey? hd hkm hkmi + +theorem self_le_maxKey?_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k kmi : α} + {v : β k} {l : List ((a : α) × β a)} (hd : DistinctKeys l) + (hkmi : (insertEntryIfNew k v l |> maxKey? |>.get <| isSome_maxKey?_insertEntryIfNew hd) = kmi) : + compare k kmi |>.isLE := + letI : Ord α := .opposite inferInstance + (minKey?_insertEntryIfNew_le_self hd hkmi :) + +theorem reverse_keys {l : List ((a : α) × β a)} : + (keys l).reverse = keys l.reverse := by + simp [keys_eq_map] + +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) : + maxKey? l = (keys l).getLast? := by + rw [← List.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) : + maxKey? (modifyKey k f l) = maxKey? l := + letI : Ord α := .opposite inferInstance + minKey?_modifyKey hd + +theorem maxKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] + {k f} {l : List ((a : α) × β a)} (hd : DistinctKeys l) : + maxKey? (alterKey k f l) = some 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 α] {k f} + {l : List ((_ : α) × β)} (hd : DistinctKeys l) : + maxKey? (modifyKey k f l) = (maxKey? l).map fun km => if km == k then k else km := + letI : Ord α := .opposite inferInstance + minKey?_modifyKey hd + +theorem maxKey?_modifyKey_eq_maxKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + [LawfulEqOrd α] {k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) : + maxKey? (modifyKey k f l) = maxKey? l := + letI : Ord α := .opposite inferInstance + minKey?_modifyKey_eq_minKey? hd + +theorem isSome_maxKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f} + {l : List ((_ : α) × β)} : + (modifyKey k f l |> maxKey?).isSome = !l.isEmpty := + letI : Ord α := .opposite inferInstance + isSome_minKey?_modifyKey + +theorem isSome_maxKey?_modifyKey_eq_isSome [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f} + {l : List ((_ : α) × β)} : + (modifyKey k f l |> maxKey?).isSome = (maxKey? l).isSome := + letI : Ord α := .opposite inferInstance + isSome_minKey?_modifyKey_eq_isSome + +theorem maxKey?_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k f km kmm} + {l : List ((_ : α) × β)} (hd : DistinctKeys l) (hkm : maxKey? l = some km) + (hkmm : (modifyKey k f l |> maxKey? |>.get <| + isSome_maxKey?_modifyKey_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) : + kmm == km := + letI : Ord α := .opposite inferInstance + minKey?_modifyKey_beq hd hkm hkmm + +theorem maxKey?_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] + {k f} {l : List ((_ : α) × β)} (hd : DistinctKeys l) : + maxKey? (alterKey k f l) = some 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 diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index fea60b540c..e83cd49918 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -1798,7 +1798,7 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] : theorem minKey?_insert [TransCmp cmp] {k v} : (t.insert k v).minKey? = - some (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.minKey?_insert theorem isSome_minKey?_insert [TransCmp cmp] {k v} : @@ -1958,7 +1958,7 @@ theorem minKey_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {he k theorem minKey_insert [TransCmp cmp] {k v} : (t.insert k v).minKey isEmpty_insert = - t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k' := + t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k' := DTreeMap.minKey_insert theorem minKey_insert_le_minKey [TransCmp cmp] {k v he} : @@ -2088,7 +2088,7 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh theorem minKey!_insert [TransCmp cmp] [Inhabited α] {k v} : (t.insert k v |>.minKey!) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (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} : @@ -2212,7 +2212,7 @@ theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] theorem minKeyD_insert [TransCmp cmp] {k v fallback} : (t.insert k v |>.minKeyD fallback) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.minKeyD_insert theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (he : t.isEmpty = false) @@ -2312,4 +2312,188 @@ theorem minKeyD_alter_eq_self [TransCmp cmp] {k f} end Min +section Max + +@[simp] +theorem maxKey?_emptyc : + (∅ : TreeMap α β cmp).maxKey? = none := + DTreeMap.maxKey?_emptyc + +theorem maxKey?_of_isEmpty [TransCmp cmp] : + (he : t.isEmpty) → t.maxKey? = none := + DTreeMap.maxKey?_of_isEmpty + +@[simp] +theorem maxKey?_eq_none_iff [TransCmp cmp] : + t.maxKey? = none ↔ t.isEmpty := + DTreeMap.maxKey?_eq_none_iff + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] {km} : + t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall + +theorem maxKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} : + t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.maxKey?_eq_some_iff_mem_and_forall + +@[simp] +theorem isNone_maxKey?_eq_isEmpty [TransCmp cmp] : + t.maxKey?.isNone = t.isEmpty := + DTreeMap.isNone_maxKey?_eq_isEmpty + +@[simp] +theorem isSome_maxKey?_eq_not_isEmpty [TransCmp cmp] : + t.maxKey?.isSome = !t.isEmpty := + DTreeMap.isSome_maxKey?_eq_not_isEmpty + +theorem isSome_maxKey?_iff_isEmpty_eq_false [TransCmp cmp] : + t.maxKey?.isSome ↔ t.isEmpty = false := + DTreeMap.isSome_maxKey?_iff_isEmpty_eq_false + +theorem maxKey?_insert [TransCmp cmp] {k v} : + (t.insert k v).maxKey? = + some (t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') := + DTreeMap.maxKey?_insert + +theorem isSome_maxKey?_insert [TransCmp cmp] {k v} : + (t.insert k v).maxKey?.isSome := + DTreeMap.isSome_maxKey?_insert + +theorem maxKey?_le_maxKey?_insert [TransCmp cmp] {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert k v |>.maxKey? |>.get isSome_maxKey?_insert) = kmi) → + cmp km kmi |>.isLE := + DTreeMap.maxKey?_le_maxKey?_insert + +theorem self_le_maxKey?_insert [TransCmp cmp] {k v kmi} : + (hkmi : (t.insert k v |>.maxKey?.get isSome_maxKey?_insert) = kmi) → + cmp k kmi |>.isLE := + DTreeMap.self_le_maxKey?_insert + +theorem contains_maxKey? [TransCmp cmp] {km} : + (hkm : t.maxKey? = some km) → + t.contains km := + DTreeMap.contains_maxKey? + +theorem isSome_maxKey?_of_contains [TransCmp cmp] {k} : + (hc : t.contains k) → t.maxKey?.isSome := + DTreeMap.isSome_maxKey?_of_contains + +theorem isSome_maxKey?_of_mem [TransCmp cmp] {k} : + k ∈ t → t.maxKey?.isSome := + DTreeMap.isSome_maxKey?_of_mem + +theorem le_maxKey?_of_contains [TransCmp cmp] {k km} : + (hc : t.contains k) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_contains hc) = km) → + cmp k km |>.isLE := + DTreeMap.le_maxKey?_of_contains + +theorem le_maxKey?_of_mem [TransCmp cmp] {k km} : + (hc : k ∈ t) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_mem hc) = km) → + cmp k km |>.isLE := + DTreeMap.le_maxKey?_of_mem + +theorem maxKey?_le [TransCmp cmp] {k} : + (∀ k', t.maxKey? = some k' → (cmp k' k).isLE) ↔ + (∀ k', k' ∈ t → (cmp k' k).isLE) := + DTreeMap.maxKey?_le + +theorem getKey?_maxKey? [TransCmp cmp] {km} : + (hkm : t.maxKey? = some km) → t.getKey? km = some km := + DTreeMap.getKey?_maxKey? + +theorem getKey_maxKey? [TransCmp cmp] {km hc} : + (hkm : t.maxKey?.get (isSome_maxKey?_of_contains hc) = km) → t.getKey km hc = km := + DTreeMap.getKey_maxKey? + +theorem getKey!_maxKey? [TransCmp cmp] [Inhabited α] {km} : + (hkm : t.maxKey? = some km) → t.getKey! km = km := + DTreeMap.getKey!_maxKey? + +theorem getKeyD_maxKey? [TransCmp cmp] {km fallback} : + (hkm : t.maxKey? = some km) → t.getKeyD km fallback = km := + DTreeMap.getKeyD_maxKey? + +@[simp] +theorem maxKey?_bind_getKey? [TransCmp cmp] : + t.maxKey?.bind t.getKey? = t.maxKey? := + DTreeMap.maxKey?_bind_getKey? + +theorem maxKey?_erase_eq_iff_not_compare_eq_maxKey? [TransCmp cmp] {k} : + (t.erase k |>.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq := + DTreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? + +theorem maxKey?_erase_eq_of_not_compare_eq_maxKey? [TransCmp cmp] {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.maxKey?) = t.maxKey? := + DTreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? + +theorem isSome_maxKey?_of_isSome_maxKey?_erase [TransCmp cmp] {k} : + (hs : t.erase k |>.maxKey?.isSome) → + t.maxKey?.isSome := + DTreeMap.isSome_maxKey?_of_isSome_maxKey?_erase + +theorem maxKey?_erase_le_maxKey? [TransCmp cmp] {k km kme} : + (hkme : (t.erase k |>.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + DTreeMap.maxKey?_erase_le_maxKey? + +theorem maxKey?_insertIfNew [TransCmp cmp] {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 isSome_maxKey?_insertIfNew [TransCmp cmp] {k v} : + (t.insertIfNew k v).maxKey?.isSome := + DTreeMap.isSome_maxKey?_insertIfNew + +theorem maxKey?_le_maxKey?_insertIfNew [TransCmp cmp] {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew k v |>.maxKey? |>.get isSome_maxKey?_insertIfNew) = kmi) → + cmp km kmi |>.isLE := + DTreeMap.maxKey?_le_maxKey?_insertIfNew + +theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} : + (hkmi : (t.insertIfNew k v |>.maxKey?.get isSome_maxKey?_insertIfNew) = kmi) → + cmp k kmi |>.isLE := + DTreeMap.self_le_maxKey?_insertIfNew + +theorem maxKey?_eq_getLast?_keys [TransCmp cmp] : + t.maxKey? = t.keys.getLast? := + DTreeMap.maxKey?_eq_getLast?_keys + +theorem maxKey?_modify [TransCmp cmp] {k f} : + (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := + DTreeMap.Const.maxKey?_modify + +@[simp] +theorem maxKey?_modify_eq_maxKey? [TransCmp cmp] [LawfulEqCmp cmp] {k f} : + (t.modify k f).maxKey? = t.maxKey? := + DTreeMap.Const.maxKey?_modify_eq_maxKey? + +theorem isSome_maxKey?_modify [TransCmp cmp] {k f} : + (t.modify k f).maxKey?.isSome = !t.isEmpty := + DTreeMap.Const.isSome_maxKey?_modify + +theorem isSome_maxKey?_modify_eq_isSome [TransCmp cmp] {k f} : + (t.modify k f).maxKey?.isSome = t.maxKey?.isSome := + DTreeMap.Const.isSome_maxKey?_modify_eq_isSome + +theorem compare_maxKey?_modify_eq [TransCmp cmp] {k f km kmm} : + (hkm : t.maxKey? = some km) → + (hkmm : (t.modify k f |>.maxKey? |>.get <| + isSome_maxKey?_modify_eq_isSome.trans <| hkm ▸ Option.isSome_some) = kmm) → + cmp kmm km = .eq := + DTreeMap.Const.compare_maxKey?_modify_eq + +theorem maxKey?_alter_eq_self [TransCmp cmp] {k f} : + (t.alter k f).maxKey? = some k ↔ + (f t[k]?).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE := + DTreeMap.Const.maxKey?_alter_eq_self + +end Max + end Std.TreeMap diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 0bf1a627b3..cfd8f4bb24 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -1807,7 +1807,7 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] (h : t.WF) : theorem minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : (t.insert k v).minKey? = - some (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.Raw.minKey?_insert h theorem isSome_minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : @@ -1969,7 +1969,7 @@ theorem minKey!_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] [Inh theorem minKey!_insert [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} : (t.insert k v |>.minKey!) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (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) @@ -2090,7 +2090,7 @@ theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : theorem minKeyD_insert [TransCmp cmp] (h : t.WF) {k v fallback} : (t.insert k v |>.minKeyD fallback) = - (t.minKey?.elim k fun k' => if cmp k k'|>.isLE then k else k') := + (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.Raw.minKeyD_insert h theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) @@ -2190,4 +2190,188 @@ theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} end Min +section Max + +@[simp] +theorem maxKey?_emptyc : + (empty : Raw α β cmp).maxKey? = none := + DTreeMap.Raw.maxKey?_emptyc + +theorem maxKey?_of_isEmpty [TransCmp cmp] (h : t.WF) : + (he : t.isEmpty) → t.maxKey? = none := + DTreeMap.Raw.maxKey?_of_isEmpty h + +@[simp] +theorem maxKey?_eq_none_iff [TransCmp cmp] (h : t.WF) : + t.maxKey? = none ↔ t.isEmpty := + DTreeMap.Raw.maxKey?_eq_none_iff h + +theorem maxKey?_eq_some_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} : + t.maxKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.Raw.maxKey?_eq_some_iff_getKey?_eq_self_and_forall h + +theorem maxKey?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} : + t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.Raw.maxKey?_eq_some_iff_mem_and_forall h + +@[simp] +theorem isNone_maxKey?_eq_isEmpty [TransCmp cmp] (h : t.WF) : + t.maxKey?.isNone = t.isEmpty := + DTreeMap.Raw.isNone_maxKey?_eq_isEmpty h + +@[simp] +theorem isSome_maxKey?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) : + t.maxKey?.isSome = !t.isEmpty := + DTreeMap.Raw.isSome_maxKey?_eq_not_isEmpty h + +theorem isSome_maxKey?_iff_isEmpty_eq_false [TransCmp cmp] (h : t.WF) : + t.maxKey?.isSome ↔ t.isEmpty = false := + DTreeMap.Raw.isSome_maxKey?_iff_isEmpty_eq_false h + +theorem maxKey?_insert [TransCmp cmp] (h : t.WF) {k v} : + (t.insert k v).maxKey? = + some (t.maxKey?.elim k fun k' => if cmp k' k |>.isLE then k else k') := + DTreeMap.Raw.maxKey?_insert h + +theorem isSome_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v} : + (t.insert k v).maxKey?.isSome := + DTreeMap.Raw.isSome_maxKey?_insert h + +theorem maxKey?_le_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insert k v |>.maxKey? |>.get <| isSome_maxKey?_insert h) = kmi) → + cmp km kmi |>.isLE := + DTreeMap.Raw.maxKey?_le_maxKey?_insert h + +theorem self_le_maxKey?_insert [TransCmp cmp] (h : t.WF) {k v kmi} : + (hkmi : (t.insert k v |>.maxKey?.get <| isSome_maxKey?_insert h) = kmi) → + cmp k kmi |>.isLE := + DTreeMap.Raw.self_le_maxKey?_insert h + +theorem contains_maxKey? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → + t.contains km := + DTreeMap.Raw.contains_maxKey? h + +theorem isSome_maxKey?_of_contains [TransCmp cmp] (h : t.WF) {k} : + (hc : t.contains k) → t.maxKey?.isSome := + DTreeMap.Raw.isSome_maxKey?_of_contains h + +theorem isSome_maxKey?_of_mem [TransCmp cmp] (h : t.WF) {k} : + k ∈ t → t.maxKey?.isSome := + DTreeMap.Raw.isSome_maxKey?_of_mem h + +theorem le_maxKey?_of_contains [TransCmp cmp] (h : t.WF) {k km} : + (hc : t.contains k) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_contains h hc) = km) → + cmp k km |>.isLE := + DTreeMap.Raw.le_maxKey?_of_contains h + +theorem le_maxKey?_of_mem [TransCmp cmp] (h : t.WF) {k km} : + (hc : k ∈ t) → (hkm : (t.maxKey?.get <| isSome_maxKey?_of_mem h hc) = km) → + cmp k km |>.isLE := + DTreeMap.Raw.le_maxKey?_of_mem h + +theorem maxKey?_le [TransCmp cmp] {k} (h : t.WF) : + (∀ k', t.maxKey? = some k' → (cmp k' k).isLE) ↔ + (∀ k', k' ∈ t → (cmp k' k).isLE) := + DTreeMap.Raw.maxKey?_le h + +theorem getKey?_maxKey? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey? km = some km := + DTreeMap.Raw.getKey?_maxKey? h + +theorem getKey_maxKey? [TransCmp cmp] (h : t.WF) {km hc} : + (hkm : t.maxKey?.get (isSome_maxKey?_of_contains h hc) = km) → t.getKey km hc = km := + DTreeMap.Raw.getKey_maxKey? h + +theorem getKey!_maxKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} : + (hkm : t.maxKey? = some km) → t.getKey! km = km := + DTreeMap.Raw.getKey!_maxKey? h + +theorem getKeyD_maxKey? [TransCmp cmp] (h : t.WF) {km fallback} : + (hkm : t.maxKey? = some km) → t.getKeyD km fallback = km := + DTreeMap.Raw.getKeyD_maxKey? h + +@[simp] +theorem maxKey?_bind_getKey? [TransCmp cmp] (h : t.WF) : + t.maxKey?.bind t.getKey? = t.maxKey? := + DTreeMap.Raw.maxKey?_bind_getKey? h + +theorem maxKey?_erase_eq_iff_not_compare_eq_maxKey? [TransCmp cmp] (h : t.WF) {k} : + (t.erase k |>.maxKey?) = t.maxKey? ↔ + ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq := + DTreeMap.Raw.maxKey?_erase_eq_iff_not_compare_eq_maxKey? h + +theorem maxKey?_erase_eq_of_not_compare_eq_maxKey? [TransCmp cmp] (h : t.WF) {k} : + (hc : ∀ {km}, t.maxKey? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.maxKey?) = t.maxKey? := + DTreeMap.Raw.maxKey?_erase_eq_of_not_compare_eq_maxKey? h + +theorem isSome_maxKey?_of_isSome_maxKey?_erase [TransCmp cmp] (h : t.WF) {k} : + (hs : t.erase k |>.maxKey?.isSome) → + t.maxKey?.isSome := + DTreeMap.Raw.isSome_maxKey?_of_isSome_maxKey?_erase h + +theorem maxKey?_erase_le_maxKey? [TransCmp cmp] (h : t.WF) {k km kme} : + (hkme : (t.erase k |>.maxKey?) = some kme) → + (hkm : (t.maxKey?.get <| + isSome_maxKey?_of_isSome_maxKey?_erase h <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + DTreeMap.Raw.maxKey?_erase_le_maxKey? h + +theorem maxKey?_insertIfNew [TransCmp cmp] (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 isSome_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v} : + (t.insertIfNew k v).maxKey?.isSome := + DTreeMap.Raw.isSome_maxKey?_insertIfNew h + +theorem maxKey?_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v km kmi} : + (hkm : t.maxKey? = some km) → + (hkmi : (t.insertIfNew k v |>.maxKey? |>.get <| isSome_maxKey?_insertIfNew h) = kmi) → + cmp km kmi |>.isLE := + DTreeMap.Raw.maxKey?_le_maxKey?_insertIfNew h + +theorem self_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v kmi} : + (hkmi : (t.insertIfNew k v |>.maxKey?.get <| isSome_maxKey?_insertIfNew h) = kmi) → + cmp k kmi |>.isLE := + DTreeMap.Raw.self_le_maxKey?_insertIfNew h + +theorem maxKey?_eq_getLast?_keys [TransCmp cmp] (h : t.WF) : + t.maxKey? = t.keys.getLast? := + DTreeMap.Raw.maxKey?_eq_getLast?_keys h + +theorem maxKey?_modify [TransCmp cmp] (h : t.WF) {k f} : + (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := + DTreeMap.Raw.Const.maxKey?_modify h + +@[simp] +theorem maxKey?_modify_eq_maxKey? [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f} : + (t.modify k f).maxKey? = t.maxKey? := + DTreeMap.Raw.Const.maxKey?_modify_eq_maxKey? h + +theorem isSome_maxKey?_modify [TransCmp cmp] {k f} (h : t.WF) : + (t.modify k f).maxKey?.isSome = !t.isEmpty := + DTreeMap.Raw.Const.isSome_maxKey?_modify h + +theorem isSome_maxKey?_modify_eq_isSome [TransCmp cmp] (h : t.WF) {k f} : + (t.modify k f).maxKey?.isSome = t.maxKey?.isSome := + DTreeMap.Raw.Const.isSome_maxKey?_modify_eq_isSome h + +theorem compare_maxKey?_modify_eq [TransCmp cmp] (h : t.WF) {k f km kmm} : + (hkm : t.maxKey? = some km) → + (hkmm : (t.modify k f |>.maxKey? |>.get <| + (isSome_maxKey?_modify_eq_isSome h).trans <| hkm ▸ Option.isSome_some) = kmm) → + cmp kmm km = .eq := + DTreeMap.Raw.Const.compare_maxKey?_modify_eq h + +theorem maxKey?_alter_eq_self [TransCmp cmp] (h : t.WF) {k f} : + (t.alter k f).maxKey? = some k ↔ + (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k' k).isLE := + DTreeMap.Raw.Const.maxKey?_alter_eq_self h + +end Max + end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index abb5109113..7bf36f36aa 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -1070,4 +1070,134 @@ theorem minD_eq_headD_toList [TransCmp cmp] {fallback} : end Min +section Max + +@[simp] +theorem max?_emptyc : + (∅ : TreeSet α cmp).max? = none := + TreeMap.maxKey?_emptyc + +theorem max?_of_isEmpty [TransCmp cmp] : + (he : t.isEmpty) → t.max? = none := + TreeMap.maxKey?_of_isEmpty + +@[simp] +theorem max?_eq_none_iff [TransCmp cmp] : + t.max? = none ↔ t.isEmpty := + TreeMap.maxKey?_eq_none_iff + +theorem max?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] {km} : + t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + TreeMap.maxKey?_eq_some_iff_getKey?_eq_self_and_forall + +theorem max?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] {km} : + t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + TreeMap.maxKey?_eq_some_iff_mem_and_forall + +@[simp] +theorem isNone_max?_eq_isEmpty [TransCmp cmp] : + t.max?.isNone = t.isEmpty := + TreeMap.isNone_maxKey?_eq_isEmpty + +@[simp] +theorem isSome_max?_eq_not_isEmpty [TransCmp cmp] : + t.max?.isSome = !t.isEmpty := + TreeMap.isSome_maxKey?_eq_not_isEmpty + +theorem isSome_max?_iff_isEmpty_eq_false [TransCmp cmp] : + t.max?.isSome ↔ t.isEmpty = false := + DTreeMap.isSome_maxKey?_iff_isEmpty_eq_false + +theorem max?_insert [TransCmp cmp] {k} : + (t.insert k).max? = + t.max?.elim k fun k' => if cmp k' k = .lt then k else k' := + TreeMap.maxKey?_insertIfNew + +theorem isSome_max?_insert [TransCmp cmp] {k} : + (t.insert k).max?.isSome := + TreeMap.isSome_maxKey?_insertIfNew + +theorem max?_le_max?_insert [TransCmp cmp] {k km kmi} : + (hkm : t.max? = some km) → + (hkmi : (t.insert k |>.max? |>.get isSome_max?_insert) = kmi) → + cmp km kmi |>.isLE := + TreeMap.maxKey?_le_maxKey?_insertIfNew + +theorem self_le_max?_insert [TransCmp cmp] {k kmi} : + (hkmi : (t.insert k |>.max?.get isSome_max?_insert) = kmi) → + cmp k kmi |>.isLE := + TreeMap.self_le_maxKey?_insertIfNew + +theorem contains_max? [TransCmp cmp] {km} : + (hkm : t.max? = some km) → + t.contains km := + TreeMap.contains_maxKey? + +theorem isSome_max?_of_contains [TransCmp cmp] {k} : + (hc : t.contains k) → t.max?.isSome := + TreeMap.isSome_maxKey?_of_contains + +theorem isSome_max?_of_mem [TransCmp cmp] {k} : + k ∈ t → t.max?.isSome := + TreeMap.isSome_maxKey?_of_mem + +theorem le_max?_of_contains [TransCmp cmp] {k km} : + (hc : t.contains k) → (hkm : (t.max?.get <| isSome_max?_of_contains hc) = km) → + cmp k km |>.isLE := + TreeMap.le_maxKey?_of_contains + +theorem le_max?_of_mem [TransCmp cmp] {k km} : + (hc : k ∈ t) → (hkm : (t.max?.get <| isSome_max?_of_mem hc) = km) → + cmp k km |>.isLE := + TreeMap.le_maxKey?_of_mem + +theorem max?_le [TransCmp cmp] {k} : + (∀ k', t.max? = some k' → (cmp k' k).isLE) ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) := + TreeMap.maxKey?_le + +theorem get?_max? [TransCmp cmp] {km} : + (hkm : t.max? = some km) → t.get? km = some km := + DTreeMap.getKey?_maxKey? + +theorem get_max? [TransCmp cmp] {km hc} : + (hkm : t.max?.get (isSome_max?_of_contains hc) = km) → t.get km hc = km := + DTreeMap.getKey_maxKey? + +theorem get!_max? [TransCmp cmp] [Inhabited α] {km} : + (hkm : t.max? = some km) → t.get! km = km := + DTreeMap.getKey!_maxKey? + +theorem getD_max? [TransCmp cmp] {km fallback} : + (hkm : t.max? = some km) → t.getD km fallback = km := + DTreeMap.getKeyD_maxKey? + +@[simp] +theorem max?_bind_get? [TransCmp cmp] : + t.max?.bind t.get? = t.max? := + TreeMap.maxKey?_bind_getKey? + +theorem max?_erase_eq_iff_not_compare_eq_max? [TransCmp cmp] {k} : + (t.erase k |>.max?) = t.max? ↔ + ∀ {km}, t.max? = some km → ¬ cmp k km = .eq := + TreeMap.maxKey?_erase_eq_iff_not_compare_eq_maxKey? + +theorem max?_erase_eq_of_not_compare_eq_max? [TransCmp cmp] {k} : + (hc : ∀ {km}, t.max? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.max?) = t.max? := + TreeMap.maxKey?_erase_eq_of_not_compare_eq_maxKey? + +theorem isSome_max?_of_isSome_max?_erase [TransCmp cmp] {k} : + (hs : t.erase k |>.max?.isSome) → + t.max?.isSome := + TreeMap.isSome_maxKey?_of_isSome_maxKey?_erase + +theorem max?_erase_le_max? [TransCmp cmp] {k km kme} : + (hkme : (t.erase k |>.max?) = some kme) → + (hkm : (t.max?.get <| + isSome_max?_of_isSome_max?_erase <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + TreeMap.maxKey?_erase_le_maxKey? + +end Max + end Std.TreeSet diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 2ee541a1f3..9fd6334204 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -972,4 +972,138 @@ theorem minD_eq_headD_toList [TransCmp cmp] (h : t.WF) {fallback} : end Min +section Max + +@[simp] +theorem max?_emptyc : + (empty : Raw α cmp).max? = none := + TreeMap.Raw.maxKey?_emptyc + +theorem max?_of_isEmpty [TransCmp cmp] (h : t.WF) : + (he : t.isEmpty) → t.max? = none := + TreeMap.Raw.maxKey?_of_isEmpty h + +@[simp] +theorem max?_eq_none_iff [TransCmp cmp] (h : t.WF) : + t.max? = none ↔ t.isEmpty := + TreeMap.Raw.maxKey?_eq_none_iff h + +theorem max?_eq_some_iff_get?_eq_self_and_forall [TransCmp cmp] (h : t.WF) {km} : + t.max? = some km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.Raw.maxKey?_eq_some_iff_getKey?_eq_self_and_forall h + +theorem max?_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {km} : + t.max? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE := + DTreeMap.Raw.maxKey?_eq_some_iff_mem_and_forall h + +@[simp] +theorem isNone_max?_eq_isEmpty [TransCmp cmp] (h : t.WF) : + t.max?.isNone = t.isEmpty := + TreeMap.Raw.isNone_maxKey?_eq_isEmpty h + +@[simp] +theorem isSome_max?_eq_not_isEmpty [TransCmp cmp] (h : t.WF) : + t.max?.isSome = !t.isEmpty := + TreeMap.Raw.isSome_maxKey?_eq_not_isEmpty h + +theorem isSome_max?_iff_isEmpty_eq_false [TransCmp cmp] (h : t.WF) : + t.max?.isSome ↔ t.isEmpty = false := + TreeMap.Raw.isSome_maxKey?_iff_isEmpty_eq_false h + +theorem max?_insert [TransCmp cmp] (h : t.WF) {k} : + (t.insert k).max? = + t.max?.elim k fun k' => if cmp k' k = .lt then k else k' := + TreeMap.Raw.maxKey?_insertIfNew h + +theorem isSome_max?_insert [TransCmp cmp] (h : t.WF) {k} : + (t.insert k).max?.isSome := + TreeMap.Raw.isSome_maxKey?_insertIfNew h + +theorem max?_le_max?_insert [TransCmp cmp] (h : t.WF) {k km kmi} : + (hkm : t.max? = some km) → + (hkmi : (t.insert k |>.max? |>.get <| isSome_max?_insert h) = kmi) → + cmp km kmi |>.isLE := + TreeMap.Raw.maxKey?_le_maxKey?_insertIfNew h + +theorem self_le_max?_insert [TransCmp cmp] (h : t.WF) {k kmi} : + (hkmi : (t.insert k |>.max?.get <| isSome_max?_insert h) = kmi) → + cmp k kmi |>.isLE := + TreeMap.Raw.self_le_maxKey?_insertIfNew h + +theorem contains_max? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.max? = some km) → + t.contains km := + TreeMap.Raw.contains_maxKey? h + +theorem isSome_max?_of_contains [TransCmp cmp] (h : t.WF) {k} : + (hc : t.contains k) → t.max?.isSome := + TreeMap.Raw.isSome_maxKey?_of_contains h + +theorem isSome_max?_of_mem [TransCmp cmp] (h : t.WF) {k} : + k ∈ t → t.max?.isSome := + TreeMap.Raw.isSome_maxKey?_of_mem h + +theorem le_max?_of_contains [TransCmp cmp] (h : t.WF) {k km} : + (hc : t.contains k) → (hkm : (t.max?.get <| isSome_max?_of_contains h hc) = km) → + cmp k km |>.isLE := + TreeMap.Raw.le_maxKey?_of_contains h + +theorem le_max?_of_mem [TransCmp cmp] (h : t.WF) {k km} : + (hc : k ∈ t) → (hkm : (t.max?.get <| isSome_max?_of_mem h hc) = km) → + cmp k km |>.isLE := + TreeMap.Raw.le_maxKey?_of_mem h + +theorem max?_le [TransCmp cmp] {k} (h : t.WF) : + (∀ k', t.max? = some k' → (cmp k' k).isLE) ↔ (∀ k', k' ∈ t → (cmp k' k).isLE) := + TreeMap.Raw.maxKey?_le h + +theorem get?_max? [TransCmp cmp] (h : t.WF) {km} : + (hkm : t.max? = some km) → t.get? km = some km := + TreeMap.Raw.getKey?_maxKey? h + +theorem get_max? [TransCmp cmp] (h : t.WF) {km hc} : + (hkm : t.max?.get (isSome_max?_of_contains h hc) = km) → t.get km hc = km := + TreeMap.Raw.getKey_maxKey? h + +theorem get!_max? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} : + (hkm : t.max? = some km) → t.get! km = km := + TreeMap.Raw.getKey!_maxKey? h + +theorem getD_max? [TransCmp cmp] (h : t.WF) {km fallback} : + (hkm : t.max? = some km) → t.getD km fallback = km := + TreeMap.Raw.getKeyD_maxKey? h + +@[simp] +theorem max?_bind_get? [TransCmp cmp] (h : t.WF) : + t.max?.bind t.get? = t.max? := + TreeMap.Raw.maxKey?_bind_getKey? h + +theorem max?_erase_eq_iff_not_compare_eq_max? [TransCmp cmp] (h : t.WF) {k} : + (t.erase k |>.max?) = t.max? ↔ + ∀ {km}, t.max? = some km → ¬ cmp k km = .eq := + TreeMap.Raw.maxKey?_erase_eq_iff_not_compare_eq_maxKey? h + +theorem max?_erase_eq_of_not_compare_eq_max? [TransCmp cmp] (h : t.WF) {k} : + (hc : ∀ {km}, t.max? = some km → ¬ cmp k km = .eq) → + (t.erase k |>.max?) = t.max? := + TreeMap.Raw.maxKey?_erase_eq_of_not_compare_eq_maxKey? h + +theorem isSome_max?_of_isSome_max?_erase [TransCmp cmp] (h : t.WF) {k} : + (hs : t.erase k |>.max?.isSome) → + t.max?.isSome := + TreeMap.Raw.isSome_maxKey?_of_isSome_maxKey?_erase h + +theorem max?_erase_le_max? [TransCmp cmp] (h : t.WF) {k km kme} : + (hkme : (t.erase k |>.max?) = some kme) → + (hkm : (t.max?.get <| + isSome_max?_of_isSome_max?_erase h <| hkme ▸ Option.isSome_some) = km) → + cmp kme km |>.isLE := + TreeMap.Raw.maxKey?_erase_le_maxKey? h + +theorem max?_eq_head?_toList [TransCmp cmp] (h : t.WF) : + t.max? = t.toList.getLast? := + TreeMap.Raw.maxKey?_eq_getLast?_keys h + +end Max + end Std.TreeSet.Raw