feat: tree map lemmas for minKeyD (#7626)
This PR provides lemmas for the tree map function `minKeyD` 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
6bdf9e46ab
commit
18ac05258b
10 changed files with 1099 additions and 1 deletions
|
|
@ -98,7 +98,8 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
|
|||
⟨`forM, (``forM_eq_forM, #[])⟩,
|
||||
⟨`minKey?, (``minKey?_eq_minKey?, #[``(minKey?_of_perm _)])⟩,
|
||||
⟨`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 _)])⟩]
|
||||
|
||||
/-- Internal implementation detail of the tree map -/
|
||||
scoped syntax "simp_to_model" (" [" (ident,*) "]")? ("using" term)? : tactic
|
||||
|
|
@ -4831,6 +4832,220 @@ theorem minKey!_alter!_eq_self [TransOrd α] [Inhabited α] (h : t.WF) {k f} :
|
|||
|
||||
end Const
|
||||
|
||||
theorem minKey_eq_minKeyD [TransOrd α] (h : t.WF) {he fallback} :
|
||||
t.minKey he = t.minKeyD fallback := by
|
||||
simp_to_model [minKey, minKeyD] using List.minKey_eq_minKeyD
|
||||
|
||||
theorem minKey?_eq_some_minKeyD [TransOrd α] (h : t.WF) {fallback} :
|
||||
(he : t.isEmpty = false) → t.minKey? = some (t.minKeyD fallback) := by
|
||||
simp_to_model [minKey?, minKeyD, isEmpty] using List.minKey?_eq_some_minKeyD
|
||||
|
||||
theorem minKeyD_eq_fallback [TransOrd α] (h : t.WF) {fallback} :
|
||||
(he : t.isEmpty) → t.minKeyD fallback = fallback := by
|
||||
simp_to_model [minKeyD, isEmpty] using List.minKeyD_eq_fallback
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
t.minKey! = t.minKeyD default := by
|
||||
simp_to_model [minKey!, minKeyD] using List.minKey!_eq_minKeyD_default
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km fallback},
|
||||
t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (compare km k).isLE := by
|
||||
simp_to_model [minKeyD, getKey?, contains, isEmpty] using
|
||||
List.minKeyD_eq_iff_getKey?_eq_self_and_forall
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [TransOrd α]
|
||||
[LawfulEqOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {km fallback},
|
||||
t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (compare km k).isLE := by
|
||||
simp_to_model [minKeyD, contains, isEmpty] using List.minKeyD_eq_some_iff_mem_and_forall
|
||||
|
||||
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
|
||||
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
|
||||
simpa [insert_eq_insert!] using minKeyD_insert h
|
||||
|
||||
theorem minKeyD_insert_le_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v fallback},
|
||||
compare (t.insert k v h.balanced |>.impl.minKeyD <| fallback) (t.minKeyD fallback) |>.isLE := by
|
||||
simp_to_model [minKeyD, isEmpty, insert] using List.minKeyD_insertEntry_le_minKeyD
|
||||
|
||||
theorem minKeyD_insert!_le_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v fallback},
|
||||
compare (t.insert! k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using minKeyD_insert_le_minKeyD h
|
||||
|
||||
theorem minKeyD_insert_le_self [TransOrd α] (h : t.WF) {k v fallback} :
|
||||
compare (t.insert k v h.balanced |>.impl.minKeyD <| fallback) k |>.isLE := by
|
||||
simp_to_model [minKeyD, insert] using List.minKeyD_insertEntry_le_self
|
||||
|
||||
theorem minKeyD_insert!_le_self [TransOrd α] (h : t.WF) {k v fallback} :
|
||||
compare (t.insert! k v |>.minKeyD fallback) k |>.isLE := by
|
||||
simpa only [insert_eq_insert!] using minKeyD_insert_le_self h
|
||||
|
||||
theorem contains_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback}, t.contains (t.minKeyD fallback) := by
|
||||
simp_to_model [minKeyD, isEmpty, contains] using List.containsKey_minKeyD
|
||||
|
||||
theorem minKeyD_mem [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback}, (t.minKeyD fallback) ∈ t :=
|
||||
contains_minKeyD h
|
||||
|
||||
theorem minKeyD_le_of_contains [TransOrd α] (h : t.WF) :
|
||||
∀ {k}, (hc : t.contains k) → ∀ {fallback},
|
||||
compare (t.minKeyD fallback) k |>.isLE := by
|
||||
simp_to_model [minKeyD, contains] using List.minKeyD_le_of_containsKey
|
||||
|
||||
theorem minKeyD_le_of_mem [TransOrd α] (h : t.WF) :
|
||||
∀ {k}, (hc : k ∈ t) → ∀ {fallback},
|
||||
compare (t.minKeyD fallback) k |>.isLE :=
|
||||
minKeyD_le_of_contains h
|
||||
|
||||
theorem le_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k fallback},
|
||||
(compare k (t.minKeyD fallback)).isLE ↔ (∀ k', k' ∈ t → (compare k k').isLE) := by
|
||||
simp_to_model [minKeyD, contains, isEmpty] using List.le_minKeyD
|
||||
|
||||
theorem getKey?_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback},
|
||||
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback) := by
|
||||
simp_to_model [minKeyD, getKey?, isEmpty] using List.getKey?_minKeyD
|
||||
|
||||
theorem getKey_minKeyD [TransOrd α] (h : t.WF) : ∀ {fallback he},
|
||||
t.getKey (t.minKeyD fallback) he = (t.minKeyD fallback) := by
|
||||
simp_to_model [minKeyD, contains, isEmpty, getKey] using List.getKey_minKeyD
|
||||
|
||||
theorem getKey_minKeyD_eq_minKey [TransOrd α] (h : t.WF) : ∀ {fallback hc},
|
||||
t.getKey (t.minKeyD fallback) hc = t.minKey (isEmpty_eq_false_of_contains h hc) := by
|
||||
simp_to_model [minKeyD, minKey, contains, isEmpty, getKey] using List.getKey_minKeyD_eq_minKey
|
||||
|
||||
theorem getKey!_minKeyD [TransOrd α] [Inhabited α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback},
|
||||
t.getKey! (t.minKeyD fallback) = (t.minKeyD fallback) := by
|
||||
simp_to_model [minKeyD, isEmpty, getKey!] using List.getKey!_minKeyD
|
||||
|
||||
theorem getKeyD_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {fallback fallback'},
|
||||
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback := by
|
||||
simp_to_model [minKeyD, getKeyD, isEmpty] using List.getKeyD_minKeyD
|
||||
|
||||
theorem minKeyD_erase_eq_iff_not_compare_minKeyD_eq [TransOrd α] (h : t.WF) :
|
||||
∀ {k fallback}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
(t.erase k h.balanced |>.impl.minKeyD <| fallback) = t.minKeyD fallback ↔
|
||||
¬ compare k (t.minKeyD fallback) = .eq := by
|
||||
simp_to_model [minKeyD, isEmpty, erase] using List.minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false
|
||||
|
||||
theorem minKeyD_erase!_eq_iff_not_compare_minKeyD_eq [TransOrd α] (h : t.WF) {k fallback} :
|
||||
(he : (t.erase! k).isEmpty = false) →
|
||||
(t.erase! k |>.minKeyD fallback) = t.minKeyD fallback ↔
|
||||
¬ compare k (t.minKeyD fallback) = .eq := by
|
||||
simpa only [erase_eq_erase!] using minKeyD_erase_eq_iff_not_compare_minKeyD_eq h
|
||||
|
||||
theorem minKeyD_erase_eq_of_not_compare_minKeyD_eq [TransOrd α] (h : t.WF) :
|
||||
∀ {k fallback}, (he : (t.erase k h.balanced).impl.isEmpty = false) →
|
||||
(heq : ¬ compare k (t.minKeyD fallback) = .eq) →
|
||||
(t.erase k h.balanced |>.impl.minKeyD <| fallback) = t.minKeyD fallback := by
|
||||
simp_to_model [minKeyD, isEmpty, erase] using
|
||||
List.minKeyD_eraseKey_eq_of_beq_minKeyD_eq_false
|
||||
|
||||
theorem minKeyD_erase!_eq_of_not_compare_minKeyD_eq [TransOrd α] (h : t.WF) {k fallback} :
|
||||
(he : (t.erase! k).isEmpty = false) → (heq : ¬ compare k (t.minKeyD fallback) = .eq) →
|
||||
(t.erase! k |>.minKeyD fallback) = t.minKeyD fallback := by
|
||||
simpa only [erase_eq_erase!] using minKeyD_erase_eq_of_not_compare_minKeyD_eq h
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [TransOrd α] (h : t.WF) :
|
||||
∀ {k}, (he : (t.erase k h.balanced).impl.isEmpty = false) → ∀ {fallback},
|
||||
compare (t.minKeyD fallback) (t.erase k h.balanced |>.impl.minKeyD <| fallback) |>.isLE := by
|
||||
simp_to_model [minKeyD, isEmpty, erase] using List.minKeyD_le_minKeyD_erase
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase! [TransOrd α] (h : t.WF) {k} :
|
||||
(he : (t.erase! k).isEmpty = false) → ∀ {fallback},
|
||||
compare (t.minKeyD fallback) (t.erase! k |>.minKeyD fallback) |>.isLE := by
|
||||
simpa only [erase_eq_erase!] using minKeyD_le_minKeyD_erase h
|
||||
|
||||
theorem minKeyD_insertIfNew [TransOrd α] (h : t.WF) : ∀ {k v fallback},
|
||||
(t.insertIfNew k v h.balanced |>.impl.minKeyD <| fallback) =
|
||||
t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simp_to_model [minKeyD, minKey?, insertIfNew] using List.minKeyD_insertEntryIfNew
|
||||
|
||||
theorem minKeyD_insertIfNew! [TransOrd α] (h : t.WF) {k v fallback} :
|
||||
(t.insertIfNew! k v |>.minKeyD fallback) =
|
||||
t.minKey?.elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKeyD_insertIfNew h
|
||||
|
||||
theorem minKeyD_insertIfNew_le_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v fallback},
|
||||
compare (t.insertIfNew k v h.balanced |>.impl.minKeyD <| fallback)
|
||||
(t.minKeyD fallback) |>.isLE := by
|
||||
simp_to_model [minKeyD, isEmpty, insertIfNew] using List.minKeyD_insertEntryIfNew_le_minKeyD
|
||||
|
||||
theorem minKeyD_insertIfNew!_le_minKeyD [TransOrd α] (h : t.WF) :
|
||||
(he : t.isEmpty = false) → ∀ {k v fallback},
|
||||
compare (t.insertIfNew! k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKeyD_insertIfNew_le_minKeyD h
|
||||
|
||||
theorem minKeyD_insertIfNew_le_self [TransOrd α] (h : t.WF) : ∀ {k v fallback},
|
||||
compare (t.insertIfNew k v h.balanced |>.impl.minKeyD <| fallback) k |>.isLE := by
|
||||
simp_to_model [minKeyD, insertIfNew] using List.minKeyD_insertEntryIfNew_le_self
|
||||
|
||||
theorem minKeyD_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v fallback} :
|
||||
compare (t.insertIfNew! k v |>.minKeyD fallback) k |>.isLE := by
|
||||
simpa only [insertIfNew_eq_insertIfNew!] using minKeyD_insertIfNew_le_self h
|
||||
|
||||
theorem minKeyD_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) : ∀ {k f fallback},
|
||||
(t.modify k f |>.minKeyD fallback) = t.minKeyD fallback := by
|
||||
simp_to_model [minKeyD, modify] using List.minKeyD_modifyKey
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) :
|
||||
∀ {k f fallback}, (he : (t.alter k f h.balanced).impl.isEmpty = false) →
|
||||
(t.alter k f h.balanced |>.impl.minKeyD <| fallback) = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [minKeyD, alter, isEmpty, contains, get?] using List.minKeyD_alterKey_eq_self
|
||||
|
||||
theorem minKeyD_alter!_eq_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f fallback} :
|
||||
(he : (t.alter! k f).isEmpty = false) →
|
||||
(t.alter! k f |>.minKeyD fallback) = k ↔
|
||||
(f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simpa only [alter_eq_alter!] using minKeyD_alter_eq_self h
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Impl α β}
|
||||
|
||||
theorem minKeyD_modify [TransOrd α] (h : t.WF) :
|
||||
∀ {k f}, (he : (modify k f t).isEmpty = false) → ∀ {fallback},
|
||||
(modify k f t |>.minKeyD fallback) =
|
||||
if compare (t.minKeyD fallback) k = .eq then k else t.minKeyD fallback := by
|
||||
simp_to_model [minKeyD, minKey, isEmpty, Const.modify] using List.Const.minKeyD_modifyKey
|
||||
|
||||
theorem minKeyD_modify_eq_minKeyD [TransOrd α] [LawfulEqOrd α] (h : t.WF) :
|
||||
∀ {k f fallback}, (modify k f t |>.minKeyD fallback) = t.minKeyD fallback := by
|
||||
simp_to_model [minKeyD, Const.modify] using List.Const.minKeyD_modifyKey_eq_minKeyD
|
||||
|
||||
theorem compare_minKeyD_modify_eq [TransOrd α] (h : t.WF) : ∀ {k f fallback},
|
||||
compare (Const.modify k f t |>.minKeyD fallback) (t.minKeyD fallback) = .eq := by
|
||||
simp_to_model [minKeyD, Const.modify] using List.Const.minKeyD_modifyKey_beq
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransOrd α] (h : t.WF) :
|
||||
∀ {k f}, (he : (alter k f t h.balanced).impl.isEmpty = false) → ∀ {fallback},
|
||||
(alter k f t h.balanced |>.impl.minKeyD <| fallback) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simp_to_model [minKeyD, Const.alter, contains, isEmpty, Const.get?] using
|
||||
List.Const.minKeyD_alterKey_eq_self
|
||||
|
||||
theorem minKeyD_alter!_eq_self [TransOrd α] (h : t.WF) {k f} :
|
||||
(he : (alter! k f t).isEmpty = false) → ∀ {fallback},
|
||||
(alter! k f t |>.minKeyD fallback) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (compare k k').isLE := by
|
||||
simpa only [alter_eq_alter!] using minKeyD_alter_eq_self h
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -480,6 +480,10 @@ theorem minKey!_eq_get!_minKey? [Ord α] [Inhabited α] {l : Impl α β} :
|
|||
l.minKey! = l.minKey?.get! := by
|
||||
induction l using minKey!.induct <;> simp_all only [minKey!, minKey?] <;> rfl
|
||||
|
||||
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 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!,
|
||||
|
|
|
|||
|
|
@ -1837,4 +1837,9 @@ theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] {l : Impl α β
|
|||
l.minKey! = List.minKey! l.toListModel := by
|
||||
simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo]
|
||||
|
||||
theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] {l : Impl α β} (hlo : l.Ordered)
|
||||
{fallback} :
|
||||
l.minKeyD fallback = List.minKeyD l.toListModel fallback := by
|
||||
simp [Impl.minKeyD_eq_getD_minKey?, List.minKeyD_eq_getD_minKey?, minKey?_eq_minKey? hlo]
|
||||
|
||||
end Std.DTreeMap.Internal.Impl
|
||||
|
|
|
|||
|
|
@ -3236,6 +3236,140 @@ theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
|||
|
||||
end Const
|
||||
|
||||
theorem minKey?_eq_some_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.minKey? = some (t.minKeyD fallback) :=
|
||||
Impl.minKey?_eq_some_minKeyD t.wf he
|
||||
|
||||
theorem minKeyD_eq_fallback [TransCmp cmp] (he : t.isEmpty) {fallback} :
|
||||
t.minKeyD fallback = fallback :=
|
||||
Impl.minKeyD_eq_fallback t.wf he
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [TransCmp cmp] [Inhabited α] :
|
||||
t.minKey! = t.minKeyD default :=
|
||||
Impl.minKey!_eq_minKeyD_default t.wf
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKeyD_eq_iff_getKey?_eq_self_and_forall t.wf he
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKeyD_eq_some_iff_mem_and_forall t.wf he
|
||||
|
||||
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') :=
|
||||
Impl.minKeyD_insert t.wf
|
||||
|
||||
theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (he : t.isEmpty = false)
|
||||
{k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_insert_le_minKeyD t.wf he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_insert_le_self [TransCmp cmp] {k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_insert_le_self t.wf (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem contains_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minKeyD fallback) :=
|
||||
Impl.contains_minKeyD t.wf he
|
||||
|
||||
theorem minKeyD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.minKeyD fallback ∈ t :=
|
||||
Impl.minKeyD_mem t.wf he
|
||||
|
||||
theorem minKeyD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_le_of_contains t.wf hc
|
||||
|
||||
theorem minKeyD_le_of_mem [TransCmp cmp] {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_le_of_mem t.wf hc
|
||||
|
||||
theorem le_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minKeyD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKeyD t.wf he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem getKey?_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback) :=
|
||||
Impl.getKey?_minKeyD t.wf he
|
||||
|
||||
theorem getKey_minKeyD [TransCmp cmp] {fallback hc} :
|
||||
t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback :=
|
||||
Impl.getKey_minKeyD t.wf
|
||||
|
||||
theorem getKey!_minKeyD [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey! (t.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.getKey!_minKeyD t.wf he
|
||||
|
||||
theorem getKeyD_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback :=
|
||||
Impl.getKeyD_minKeyD t.wf he
|
||||
|
||||
theorem minKeyD_erase_eq_of_not_compare_minKeyD_eq [TransCmp cmp] {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minKeyD fallback) = .eq) :
|
||||
(t.erase k |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.minKeyD_erase_eq_of_not_compare_minKeyD_eq t.wf he heq
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [TransCmp cmp] {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minKeyD fallback) (t.erase k |>.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_le_minKeyD_erase t.wf he
|
||||
|
||||
theorem minKeyD_insertIfNew [TransCmp cmp] {k v fallback} :
|
||||
(t.insertIfNew k v |>.minKeyD fallback) =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
Impl.minKeyD_insertIfNew t.wf
|
||||
|
||||
theorem minKeyD_insertIfNew_le_minKeyD [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_insertIfNew_le_minKeyD t.wf he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_insertIfNew_le_self [TransCmp cmp] {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_insertIfNew_le_self t.wf (instOrd := ⟨cmp⟩)
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
|
||||
(t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.minKeyD_modify t.wf
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] {k f}
|
||||
(he : (t.alter k f).isEmpty = false) {fallback} :
|
||||
(t.alter k f |>.minKeyD fallback) = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKeyD_alter_eq_self t.wf he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : DTreeMap α β cmp}
|
||||
|
||||
theorem minKeyD_modify [TransCmp cmp] {k f}
|
||||
(he : (modify t k f).isEmpty = false) {fallback} :
|
||||
(modify t k f |>.minKeyD fallback) =
|
||||
if cmp (t.minKeyD fallback) k = .eq then k else (t.minKeyD fallback) :=
|
||||
Impl.Const.minKeyD_modify t.wf he
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
|
||||
(modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.Const.minKeyD_modify_eq_minKeyD t.wf
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
|
||||
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
|
||||
Impl.Const.compare_minKeyD_modify_eq t.wf (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
|
||||
(he : (alter t k f).isEmpty = false) {fallback} :
|
||||
(alter t k f |>.minKeyD fallback) = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKeyD_alter_eq_self t.wf he
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap
|
||||
|
|
|
|||
|
|
@ -3097,6 +3097,140 @@ theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
|||
|
||||
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
|
||||
|
||||
theorem minKeyD_eq_fallback [TransCmp cmp] (h : t.WF) (he : t.isEmpty) {fallback} :
|
||||
t.minKeyD fallback = fallback :=
|
||||
Impl.minKeyD_eq_fallback h he
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.minKey! = t.minKeyD default :=
|
||||
Impl.minKey!_eq_minKeyD_default h
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKeyD_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
Impl.minKeyD_eq_some_iff_mem_and_forall h he
|
||||
|
||||
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') :=
|
||||
Impl.minKeyD_insert! h
|
||||
|
||||
theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_insert!_le_minKeyD h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_insert_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_insert!_le_self h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem contains_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minKeyD fallback) :=
|
||||
Impl.contains_minKeyD h he
|
||||
|
||||
theorem minKeyD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.minKeyD fallback ∈ t :=
|
||||
Impl.minKeyD_mem h he
|
||||
|
||||
theorem minKeyD_le_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_le_of_contains h hc
|
||||
|
||||
theorem minKeyD_le_of_mem [TransCmp cmp] (h : t.WF) {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_le_of_mem h hc
|
||||
|
||||
theorem le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minKeyD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
Impl.le_minKeyD h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem getKey?_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback) :=
|
||||
Impl.getKey?_minKeyD h he
|
||||
|
||||
theorem getKey_minKeyD [TransCmp cmp] (h : t.WF) {fallback hc} :
|
||||
t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback :=
|
||||
Impl.getKey_minKeyD h
|
||||
|
||||
theorem getKey!_minKeyD [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey! (t.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.getKey!_minKeyD h he
|
||||
|
||||
theorem getKeyD_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback :=
|
||||
Impl.getKeyD_minKeyD h he
|
||||
|
||||
theorem minKeyD_erase_eq_of_not_compare_minKeyD_eq [TransCmp cmp] (h : t.WF) {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minKeyD fallback) = .eq) :
|
||||
(t.erase k |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.minKeyD_erase!_eq_of_not_compare_minKeyD_eq h he heq
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [TransCmp cmp] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minKeyD fallback) (t.erase k |>.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_le_minKeyD_erase! h he
|
||||
|
||||
theorem minKeyD_insertIfNew [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
(t.insertIfNew k v |>.minKeyD fallback) =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
Impl.minKeyD_insertIfNew! h
|
||||
|
||||
theorem minKeyD_insertIfNew_le_minKeyD [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
Impl.minKeyD_insertIfNew!_le_minKeyD h he (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
|
||||
Impl.minKeyD_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
|
||||
(t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.minKeyD_modify h
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f}
|
||||
(he : (t.alter k f).isEmpty = false) {fallback} :
|
||||
(t.alter k f |>.minKeyD fallback) = k ↔ (f (t.get? k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.minKeyD_alter!_eq_self h he
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v} {t : Raw α β cmp}
|
||||
|
||||
theorem minKeyD_modify [TransCmp cmp] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) {fallback} :
|
||||
(modify t k f |>.minKeyD fallback) =
|
||||
if cmp (t.minKeyD fallback) k = .eq then k else (t.minKeyD fallback) :=
|
||||
Impl.Const.minKeyD_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
|
||||
(modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
Impl.Const.minKeyD_modify_eq_minKeyD h
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
|
||||
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
|
||||
Impl.Const.compare_minKeyD_modify_eq h (instOrd := ⟨cmp⟩)
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) {fallback} :
|
||||
(alter t k f |>.minKeyD fallback) = k ↔
|
||||
(f (Const.get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
Impl.Const.minKeyD_alter!_eq_self h he
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.DTreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -5131,6 +5131,212 @@ theorem minKey!_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd
|
|||
|
||||
end Const
|
||||
|
||||
/-- Returns the smallest key in an associative list or `fallback` if the list is empty. -/
|
||||
def minKeyD [Ord α] (xs : List ((a : α) × β a)) (fallback : α) : α :=
|
||||
minKey? xs |>.getD fallback
|
||||
|
||||
theorem minKeyD_of_perm [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l l' : List ((a : α) × β a)} {fallback} (hd : DistinctKeys l) (hp : l.Perm l') :
|
||||
minKeyD l fallback = minKeyD l' fallback := by
|
||||
simp [minKeyD, minKey?_of_perm hd hp]
|
||||
|
||||
theorem minKeyD_eq_getD_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {fallback} :
|
||||
minKeyD l fallback = (minKey? l).getD fallback :=
|
||||
rfl
|
||||
|
||||
theorem minKey_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {he fallback} :
|
||||
minKey l he = minKeyD l fallback := by
|
||||
simp [minKey_eq_get_minKey?, minKeyD_eq_getD_minKey?, Option.get_eq_getD (fallback := fallback)]
|
||||
|
||||
theorem minKey?_eq_some_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {fallback} (he : l.isEmpty = false) :
|
||||
minKey? l = some (minKeyD l fallback) := by
|
||||
simp [← minKey_eq_minKeyD (he := he), minKey_eq_get_minKey?]
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} :
|
||||
minKey! l = minKeyD l default := by
|
||||
simp [minKey!_eq_get!_minKey?, minKeyD_eq_getD_minKey?, Option.get!_eq_getD]
|
||||
|
||||
theorem minKeyD_eq_fallback [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} {fallback} (h : l.isEmpty) :
|
||||
minKeyD l fallback = fallback := by
|
||||
simp [minKeyD, minKey?_eq_none_iff_isEmpty.mpr h]
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {km fallback} :
|
||||
minKeyD l fallback = km ↔
|
||||
getKey? km l = some km ∧ ∀ k, containsKey k l → (compare km k).isLE := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_eq_iff_getKey?_eq_self_and_forall hd (he := he)
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
[LawfulEqOrd α] {l : List ((a : α) × β a)} (hd : DistinctKeys l)
|
||||
(he : l.isEmpty = false) {km fallback} :
|
||||
minKeyD l fallback = km ↔ containsKey km l ∧ ∀ k, containsKey k l → (compare km k).isLE := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_eq_some_iff_mem_and_forall hd (he := he)
|
||||
|
||||
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
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntry hd
|
||||
|
||||
theorem minKeyD_insertEntry_le_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v fallback} :
|
||||
compare (insertEntry k v l |> minKeyD <| fallback) (minKeyD l fallback) |>.isLE := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntry_le_minKey hd (he := he)
|
||||
|
||||
theorem minKeyD_insertEntry_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v fallback} :
|
||||
compare (insertEntry k v l |> minKeyD <| fallback) k |>.isLE := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntry_le_self hd
|
||||
|
||||
theorem containsKey_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback} :
|
||||
containsKey (minKeyD l fallback) l := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using containsKey_minKey hd (he := he)
|
||||
|
||||
theorem minKeyD_le_of_containsKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (hc : containsKey k l) {fallback} :
|
||||
compare (minKeyD l fallback) k |>.isLE := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using minKey_le_of_containsKey hd hc
|
||||
|
||||
theorem le_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k fallback} :
|
||||
(compare k (minKeyD l fallback)).isLE ↔ (∀ k', containsKey k' l → (compare k k').isLE) := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using le_minKey hd (he := he)
|
||||
|
||||
theorem getKey?_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback} :
|
||||
getKey? (minKeyD l fallback) l = some (minKeyD l fallback) := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using getKey?_minKey hd (he := he)
|
||||
|
||||
theorem getKey_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback he} :
|
||||
getKey (minKeyD l fallback) l he = minKeyD l fallback := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
getKey_minKey hd (he := isEmpty_eq_false_of_containsKey he)
|
||||
|
||||
theorem getKey_minKeyD_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {fallback he} :
|
||||
getKey (minKeyD l fallback) l he = minKey l (isEmpty_eq_false_of_containsKey he) := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
getKey_minKey hd (he := isEmpty_eq_false_of_containsKey he)
|
||||
|
||||
theorem getKey!_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback} :
|
||||
getKey! (minKeyD l fallback) l = minKeyD l fallback := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using getKey!_minKey hd (he := he)
|
||||
|
||||
theorem getKeyD_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {fallback fallback'} :
|
||||
getKeyD (minKeyD l fallback) l fallback' = minKeyD l fallback := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using getKeyD_minKey hd (he := he)
|
||||
|
||||
theorem minKeyD_eraseKey_eq_iff_beq_minKey_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> minKeyD <| fallback) = minKeyD l fallback ↔
|
||||
(k == (minKeyD l fallback)) = false := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_eraseKey_eq_iff_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKeyD_eraseKey_eq_iff_beq_minKeyD_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback}
|
||||
(he : (eraseKey k l).isEmpty = false) :
|
||||
(eraseKey k l |> minKeyD <| fallback) = minKeyD l fallback ↔
|
||||
(k == (minKeyD l fallback)) = false := by
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_eraseKey_eq_iff_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKeyD_eraseKey_eq_of_beq_minKeyD_eq_false [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k fallback}
|
||||
(he : (eraseKey k l).isEmpty = false) : (heq : (k == minKeyD l fallback) = false) →
|
||||
(eraseKey k l |> minKeyD <| fallback) = minKeyD l fallback:= by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_eraseKey_eq_of_beq_minKey_eq_false hd (he := he)
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k} (he : (eraseKey k l).isEmpty = false)
|
||||
{fallback} :
|
||||
compare (minKeyD l fallback) (eraseKey k l |> minKeyD <| fallback) |>.isLE := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_le_minKey_erase hd (he := he)
|
||||
|
||||
theorem minKeyD_insertEntryIfNew [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v fallback} :
|
||||
(insertEntryIfNew k v l |> minKeyD <| fallback) =
|
||||
(minKey? l).elim k fun k' => if compare k k' = .lt then k else k' := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntryIfNew hd
|
||||
|
||||
theorem minKeyD_insertEntryIfNew_le_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) (he : l.isEmpty = false) {k v fallback} :
|
||||
compare (insertEntryIfNew k v l |> minKeyD <| fallback) (minKeyD l fallback) |>.isLE := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using
|
||||
minKey_insertEntryIfNew_le_minKey hd (he := he)
|
||||
|
||||
theorem minKeyD_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k v fallback} :
|
||||
compare (insertEntryIfNew k v l |> minKeyD <| fallback) k |>.isLE := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_insertEntryIfNew_le_self hd
|
||||
|
||||
theorem minKeyD_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f fallback} :
|
||||
(modifyKey k f l |> minKeyD <| fallback) = minKeyD l fallback := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKeyD_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f fallback}
|
||||
(he : (alterKey k f l).isEmpty = false) :
|
||||
(alterKey k f l |> minKeyD <| fallback) = k ↔
|
||||
(f (getValueCast? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_alterKey_eq_self hd (he := he)
|
||||
|
||||
namespace Const
|
||||
|
||||
variable {β : Type v}
|
||||
|
||||
theorem minKeyD_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (modifyKey k f l).isEmpty = false)
|
||||
{fallback} :
|
||||
(modifyKey k f l |> minKeyD <| fallback) = if (minKeyD l fallback) == k then k else (minKeyD l fallback) := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_modifyKey hd (he := he)
|
||||
|
||||
theorem minKeyD_modifyKey_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f fallback} :
|
||||
(modifyKey k f l |> minKeyD <| fallback) = minKeyD l fallback := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey_eq_minKey hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKeyD_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f fallback} :
|
||||
(modifyKey k f l |> minKeyD <| fallback) == (minKeyD l fallback) := by
|
||||
cases he : l.isEmpty
|
||||
· have := minKey_modifyKey_beq hd (he := isEmpty_modifyKey k f l ▸ he)
|
||||
-- fails after inlining `this`
|
||||
simpa [minKey_eq_minKeyD (fallback := fallback)] using this
|
||||
· simp_all [modifyKey]
|
||||
|
||||
theorem minKeyD_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
|
||||
{l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (alterKey k f l).isEmpty = false)
|
||||
{fallback} :
|
||||
(alterKey k f l |> minKeyD <| fallback) = k ↔
|
||||
(f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k k').isLE := by
|
||||
simpa only [minKey_eq_minKeyD (fallback := fallback)] using minKey_alterKey_eq_self hd (he := he)
|
||||
|
||||
end Const
|
||||
|
||||
end Min
|
||||
|
||||
end Std.Internal.List
|
||||
|
|
|
|||
|
|
@ -2156,6 +2156,124 @@ theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] {k f}
|
|||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Const.minKey!_alter_eq_self he
|
||||
|
||||
theorem minKey?_eq_some_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.minKey? = some (t.minKeyD fallback) :=
|
||||
DTreeMap.minKey?_eq_some_minKeyD he
|
||||
|
||||
theorem minKeyD_eq_fallback [TransCmp cmp] (he : t.isEmpty) {fallback} :
|
||||
t.minKeyD fallback = fallback :=
|
||||
DTreeMap.minKeyD_eq_fallback he
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [TransCmp cmp] [Inhabited α] :
|
||||
t.minKey! = t.minKeyD default :=
|
||||
DTreeMap.minKey!_eq_minKeyD_default
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.minKeyD_eq_some_iff_mem_and_forall he
|
||||
|
||||
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') :=
|
||||
DTreeMap.minKeyD_insert
|
||||
|
||||
theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (he : t.isEmpty = false)
|
||||
{k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.minKeyD_insert_le_minKeyD he
|
||||
|
||||
theorem minKeyD_insert_le_self [TransCmp cmp] {k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.minKeyD_insert_le_self
|
||||
|
||||
theorem contains_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minKeyD fallback) :=
|
||||
DTreeMap.contains_minKeyD he
|
||||
|
||||
theorem minKeyD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.minKeyD fallback ∈ t :=
|
||||
DTreeMap.minKeyD_mem he
|
||||
|
||||
theorem minKeyD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.minKeyD_le_of_contains hc
|
||||
|
||||
theorem minKeyD_le_of_mem [TransCmp cmp] {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.minKeyD_le_of_mem hc
|
||||
|
||||
theorem le_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minKeyD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.le_minKeyD he
|
||||
|
||||
theorem getKey?_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback) :=
|
||||
DTreeMap.getKey?_minKeyD he
|
||||
|
||||
theorem getKey_minKeyD [TransCmp cmp] {fallback hc} :
|
||||
t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback :=
|
||||
DTreeMap.getKey_minKeyD
|
||||
|
||||
theorem getKey!_minKeyD [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey! (t.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.getKey!_minKeyD he
|
||||
|
||||
theorem getKeyD_minKeyD [TransCmp cmp] (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback :=
|
||||
DTreeMap.getKeyD_minKeyD he
|
||||
|
||||
theorem minKeyD_erase_eq_of_not_compare_minKeyD_eq [TransCmp cmp] {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minKeyD fallback) = .eq) :
|
||||
(t.erase k |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq he heq
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [TransCmp cmp] {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minKeyD fallback) (t.erase k |>.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.minKeyD_le_minKeyD_erase he
|
||||
|
||||
theorem minKeyD_insertIfNew [TransCmp cmp] {k v fallback} :
|
||||
(t.insertIfNew k v |>.minKeyD fallback) =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.minKeyD_insertIfNew
|
||||
|
||||
theorem minKeyD_insertIfNew_le_minKeyD [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.minKeyD_insertIfNew_le_minKeyD he
|
||||
|
||||
theorem minKeyD_insertIfNew_le_self [TransCmp cmp] {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.minKeyD_insertIfNew_le_self
|
||||
|
||||
theorem minKeyD_modify [TransCmp cmp] {k f}
|
||||
(he : (modify t k f).isEmpty = false) {fallback} :
|
||||
(modify t k f |>.minKeyD fallback) =
|
||||
if cmp (t.minKeyD fallback) k = .eq then k else (t.minKeyD fallback) :=
|
||||
DTreeMap.Const.minKeyD_modify he
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
|
||||
(modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.Const.minKeyD_modify_eq_minKeyD
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKeyD_modify_eq [TransCmp cmp] {k f fallback} :
|
||||
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
|
||||
DTreeMap.Const.compare_minKeyD_modify_eq
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] {k f}
|
||||
(he : (alter t k f).isEmpty = false) {fallback} :
|
||||
(alter t k f |>.minKeyD fallback) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Const.minKeyD_alter_eq_self he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap
|
||||
|
|
|
|||
|
|
@ -2038,6 +2038,124 @@ theorem minKey!_alter_eq_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
|
|||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Raw.Const.minKey!_alter_eq_self h he
|
||||
|
||||
theorem minKey?_eq_some_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.minKey? = some (t.minKeyD fallback) :=
|
||||
DTreeMap.Raw.minKey?_eq_some_minKeyD h he
|
||||
|
||||
theorem minKeyD_eq_fallback [TransCmp cmp] (h : t.WF) (he : t.isEmpty) {fallback} :
|
||||
t.minKeyD fallback = fallback :=
|
||||
DTreeMap.Raw.minKeyD_eq_fallback h he
|
||||
|
||||
theorem minKey!_eq_minKeyD_default [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.minKey! = t.minKeyD default :=
|
||||
DTreeMap.Raw.minKey!_eq_minKeyD_default h
|
||||
|
||||
theorem minKeyD_eq_iff_getKey?_eq_self_and_forall [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKeyD_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem minKeyD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minKeyD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKeyD_eq_some_iff_mem_and_forall h he
|
||||
|
||||
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') :=
|
||||
DTreeMap.Raw.minKeyD_insert h
|
||||
|
||||
theorem minKeyD_insert_le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false)
|
||||
{k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insert_le_minKeyD h he
|
||||
|
||||
theorem minKeyD_insert_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
cmp (t.insert k v |>.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insert_le_self h
|
||||
|
||||
theorem contains_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minKeyD fallback) :=
|
||||
DTreeMap.Raw.contains_minKeyD h he
|
||||
|
||||
theorem minKeyD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.minKeyD fallback ∈ t :=
|
||||
DTreeMap.Raw.minKeyD_mem h he
|
||||
|
||||
theorem minKeyD_le_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_of_contains h hc
|
||||
|
||||
theorem minKeyD_le_of_mem [TransCmp cmp] (h : t.WF) {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_of_mem h hc
|
||||
|
||||
theorem le_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minKeyD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.Raw.le_minKeyD h he
|
||||
|
||||
theorem getKey?_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey? (t.minKeyD fallback) = some (t.minKeyD fallback) :=
|
||||
DTreeMap.Raw.getKey?_minKeyD h he
|
||||
|
||||
theorem getKey_minKeyD [TransCmp cmp] (h : t.WF) {fallback hc} :
|
||||
t.getKey (t.minKeyD fallback) hc = t.minKeyD fallback :=
|
||||
DTreeMap.Raw.getKey_minKeyD h
|
||||
|
||||
theorem getKey!_minKeyD [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.getKey! (t.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.Raw.getKey!_minKeyD h he
|
||||
|
||||
theorem getKeyD_minKeyD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getKeyD (t.minKeyD fallback) fallback' = t.minKeyD fallback :=
|
||||
DTreeMap.Raw.getKeyD_minKeyD h he
|
||||
|
||||
theorem minKeyD_erase_eq_of_not_compare_minKeyD_eq [TransCmp cmp] (h : t.WF) {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minKeyD fallback) = .eq) :
|
||||
(t.erase k |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.Raw.minKeyD_erase_eq_of_not_compare_minKeyD_eq h he heq
|
||||
|
||||
theorem minKeyD_le_minKeyD_erase [TransCmp cmp] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minKeyD fallback) (t.erase k |>.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_minKeyD_erase h he
|
||||
|
||||
theorem minKeyD_insertIfNew [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
(t.insertIfNew k v |>.minKeyD fallback) =
|
||||
t.minKey?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew h
|
||||
|
||||
theorem minKeyD_insertIfNew_le_minKeyD [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) (t.minKeyD fallback) |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew_le_minKeyD h he
|
||||
|
||||
theorem minKeyD_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v fallback} :
|
||||
cmp (t.insertIfNew k v |>.minKeyD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew_le_self h
|
||||
|
||||
theorem minKeyD_modify [TransCmp cmp] (h : t.WF) {k f}
|
||||
(he : (modify t k f).isEmpty = false) {fallback} :
|
||||
(modify t k f |>.minKeyD fallback) =
|
||||
if cmp (t.minKeyD fallback) k = .eq then k else (t.minKeyD fallback) :=
|
||||
DTreeMap.Raw.Const.minKeyD_modify h he
|
||||
|
||||
@[simp]
|
||||
theorem minKeyD_modify_eq_minKeyD [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
|
||||
(modify t k f |>.minKeyD fallback) = t.minKeyD fallback :=
|
||||
DTreeMap.Raw.Const.minKeyD_modify_eq_minKeyD h
|
||||
|
||||
@[simp]
|
||||
theorem compare_minKeyD_modify_eq [TransCmp cmp] (h : t.WF) {k f fallback} :
|
||||
cmp (modify t k f |>.minKeyD fallback) (t.minKeyD fallback) = .eq :=
|
||||
DTreeMap.Raw.Const.compare_minKeyD_modify_eq h
|
||||
|
||||
theorem minKeyD_alter_eq_self [TransCmp cmp] (h : t.WF) {k f}
|
||||
(he : (alter t k f).isEmpty = false) {fallback} :
|
||||
(alter t k f |>.minKeyD fallback) = k ↔
|
||||
(f (get? t k)).isSome ∧ ∀ k', k' ∈ t → (cmp k k').isLE :=
|
||||
DTreeMap.Raw.Const.minKeyD_alter_eq_self h he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeMap.Raw
|
||||
|
|
|
|||
|
|
@ -954,6 +954,88 @@ theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] {k}
|
|||
cmp t.min! (t.erase k |>.min!) |>.isLE :=
|
||||
DTreeMap.minKey!_le_minKey!_erase he
|
||||
|
||||
theorem min?_eq_some_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.min? = some (t.minD fallback) :=
|
||||
TreeMap.minKey?_eq_some_minKeyD he
|
||||
|
||||
theorem minD_eq_fallback [TransCmp cmp] (he : t.isEmpty) {fallback} :
|
||||
t.minD fallback = fallback :=
|
||||
TreeMap.minKeyD_eq_fallback he
|
||||
|
||||
theorem min!_eq_minD_default [TransCmp cmp] [Inhabited α] :
|
||||
t.min! = t.minD default :=
|
||||
TreeMap.minKey!_eq_minKeyD_default
|
||||
|
||||
theorem minD_eq_iff_get?_eq_self_and_forall [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
TreeMap.minKeyD_eq_iff_getKey?_eq_self_and_forall he
|
||||
|
||||
theorem minD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp]
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
TreeMap.minKeyD_eq_some_iff_mem_and_forall he
|
||||
|
||||
theorem minD_insert [TransCmp cmp] {k fallback} :
|
||||
(t.insert k |>.minD fallback) =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
TreeMap.minKeyD_insertIfNew
|
||||
|
||||
theorem minD_insert_le_minD [TransCmp cmp]
|
||||
(he : t.isEmpty = false) {k fallback} :
|
||||
cmp (t.insert k |>.minD fallback) (t.minD fallback) |>.isLE :=
|
||||
TreeMap.minKeyD_insertIfNew_le_minKeyD he
|
||||
|
||||
theorem minD_insert_le_self [TransCmp cmp] {k fallback} :
|
||||
cmp (t.insert k |>.minD fallback) k |>.isLE :=
|
||||
TreeMap.minKeyD_insertIfNew_le_self
|
||||
|
||||
theorem contains_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minD fallback) :=
|
||||
TreeMap.contains_minKeyD he
|
||||
|
||||
theorem minD_mem [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.minD fallback ∈ t :=
|
||||
TreeMap.minKeyD_mem he
|
||||
|
||||
theorem minD_le_of_contains [TransCmp cmp] {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minD fallback) k |>.isLE :=
|
||||
TreeMap.minKeyD_le_of_contains hc
|
||||
|
||||
theorem minD_le_of_mem [TransCmp cmp] {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minD fallback) k |>.isLE :=
|
||||
TreeMap.minKeyD_le_of_mem hc
|
||||
|
||||
theorem le_minD [TransCmp cmp] (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
TreeMap.le_minKeyD he
|
||||
|
||||
theorem get?_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
|
||||
t.get? (t.minD fallback) = some (t.minD fallback) :=
|
||||
TreeMap.getKey?_minKeyD he
|
||||
|
||||
theorem get_minD [TransCmp cmp] {fallback hc} :
|
||||
t.get (t.minD fallback) hc = t.minD fallback :=
|
||||
TreeMap.getKey_minKeyD
|
||||
|
||||
theorem get!_minD [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) {fallback} :
|
||||
t.get! (t.minD fallback) = t.minD fallback :=
|
||||
TreeMap.getKey!_minKeyD he
|
||||
|
||||
theorem getD_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getD (t.minD fallback) fallback' = t.minD fallback :=
|
||||
TreeMap.getKeyD_minKeyD he
|
||||
|
||||
theorem minD_erase_eq_of_not_compare_minD_eq [TransCmp cmp] {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minD fallback) = .eq) :
|
||||
(t.erase k |>.minD fallback) = t.minD fallback :=
|
||||
TreeMap.minKeyD_erase_eq_of_not_compare_minKeyD_eq he heq
|
||||
|
||||
theorem minD_le_minD_erase [TransCmp cmp] {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
|
||||
TreeMap.minKeyD_le_minKeyD_erase he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeSet
|
||||
|
|
|
|||
|
|
@ -860,6 +860,88 @@ theorem min!_le_min!_erase [TransCmp cmp] [Inhabited α] (h : t.WF) {k}
|
|||
cmp t.min! (t.erase k |>.min!) |>.isLE :=
|
||||
DTreeMap.Raw.minKey!_le_minKey!_erase h he
|
||||
|
||||
theorem min?_eq_some_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.min? = some (t.minD fallback) :=
|
||||
DTreeMap.Raw.minKey?_eq_some_minKeyD h he
|
||||
|
||||
theorem minD_eq_fallback [TransCmp cmp] (h : t.WF) (he : t.isEmpty) {fallback} :
|
||||
t.minD fallback = fallback :=
|
||||
DTreeMap.Raw.minKeyD_eq_fallback h he
|
||||
|
||||
theorem min!_eq_minD_default [TransCmp cmp] [Inhabited α] (h : t.WF) :
|
||||
t.min! = t.minD default :=
|
||||
DTreeMap.Raw.minKey!_eq_minKeyD_default h
|
||||
|
||||
theorem minD_eq_iff_get?_eq_self_and_forall [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKeyD_eq_iff_getKey?_eq_self_and_forall h he
|
||||
|
||||
theorem minD_eq_some_iff_mem_and_forall [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {km fallback} :
|
||||
t.minD fallback = km ↔ km ∈ t ∧ ∀ k, k ∈ t → (cmp km k).isLE :=
|
||||
DTreeMap.Raw.minKeyD_eq_some_iff_mem_and_forall h he
|
||||
|
||||
theorem minD_insert [TransCmp cmp] (h : t.WF) {k fallback} :
|
||||
(t.insert k |>.minD fallback) =
|
||||
t.min?.elim k fun k' => if cmp k k' = .lt then k else k' :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew h
|
||||
|
||||
theorem minD_insert_le_minD [TransCmp cmp] (h : t.WF)
|
||||
(he : t.isEmpty = false) {k fallback} :
|
||||
cmp (t.insert k |>.minD fallback) (t.minD fallback) |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew_le_minKeyD h he
|
||||
|
||||
theorem minD_insert_le_self [TransCmp cmp] (h : t.WF) {k fallback} :
|
||||
cmp (t.insert k |>.minD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_insertIfNew_le_self h
|
||||
|
||||
theorem contains_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.contains (t.minD fallback) :=
|
||||
DTreeMap.Raw.contains_minKeyD h he
|
||||
|
||||
theorem minD_mem [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.minD fallback ∈ t :=
|
||||
DTreeMap.Raw.minKeyD_mem h he
|
||||
|
||||
theorem minD_le_of_contains [TransCmp cmp] (h : t.WF) {k} (hc : t.contains k) {fallback} :
|
||||
cmp (t.minD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_of_contains h hc
|
||||
|
||||
theorem minD_le_of_mem [TransCmp cmp] (h : t.WF) {k} (hc : k ∈ t) {fallback} :
|
||||
cmp (t.minD fallback) k |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_of_mem h hc
|
||||
|
||||
theorem le_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {k fallback} :
|
||||
(cmp k (t.minD fallback)).isLE ↔ (∀ k', k' ∈ t → (cmp k k').isLE) :=
|
||||
DTreeMap.Raw.le_minKeyD h he
|
||||
|
||||
theorem get?_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.get? (t.minD fallback) = some (t.minD fallback) :=
|
||||
DTreeMap.Raw.getKey?_minKeyD h he
|
||||
|
||||
theorem get_minD [TransCmp cmp] (h : t.WF) {fallback hc} :
|
||||
t.get (t.minD fallback) hc = t.minD fallback :=
|
||||
DTreeMap.Raw.getKey_minKeyD h
|
||||
|
||||
theorem get!_minD [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) {fallback} :
|
||||
t.get! (t.minD fallback) = t.minD fallback :=
|
||||
DTreeMap.Raw.getKey!_minKeyD h he
|
||||
|
||||
theorem getD_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback fallback'} :
|
||||
t.getD (t.minD fallback) fallback' = t.minD fallback :=
|
||||
DTreeMap.Raw.getKeyD_minKeyD h he
|
||||
|
||||
theorem minD_erase_eq_of_not_compare_minD_eq [TransCmp cmp] (h : t.WF) {k fallback}
|
||||
(he : (t.erase k).isEmpty = false) (heq : ¬ cmp k (t.minD fallback) = .eq) :
|
||||
(t.erase k |>.minD fallback) = t.minD fallback :=
|
||||
DTreeMap.Raw.minKeyD_erase_eq_of_not_compare_minKeyD_eq h he heq
|
||||
|
||||
theorem minD_le_minD_erase [TransCmp cmp] (h : t.WF) {k}
|
||||
(he : (t.erase k).isEmpty = false) {fallback} :
|
||||
cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
|
||||
DTreeMap.Raw.minKeyD_le_minKeyD_erase h he
|
||||
|
||||
end Min
|
||||
|
||||
end Std.TreeSet.Raw
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue