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 <datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert
GitHub
parent
3b40e0e588
commit
7f4e4557a7
12 changed files with 1715 additions and 77 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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!,
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue