From 556e96088ed3850c8fbede8598bc33c9eae4e54c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 20 Nov 2025 16:35:07 +0000 Subject: [PATCH] feat: add lemmas relating `getMin`/`getMin?`/`getMin!`/`getMinD` and insertion to the empty (D)TreeMap/TreeSet (#11231) This PR adds several lemmas that relate `getMin`/`getMin?`/`getMin!`/`getMinD` and insertion to the empty (D)TreeMap/TreeSet and their extensional variants. --------- Co-authored-by: Markus Himmel --- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 88 +++++++++++++++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 32 ++++++++ src/Std/Data/DTreeMap/Raw/Lemmas.lean | 24 ++++++ src/Std/Data/ExtDTreeMap/Lemmas.lean | 36 +++++++++ src/Std/Data/ExtTreeMap/Lemmas.lean | 32 ++++++++ src/Std/Data/ExtTreeSet/Lemmas.lean | 16 ++++ src/Std/Data/Internal/List/Associative.lean | 42 ++++++++++ src/Std/Data/TreeMap/Lemmas.lean | 32 ++++++++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 24 ++++++ src/Std/Data/TreeSet/Lemmas.lean | 16 ++++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 12 +++ 11 files changed, 354 insertions(+) diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 6970a92e6e..dfddfec848 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -5948,6 +5948,94 @@ theorem isSome_minKey?_insert! [TransOrd α] (h : t.WF) {k v} : (t.insert! k v).minKey?.isSome := by simpa only [insert_eq_insert!] using isSome_minKey?_insert h +theorem minKey_insert_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v h.balanced).impl.minKey (isEmpty_insert h) = k := by + revert he + simp_to_model [isEmpty, insert, minKey] using List.minKey_insertEntry_of_isEmpty + +theorem minKey_insert!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert! k v).minKey (isEmpty_insert! h) = k := by + simpa only [insert_eq_insert!] using minKey_insert_of_isEmpty h he + +theorem minKey?_insert_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v h.balanced).impl.minKey? = some k := by + revert he + simp_to_model [isEmpty, insert, minKey?] using List.minKey?_insertEntry_of_isEmpty + +theorem minKey?_insert!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert! k v).minKey? = some k := by + simpa only [insert_eq_insert!] using minKey?_insert_of_isEmpty h he + +theorem minKey!_insert_of_isEmpty [TransOrd α] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v h.balanced).impl.minKey! = k := by + revert he + simp_to_model [isEmpty, insert, minKey!] + intro he + apply List.minKey!_insertEntry_of_isEmpty + · wf_trivial + · exact he + +theorem minKey!_insert!_of_isEmpty [TransOrd α] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert! k v).minKey! = k := by + simpa only [insert_eq_insert!] using minKey!_insert_of_isEmpty h he + +theorem minKeyD_insert_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v h.balanced).impl.minKeyD fallback = k := by + revert he + simp_to_model [isEmpty, insert, minKeyD] + intro he + apply List.minKeyD_insertEntry_of_isEmpty + · wf_trivial + · exact he + +theorem minKeyD_insert!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insert! k v).minKeyD fallback = k := by + simpa only [insert_eq_insert!] using minKeyD_insert_of_isEmpty h he + +theorem minKey_insertIfNew_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v h.balanced).impl.minKey (isEmpty_insertIfNew h) = k := by + revert he + simp_to_model [isEmpty, insertIfNew, minKey] using List.minKey_insertEntryIfNew_of_isEmpty + +theorem minKey_insertIfNew!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew! k v).minKey (isEmpty_insertIfNew! h) = k := by + simpa only [insertIfNew_eq_insertIfNew!] using minKey_insertIfNew_of_isEmpty h he + +theorem minKey?_insertIfNew_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v h.balanced).impl.minKey? = some k := by + revert he + simp_to_model [isEmpty, insertIfNew, minKey?] using List.minKey?_insertEntryIfNew_of_isEmpty + +theorem minKey?_insertIfNew!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew! k v).minKey? = some k := by + simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_of_isEmpty h he + +theorem minKey!_insertIfNew_of_isEmpty [TransOrd α] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v h.balanced).impl.minKey! = k := by + revert he + simp_to_model [isEmpty, insertIfNew, minKey!] + intro he + apply List.minKey!_insertEntryIfNew_of_isEmpty + · wf_trivial + · exact he + +theorem minKey!_insertIfNew!_of_isEmpty [TransOrd α] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew! k v).minKey! = k := by + simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_of_isEmpty h he + +theorem minKeyD_insertIfNew_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v h.balanced).impl.minKeyD fallback = k := by + revert he + simp_to_model [isEmpty, insertIfNew, minKeyD] + intro he + apply List.minKeyD_insertEntryIfNew_of_isEmpty + · wf_trivial + · exact he + +theorem minKeyD_insertIfNew!_of_isEmpty [TransOrd α] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew! k v).minKeyD fallback = k := by + simpa only [insertIfNew_eq_insertIfNew!] using minKeyD_insertIfNew_of_isEmpty h he + theorem minKey?_insert_le_minKey? [TransOrd α] (h : t.WF) {k v km kmi} : (hkm : t.minKey? = some km) → (hkmi : (t.insert k v h.balanced |>.impl.minKey? |>.get <| isSome_minKey?_insert h) = kmi) → diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index bfd34d71b3..d3d1e4d194 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -3619,6 +3619,38 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] : (t.insert k v).minKey?.isSome := Impl.isSome_minKey?_insert t.wf +theorem minKey_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey isEmpty_insert = k := + Impl.minKey_insert_of_isEmpty t.wf he + +theorem minKey?_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + Impl.minKey?_insert_of_isEmpty t.wf he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + Impl.minKey!_insert_of_isEmpty t.wf he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + Impl.minKeyD_insert_of_isEmpty t.wf he + +theorem minKey_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey isEmpty_insertIfNew = k := + Impl.minKey_insertIfNew_of_isEmpty t.wf he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + Impl.minKey?_insertIfNew_of_isEmpty t.wf he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + Impl.minKey!_insertIfNew_of_isEmpty t.wf he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := + Impl.minKeyD_insertIfNew_of_isEmpty t.wf he + theorem minKey?_insert_le_minKey? [TransCmp cmp] {k v km kmi} : (hkm : t.minKey? = some km) → (hkmi : (t.insert k v |>.minKey? |>.get isSome_minKey?_insert) = kmi) → diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index d8248b5915..80bd8f277e 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -3780,6 +3780,30 @@ theorem isSome_minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : (t.insert k v).minKey?.isSome := Impl.isSome_minKey?_insert! h +theorem minKey?_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + Impl.minKey?_insert!_of_isEmpty h he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + Impl.minKey!_insert!_of_isEmpty h he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + Impl.minKeyD_insert!_of_isEmpty h he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + Impl.minKey?_insertIfNew!_of_isEmpty h he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + Impl.minKey!_insertIfNew!_of_isEmpty h he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := + Impl.minKeyD_insertIfNew!_of_isEmpty h he + theorem minKey?_insert_le_minKey? [TransCmp cmp] (h : t.WF) {k v km kmi} : (hkm : t.minKey? = some km) → (hkmi : (t.insert k v |>.minKey? |>.get <| isSome_minKey?_insert h) = kmi) → diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean index 1bfc19209b..cae44acbf3 100644 --- a/src/Std/Data/ExtDTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean @@ -3407,6 +3407,42 @@ theorem isSome_minKey?_iff_ne_empty [TransCmp cmp] : (t.insert k v).minKey?.isSome := t.inductionOn fun _ => DTreeMap.isSome_minKey?_insert +theorem minKey_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey insert_ne_empty = k := by + induction t + case mk a => + exact DTreeMap.minKey_insert_of_isEmpty he + +theorem minKey?_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + t.inductionOn (fun _ he => DTreeMap.minKey?_insert_of_isEmpty he) he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + t.inductionOn (fun _ he => DTreeMap.minKey!_insert_of_isEmpty he) he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + t.inductionOn (fun _ he => DTreeMap.minKeyD_insert_of_isEmpty he) he + +theorem minKey_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey insertIfNew_ne_empty = k := by + induction t + case mk a => + exact DTreeMap.minKey_insertIfNew_of_isEmpty he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + t.inductionOn (fun _ he => DTreeMap.minKey?_insertIfNew_of_isEmpty he) he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + t.inductionOn (fun _ he => DTreeMap.minKey!_insertIfNew_of_isEmpty he) he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := t.inductionOn + (fun _ he => DTreeMap.minKeyD_insertIfNew_of_isEmpty he) he + theorem minKey?_insert_le_minKey? [TransCmp cmp] {k v km kmi} : (hkm : t.minKey? = some km) → (hkmi : (t.insert k v |>.minKey? |>.get isSome_minKey?_insert) = kmi) → diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean index 1f1ed8bacd..2a712ebf05 100644 --- a/src/Std/Data/ExtTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtTreeMap/Lemmas.lean @@ -2081,6 +2081,38 @@ theorem isSome_minKey?_iff_ne_empty [TransCmp cmp] : (t.insert k v).minKey?.isSome := ExtDTreeMap.isSome_minKey?_insert +theorem minKey_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey insert_ne_empty = k := + ExtDTreeMap.minKey_insert_of_isEmpty he + +theorem minKey?_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + ExtDTreeMap.minKey?_insert_of_isEmpty he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + ExtDTreeMap.minKey!_insert_of_isEmpty he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + ExtDTreeMap.minKeyD_insert_of_isEmpty he + +theorem minKey_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey insertIfNew_ne_empty = k := + ExtDTreeMap.minKey_insertIfNew_of_isEmpty he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + ExtDTreeMap.minKey?_insertIfNew_of_isEmpty he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + ExtDTreeMap.minKey!_insertIfNew_of_isEmpty he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := + ExtDTreeMap.minKeyD_insertIfNew_of_isEmpty he + theorem minKey?_insert_le_minKey? [TransCmp cmp] {k v km kmi} : (hkm : t.minKey? = some km) → (hkmi : (t.insert k v |>.minKey? |>.get isSome_minKey?_insert) = kmi) → diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean index fdbc2592f3..518d9d608b 100644 --- a/src/Std/Data/ExtTreeSet/Lemmas.lean +++ b/src/Std/Data/ExtTreeSet/Lemmas.lean @@ -887,6 +887,22 @@ theorem isSome_min?_insert [TransCmp cmp] {k} : (t.insert k).min?.isSome := ExtTreeMap.isSome_minKey?_insertIfNew +theorem min_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) : + (t.insert k).min insert_ne_empty = k := + ExtTreeMap.minKey_insertIfNew_of_isEmpty he + +theorem min?_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) : + (t.insert k).min? = some k := + ExtTreeMap.minKey?_insertIfNew_of_isEmpty he + +theorem min!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k} (he : t.isEmpty) : + (t.insert k).min! = k := + ExtTreeMap.minKey!_insertIfNew_of_isEmpty he + +theorem minD_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) {fallback : α} : + (t.insert k).minD fallback = k := + ExtTreeMap.minKeyD_insertIfNew_of_isEmpty he + theorem min?_insert_le_min? [TransCmp cmp] {k km kmi} : (hkm : t.min? = some km) → (hkmi : (t.insert k |>.min? |>.get isSome_min?_insert) = kmi) → diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 3c076f6565..025078c8e8 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -7958,6 +7958,21 @@ theorem minKeyD_eq_getD_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α minKeyD l fallback = (minKey? l).getD fallback := (rfl) +theorem minKey_insertEntry_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + List.minKey (insertEntry k v l) isEmpty_insertEntry = k := by + simp [minKey, minKey?_insertEntry hl, minKey?_of_isEmpty he] + +theorem minKey?_insertEntry_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + minKey? (insertEntry k v l) = some k := by + simp [minKey?_insertEntry hl, minKey?_of_isEmpty he] + +theorem minKeyD_insertEntry_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) {fallback : α} : + minKeyD (insertEntry k v l) fallback = k := by + simp [minKeyD, minKey?_insertEntry hl, minKey?_of_isEmpty he] + theorem minKey_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {he fallback} : minKey l he = minKeyD l fallback := by @@ -7973,6 +7988,33 @@ theorem minKey!_eq_minKeyD_default [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd minKey! l = minKeyD l default := by simp [minKey!_eq_get!_minKey?, minKeyD_eq_getD_minKey?, Option.get!_eq_getD] +theorem minKey!_insertEntry_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + minKey! (insertEntry k v l) = k := by + simp [minKey!_eq_minKeyD_default] + apply minKeyD_insertEntry_of_isEmpty hl he + +theorem minKey_insertEntryIfNew_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + List.minKey (insertEntryIfNew k v l) isEmpty_insertEntryIfNew = k := by + simp [minKey, minKey?_insertEntryIfNew hl, minKey?_of_isEmpty he] + +theorem minKey?_insertEntryIfNew_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + minKey? (insertEntryIfNew k v l) = some k := by + simp [minKey?_insertEntryIfNew hl, minKey?_of_isEmpty he] + +theorem minKeyD_insertEntryIfNew_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) {fallback : α} : + minKeyD (insertEntryIfNew k v l) fallback = k := by + simp [minKeyD, minKey?_insertEntryIfNew hl, minKey?_of_isEmpty he] + +theorem minKey!_insertEntryIfNew_of_isEmpty [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] {k : α} {v : β k} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) (he : l.isEmpty) : + minKey! (insertEntryIfNew k v l) = k := by + simp [minKey!_eq_minKeyD_default] + apply minKeyD_insertEntryIfNew_of_isEmpty hl he + theorem minKeyD_eq_fallback [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : List ((a : α) × β a)} {fallback} (h : l.isEmpty) : minKeyD l fallback = fallback := by diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 569e8761c5..48b11519af 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -2330,6 +2330,38 @@ theorem isSome_minKey?_iff_isEmpty_eq_false [TransCmp cmp] : some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.minKey?_insert +theorem minKey_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey isEmpty_insert = k := + DTreeMap.minKey_insert_of_isEmpty he + +theorem minKey?_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + DTreeMap.minKey?_insert_of_isEmpty he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + DTreeMap.minKey!_insert_of_isEmpty he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + DTreeMap.minKeyD_insert_of_isEmpty he + +theorem minKey_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey isEmpty_insertIfNew = k := + DTreeMap.minKey_insertIfNew_of_isEmpty he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + DTreeMap.minKey?_insertIfNew_of_isEmpty he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + DTreeMap.minKey!_insertIfNew_of_isEmpty he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := + DTreeMap.minKeyD_insertIfNew_of_isEmpty he + @[grind =] theorem isSome_minKey?_insert [TransCmp cmp] {k v} : (t.insert k v).minKey?.isSome := DTreeMap.isSome_minKey?_insert diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 1f9923b7be..c9fc8e89d8 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -2380,6 +2380,30 @@ theorem minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : some (t.minKey?.elim k fun k' => if cmp k k' |>.isLE then k else k') := DTreeMap.Raw.minKey?_insert h +theorem minKey?_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v).minKey? = some k := + DTreeMap.Raw.minKey?_insert_of_isEmpty h he + +theorem minKey!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insert k v).minKey! = k := + DTreeMap.Raw.minKey!_insert_of_isEmpty h he + +theorem minKeyD_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insert k v).minKeyD fallback = k := + DTreeMap.Raw.minKeyD_insert_of_isEmpty h he + +theorem minKey?_insertIfNew_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey? = some k := + DTreeMap.Raw.minKey?_insertIfNew_of_isEmpty h he + +theorem minKey!_insertIfNew_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {k v} (he : t.isEmpty) : + (t.insertIfNew k v).minKey! = k := + DTreeMap.Raw.minKey!_insertIfNew_of_isEmpty h he + +theorem minKeyD_insertIfNew_of_isEmpty [TransCmp cmp] (h : t.WF) {k v} (he : t.isEmpty) {fallback : α} : + (t.insertIfNew k v).minKeyD fallback = k := + DTreeMap.Raw.minKeyD_insertIfNew_of_isEmpty h he + @[grind =] theorem isSome_minKey?_insert [TransCmp cmp] (h : t.WF) {k v} : (t.insert k v).minKey?.isSome := diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 51f981cfc6..d11c1c88d7 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -1060,6 +1060,22 @@ theorem isSome_min?_insert [TransCmp cmp] {k} : (t.insert k).min?.isSome := TreeMap.isSome_minKey?_insertIfNew +theorem min_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) : + (t.insert k).min isEmpty_insert = k := + TreeMap.minKey_insertIfNew_of_isEmpty he + +theorem min?_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) : + (t.insert k).min? = some k := + TreeMap.minKey?_insertIfNew_of_isEmpty he + +theorem min!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] {k} (he : t.isEmpty) : + (t.insert k).min! = k := + TreeMap.minKey!_insertIfNew_of_isEmpty he + +theorem minD_insert_of_isEmpty [TransCmp cmp] {k} (he : t.isEmpty) {fallback : α} : + (t.insert k).minD fallback = k := + TreeMap.minKeyD_insertIfNew_of_isEmpty he + theorem min?_insert_le_min? [TransCmp cmp] {k km kmi} : (hkm : t.min? = some km) → (hkmi : (t.insert k |>.min? |>.get isSome_min?_insert) = kmi) → diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index d62f006dd5..2d69e536db 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -1096,6 +1096,18 @@ theorem isSome_min?_insert [TransCmp cmp] (h : t.WF) {k} : (t.insert k).min?.isSome := TreeMap.Raw.isSome_minKey?_insertIfNew h +theorem min?_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k} (he : t.isEmpty) : + (t.insert k).min? = some k := + TreeMap.Raw.minKey?_insertIfNew_of_isEmpty h he + +theorem min!_insert_of_isEmpty [TransCmp cmp] [Inhabited α] (h : t.WF) {k} (he : t.isEmpty) : + (t.insert k).min! = k := + TreeMap.Raw.minKey!_insertIfNew_of_isEmpty h he + +theorem minD_insert_of_isEmpty [TransCmp cmp] (h : t.WF) {k} (he : t.isEmpty) {fallback : α} : + (t.insert k).minD fallback = k := + TreeMap.Raw.minKeyD_insertIfNew_of_isEmpty h he + theorem min?_insert_le_min? [TransCmp cmp] (h : t.WF) {k km kmi} : (hkm : t.min? = some km) → (hkmi : (t.insert k |>.min? |>.get <| isSome_min?_insert h) = kmi) →