max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: add missing treemap lemmas (#7674)

Browse source 
This PR add missing lemmas about the tree map: `minKey*` variants return
the head of `keys`, `keys` and `toList` are ordered and `getKey*
t.minKey?` equals the minimum.

---------

Co-authored-by: Paul Reichert <datokrat@users.noreply.github.com>
This commit is contained in:
Paul Reichert 2025-03-25 11:27:47 +01:00 • committed by GitHub
parent 69a03ba00b
commit 44365811cc
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
8 changed files with 298 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

42
src/Std/Data/DTreeMap/Internal/Lemmas.lean
View file

@ -1560,6 +1560,11 @@ theorem distinct_keys [TransOrd α] (h : t.WF) :
t.keys.Pairwise (fun a b => ¬ compare a b = .eq) := by
simp_to_model [keys] using h.ordered.distinctKeys.distinct
theorem ordered_keys [TransOrd α] (h : t.WF) :
t.keys.Pairwise (fun a b => compare a b = .lt) := by
simp_to_model; simp only [keys_eq_map]
exact h.ordered.map _ fun _ _ hcmp => hcmp
theorem map_fst_toList_eq_keys :
t.toList.map Sigma.fst = t.keys := by
simp_to_model [toList, keys] using (List.keys_eq_map ..).symm
@ -1593,6 +1598,10 @@ theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
t.toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
simp_to_model [toList] using List.pairwise_fst_eq_false
theorem ordered_keys_toList [TransOrd α] (h : t.WF) :
t.toList.Pairwise (fun a b => compare a.1 b.1 = .lt) := by
simp_to_model [toList] using h.ordered
namespace Const
variable {β : Type v} {t : Impl α β}
@ -1642,6 +1651,11 @@ theorem distinct_keys_toList [TransOrd α] (h : t.WF) :
(toList t).Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by
simp_to_model [Const.toList] using List.pairwise_fst_eq_false_map_toProd
theorem ordered_keys_toList [TransOrd α] (h : t.WF) :
(toList t).Pairwise (fun a b => compare a.1 b.1 = .lt) := by
simp_to_model
exact h.ordered.map _ fun _ _ hcmp => hcmp
end Const
section monadic
@ -4350,6 +4364,18 @@ theorem getKey?_minKey? [TransOrd α] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey? km = some km := by
simp_to_model using List.getKey?_minKey?
theorem getKey_minKey? [TransOrd α] (h : t.WF) {km hc} :
(hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km := by
simp_to_model using List.getKey_minKey?
theorem getKey!_minKey? [TransOrd α] [Inhabited α] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey! km = km := by
simp_to_model using List.getKey!_minKey?
theorem getKeyD_minKey? [TransOrd α] (h : t.WF) {km fallback} :
(hkm : t.minKey? = some km) → t.getKeyD km fallback = km := by
simp_to_model using List.getKeyD_minKey?
@[simp]
theorem minKey?_bind_getKey? [TransOrd α] (h : t.WF) :
t.minKey?.bind t.getKey? = t.minKey? := by
@ -4440,6 +4466,10 @@ theorem minKey?_insertIfNew!_le_self [TransOrd α] (h : t.WF) {k v kmi} :
compare kmi k |>.isLE := by
simpa only [insertIfNew_eq_insertIfNew!] using minKey?_insertIfNew_le_self h
theorem minKey?_eq_head?_keys [TransOrd α] (h : t.WF) :
t.minKey? = t.keys.head? := by
simp_to_model [minKey?, keys] using List.minKey?_eq_head?_keys h.ordered
theorem minKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) :
(t.modify k f).minKey? = t.minKey? := by
simp_to_model [modify] using List.minKey?_modifyKey
@ -4590,6 +4620,10 @@ theorem minKey_insertIfNew_le_self [TransOrd α] (h : t.WF) {k v} :
compare (t.insertIfNew k v h.balanced |>.impl.minKey <| isEmpty_insertIfNew h) k |>.isLE := by
simp_to_model [minKey, insertIfNew] using List.minKey_insertEntryIfNew_le_self
theorem minKey_eq_head_keys [TransOrd α] (h : t.WF) {he} :
t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by
simp_to_model [minKey, keys] using List.minKey_eq_head_keys h.ordered
theorem minKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} :
(t.modify k f).minKey he = t.minKey (isEmpty_modify h ▸ he):= by
simp_to_model [minKey, modify] using List.minKey_modifyKey
@ -4784,6 +4818,10 @@ theorem minKey!_insertIfNew!_le_self [TransOrd α] [Inhabited α] (h : t.WF) {k
compare (t.insertIfNew! k v |>.minKey!) k |>.isLE := by
simpa only [insertIfNew_eq_insertIfNew!] using minKey!_insertIfNew_le_self h
theorem minKey!_eq_head!_keys [TransOrd α] [Inhabited α] (h : t.WF) :
t.minKey! = t.keys.head! := by
simp_to_model [minKey!, keys] using List.minKey!_eq_head!_keys h.ordered
theorem minKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f},
(t.modify k f |>.minKey!) = t.minKey! := by
simp_to_model [minKey!, modify] using List.minKey!_modifyKey
@ -4997,6 +5035,10 @@ 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_eq_headD_keys [TransOrd α] (h : t.WF) {fallback} :
t.minKeyD fallback = t.keys.headD fallback := by
simp_to_model [minKeyD, keys] using List.minKeyD_eq_headD_keys h.ordered
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

40
src/Std/Data/DTreeMap/Lemmas.lean
View file

@ -1015,6 +1015,10 @@ theorem distinct_keys [TransCmp cmp] :
t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
Impl.distinct_keys t.wf
theorem ordered_keys [TransCmp cmp] :
t.keys.Pairwise (fun a b => cmp a b = .lt) :=
Impl.ordered_keys t.wf
@[simp]
theorem map_fst_toList_eq_keys :
t.toList.map Sigma.fst = t.keys :=
@ -1052,6 +1056,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
Impl.distinct_keys_toList t.wf
theorem ordered_keys_toList [TransCmp cmp] :
t.toList.Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
Impl.ordered_keys_toList t.wf
namespace Const
variable {β : Type v} {t : DTreeMap α β cmp}
@ -1103,6 +1111,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
(toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
Impl.Const.distinct_keys_toList t.wf
theorem ordered_keys_toList [TransCmp cmp] :
(toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
Impl.Const.ordered_keys_toList t.wf
end Const
section monadic
@ -2871,6 +2883,18 @@ theorem getKey?_minKey? [TransCmp cmp] {km} :
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
Impl.getKey?_minKey? t.wf
theorem getKey_minKey? [TransCmp cmp] {km hc} :
(hkm : t.minKey?.get (isSome_minKey?_of_contains hc) = km) → t.getKey km hc = km :=
Impl.getKey_minKey? t.wf
theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] {km} :
(hkm : t.minKey? = some km) → t.getKey! km = km :=
Impl.getKey!_minKey? t.wf
theorem getKeyD_minKey? [TransCmp cmp] {km fallback} :
(hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
Impl.getKeyD_minKey? t.wf
@[simp]
theorem minKey?_bind_getKey? [TransCmp cmp] :
t.minKey?.bind t.getKey? = t.minKey? :=
@ -2918,6 +2942,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
cmp kmi k |>.isLE :=
Impl.minKey?_insertIfNew_le_self t.wf
theorem minKey?_eq_head?_keys [TransCmp cmp] :
t.minKey? = t.keys.head? :=
Impl.minKey?_eq_head?_keys t.wf
@[simp]
theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} :
(t.modify k f).minKey? = t.minKey? :=
@ -3064,6 +3092,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
cmp (t.insertIfNew k v |>.minKey <| isEmpty_insertIfNew) k |>.isLE :=
Impl.minKey_insertIfNew_le_self t.wf
theorem minKey_eq_head_keys [TransCmp cmp] {he} :
t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
Impl.minKey_eq_head_keys t.wf
@[simp]
theorem minKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} :
(t.modify k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) :=
@ -3199,6 +3231,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
Impl.minKey!_insertIfNew_le_self t.wf
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
t.minKey! = t.keys.head! :=
Impl.minKey!_eq_head!_keys t.wf
@[simp]
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} :
(t.modify k f |>.minKey!) = t.minKey! :=
@ -3332,6 +3368,10 @@ 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⟩)
theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} :
t.minKeyD fallback = t.keys.headD fallback :=
Impl.minKeyD_eq_headD_keys t.wf
@[simp]
theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} :
(t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=

36
src/Std/Data/DTreeMap/Raw/Lemmas.lean
View file

@ -1025,6 +1025,10 @@ theorem distinct_keys [TransCmp cmp] (h : t.WF) :
t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
Impl.distinct_keys h.out
theorem ordered_keys [TransCmp cmp] (h : t.WF) :
t.keys.Pairwise (fun a b => cmp a b = .lt) :=
Impl.ordered_keys h.out
@[simp]
theorem map_fst_toList_eq_keys :
t.toList.map Sigma.fst = t.keys :=
@ -1062,6 +1066,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
Impl.distinct_keys_toList h.out
theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
t.toList.Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
Impl.ordered_keys_toList h.out
namespace Const
variable {β : Type v} {t : Raw α β cmp}
@ -1114,6 +1122,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
(toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
Impl.Const.distinct_keys_toList h.out
theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
(toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
Impl.Const.ordered_keys_toList h.out
end Const
section monadic
@ -2876,6 +2888,18 @@ theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
Impl.getKey?_minKey? h
theorem getKey_minKey? [TransCmp cmp] (h : t.WF) {km hc} :
(hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km :=
Impl.getKey_minKey? h
theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey! km = km :=
Impl.getKey!_minKey? h
theorem getKeyD_minKey? [TransCmp cmp] (h : t.WF) {km fallback} :
(hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
Impl.getKeyD_minKey? h
@[simp]
theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
t.minKey?.bind t.getKey? = t.minKey? :=
@ -2923,6 +2947,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
cmp kmi k |>.isLE :=
Impl.minKey?_insertIfNew!_le_self h
theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
t.minKey? = t.keys.head? :=
Impl.minKey?_eq_head?_keys h
@[simp]
theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) :
(t.modify k f).minKey? = t.minKey? :=
@ -3060,6 +3088,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
Impl.minKey!_insertIfNew!_le_self h (instOrd := ⟨cmp⟩)
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.minKey! = t.keys.head! :=
Impl.minKey!_eq_head!_keys h
@[simp]
theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} :
(t.modify k f |>.minKey!) = t.minKey! :=
@ -3193,6 +3225,10 @@ 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⟩)
theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
t.minKeyD fallback = t.keys.headD fallback :=
Impl.minKeyD_eq_headD_keys h
@[simp]
theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} :
(t.modify k f |>.minKeyD fallback) = t.minKeyD fallback :=

61
src/Std/Data/Internal/List/Associative.lean
View file

@ -4500,6 +4500,34 @@ theorem getKey?_minKey? [Ord α] [TransOrd α] [BEq α] [BEq α] [LawfulBEqOrd
getKey? km l = some km := by
simp_all [minKey?_eq_some_iff_getKey?_eq_self_and_forall hd]
private theorem Option.get_eq_iff_eq_some {o : Option α} {h k} :
o.get h = k ↔ o = some k := by
simp [Option.eq_some_iff_get_eq, exists_prop_of_true h]
private theorem Option.eq_get_iff_some_eq {o : Option α} {h k} :
k = o.get h ↔ some k = o := by
conv => congr <;> rw [eq_comm]
exact get_eq_iff_eq_some
theorem getKey_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {km hc} :
(hkm : (minKey? l |>.get <| isSome_minKey?_of_containsKey hc) = km) → getKey km l hc = km := by
have := (Option.eq_some_iff_get_eq.mp <| getKey?_eq_some_getKey hc).2
simp only [← this, Option.get_eq_iff_eq_some]
exact getKey?_minKey? hd
theorem getKey!_minKey? [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {km} :
(hkm : minKey? l = some km) → getKey! km l = km := by
intro h
simp [getKey!_eq_getKey?, getKey?_minKey? hd h]
theorem getKeyD_minKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {km fallback} :
(hkm : minKey? l = some km) → getKeyD km l fallback = km := by
intro h
simp [getKeyD_eq_getKey?, getKey?_minKey? hd h]
theorem minKey?_bind_getKey? [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
(minKey? l |>.bind fun k => getKey? k l) = minKey? l := by
@ -4665,6 +4693,11 @@ theorem minKey?_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
rw [OrientedCmp.eq_swap (cmp := compare)]
simp_all
theorem minKey?_eq_head?_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) :
minKey? l = (keys l).head? := by
simp [minKey?, minEntry?_eq_head? ho, keys_eq_map]
theorem minKey?_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
{l : List ((a : α) × β a)} (hd : DistinctKeys l) :
minKey? (modifyKey k f l) = minKey? l := by
@ -4785,15 +4818,6 @@ theorem minKey?_eq_some_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
minKey? l = some (minKey l he) := by
simp [minKey_eq_get_minKey?]
private theorem Option.get_eq_iff_eq_some {o : Option α} {h k} :
o.get h = k ↔ o = some k := by
simp [Option.eq_some_iff_get_eq, exists_prop_of_true h]
private theorem Option.eq_get_iff_some_eq {o : Option α} {h k} :
k = o.get h ↔ some k = o := by
conv => congr <;> rw [eq_comm]
exact get_eq_iff_eq_some
theorem minKey_eq_iff_getKey?_eq_self_and_forall [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he km} :
minKey l he = km ↔ getKey? km l = some km ∧ ∀ k, containsKey k l → (compare km k).isLE := by
@ -4903,6 +4927,12 @@ theorem minKey_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [LawfulB
compare (insertEntryIfNew k v l |> minKey <| isEmpty_insertEntryIfNew) k |>.isLE :=
minKey?_insertEntryIfNew_le_self hd minKey_eq_get_minKey?.symm
theorem minKey_eq_head_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {he} :
minKey l he = (keys l).head (by simp_all [keys_eq_map, List.isEmpty_eq_false_iff]) := by
simp [minKey_eq_get_minKey?, Option.get_eq_iff_eq_some, ← List.head?_eq_head,
minKey?_eq_head?_keys ho]
theorem minKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f}
{l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} :
(modifyKey k f l |> minKey <| he) = minKey l (isEmpty_modifyKey k f l ▸ he):= by
@ -5080,6 +5110,14 @@ theorem minKey!_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
compare (insertEntryIfNew k v l |> minKey!) k |>.isLE := by
simpa only [minKey_eq_minKey!] using minKey_insertEntryIfNew_le_self hd
theorem minKey!_eq_head!_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α]
{l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) :
minKey! l = (keys l).head! := by
cases l
· rfl
· simp only [minKey!_eq_get!_minKey?, minKey?_eq_head?_keys ho]
rfl
theorem minKey!_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α]
[Inhabited α] {l : List ((a : α) × β a)} (hd : DistinctKeys l) {k f} :
(modifyKey k f l |> minKey!) = minKey! l := by
@ -5284,6 +5322,11 @@ theorem minKeyD_insertEntryIfNew_le_self [Ord α] [TransOrd α] [BEq α] [Lawful
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_eq_headD_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α]
{l : List ((a : α) × β a)} (ho : l.Pairwise fun a b => compare a.1 b.1 = .lt) {fallback} :
minKeyD l fallback = (keys l).headD fallback := by
simp [minKeyD_eq_getD_minKey?, minKey?_eq_head?_keys ho]
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

36
src/Std/Data/TreeMap/Lemmas.lean
View file

@ -753,6 +753,10 @@ theorem distinct_keys [TransCmp cmp] :
t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
DTreeMap.distinct_keys
theorem ordered_keys [TransCmp cmp] :
t.keys.Pairwise (fun a b => cmp a b = .lt) :=
DTreeMap.ordered_keys
@[simp]
theorem map_fst_toList_eq_keys :
(toList t).map Prod.fst = t.keys :=
@ -801,6 +805,10 @@ theorem distinct_keys_toList [TransCmp cmp] :
(toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
DTreeMap.Const.distinct_keys_toList
theorem ordered_keys_toList [TransCmp cmp] :
(toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
DTreeMap.Const.ordered_keys_toList
section monadic
variable {δ : Type w} {m : Type w → Type w}
@ -1840,6 +1848,18 @@ theorem getKey?_minKey? [TransCmp cmp] {km} :
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
DTreeMap.getKey?_minKey?
theorem getKey_minKey? [TransCmp cmp] {km hc} :
(hkm : t.minKey?.get (isSome_minKey?_of_contains hc) = km) → t.getKey km hc = km :=
DTreeMap.getKey_minKey?
theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] {km} :
(hkm : t.minKey? = some km) → t.getKey! km = km :=
DTreeMap.getKey!_minKey?
theorem getKeyD_minKey? [TransCmp cmp] {km fallback} :
(hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
DTreeMap.getKeyD_minKey?
@[simp]
theorem minKey?_bind_getKey? [TransCmp cmp] :
t.minKey?.bind t.getKey? = t.minKey? :=
@ -1887,6 +1907,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} :
cmp kmi k |>.isLE :=
DTreeMap.minKey?_insertIfNew_le_self
theorem minKey?_eq_head?_keys [TransCmp cmp] :
t.minKey? = t.keys.head? :=
DTreeMap.minKey?_eq_head?_keys
theorem minKey?_modify [TransCmp cmp] {k f} :
(t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
DTreeMap.Const.minKey?_modify
@ -2017,6 +2041,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} :
cmp (t.insertIfNew k v |>.minKey <| isEmpty_insertIfNew) k |>.isLE :=
DTreeMap.minKey_insertIfNew_le_self
theorem minKey_eq_head_keys [TransCmp cmp] {he} :
t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) :=
DTreeMap.minKey_eq_head_keys
theorem minKey_modify [TransCmp cmp] {k f he} :
(modify t k f).minKey he =
if cmp (t.minKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then
@ -2135,6 +2163,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} :
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
DTreeMap.minKey!_insertIfNew_le_self
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] :
t.minKey! = t.keys.head! :=
DTreeMap.minKey!_eq_head!_keys
theorem minKey!_modify [TransCmp cmp] [Inhabited α] {k f}
(he : (modify t k f).isEmpty = false) :
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
@ -2252,6 +2284,10 @@ 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_eq_headD_keys [TransCmp cmp] {fallback} :
t.minKeyD fallback = t.keys.headD fallback :=
DTreeMap.minKeyD_eq_headD_keys
theorem minKeyD_modify [TransCmp cmp] {k f}
(he : (modify t k f).isEmpty = false) {fallback} :
(modify t k f |>.minKeyD fallback) =

32
src/Std/Data/TreeMap/Raw/Lemmas.lean
View file

@ -761,6 +761,10 @@ theorem distinct_keys [TransCmp cmp] (h : t.WF) :
t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) :=
DTreeMap.Raw.distinct_keys h
theorem ordered_keys [TransCmp cmp] (h : t.WF) :
t.keys.Pairwise (fun a b => cmp a b = .lt) :=
DTreeMap.Raw.ordered_keys h
@[simp]
theorem map_fst_toList_eq_keys :
(toList t).map Prod.fst = t.keys :=
@ -810,6 +814,10 @@ theorem distinct_keys_toList [TransCmp cmp] (h : t.WF) :
(toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) :=
DTreeMap.Raw.Const.distinct_keys_toList h
theorem ordered_keys_toList [TransCmp cmp] (h : t.WF) :
(toList t).Pairwise (fun a b => cmp a.1 b.1 = .lt) :=
DTreeMap.Raw.Const.ordered_keys_toList h
section monadic
variable {δ : Type w} {m : Type w → Type w}
@ -1849,6 +1857,18 @@ theorem getKey?_minKey? [TransCmp cmp] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey? km = some km :=
DTreeMap.Raw.getKey?_minKey? h
theorem getKey_minKey? [TransCmp cmp] (h : t.WF) {km hc} :
(hkm : t.minKey?.get (isSome_minKey?_of_contains h hc) = km) → t.getKey km hc = km :=
DTreeMap.Raw.getKey_minKey? h
theorem getKey!_minKey? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
(hkm : t.minKey? = some km) → t.getKey! km = km :=
DTreeMap.Raw.getKey!_minKey? h
theorem getKeyD_minKey? [TransCmp cmp] (h : t.WF) {km fallback} :
(hkm : t.minKey? = some km) → t.getKeyD km fallback = km :=
DTreeMap.Raw.getKeyD_minKey? h
@[simp]
theorem minKey?_bind_getKey? [TransCmp cmp] (h : t.WF) :
t.minKey?.bind t.getKey? = t.minKey? :=
@ -1896,6 +1916,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] (h : t.WF) {k v kmi} :
cmp kmi k |>.isLE :=
DTreeMap.Raw.minKey?_insertIfNew_le_self h
theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) :
t.minKey? = t.keys.head? :=
DTreeMap.Raw.minKey?_eq_head?_keys h
theorem minKey?_modify [TransCmp cmp] (h : t.WF) {k f} :
(t.modify k f).minKey? = t.minKey?.map fun km => if cmp km k = .eq then k else km :=
DTreeMap.Raw.Const.minKey?_modify h
@ -2017,6 +2041,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k
cmp (t.insertIfNew k v |>.minKey!) k |>.isLE :=
DTreeMap.Raw.minKey!_insertIfNew_le_self h
theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.minKey! = t.keys.head! :=
DTreeMap.Raw.minKey!_eq_head!_keys h
theorem minKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f}
(he : (modify t k f).isEmpty = false) :
(modify t k f |> minKey!) = if cmp t.minKey! k = .eq then k else t.minKey! :=
@ -2134,6 +2162,10 @@ 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_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} :
t.minKeyD fallback = t.keys.headD fallback :=
DTreeMap.Raw.minKeyD_eq_headD_keys 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) =

32
src/Std/Data/TreeSet/Lemmas.lean
View file

@ -425,6 +425,10 @@ theorem distinct_toList [TransCmp cmp] :
t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
DTreeMap.distinct_keys
theorem ordered_toList [TransCmp cmp] :
t.toList.Pairwise (fun a b => cmp a b = .lt) :=
DTreeMap.ordered_keys
section monadic
variable {δ : Type w} {m : Type w → Type w}
@ -757,6 +761,18 @@ theorem get?_min? [TransCmp cmp] {km} :
(hkm : t.min? = some km) → t.get? km = some km :=
DTreeMap.getKey?_minKey?
theorem get_min? [TransCmp cmp] {km hc} :
(hkm : t.min?.get (isSome_min?_of_contains hc) = km) → t.get km hc = km :=
DTreeMap.getKey_minKey?
theorem get!_min? [TransCmp cmp] [Inhabited α] {km} :
(hkm : t.min? = some km) → t.get! km = km :=
DTreeMap.getKey!_minKey?
theorem getD_min? [TransCmp cmp] {km fallback} :
(hkm : t.min? = some km) → t.getD km fallback = km :=
DTreeMap.getKeyD_minKey?
@[simp]
theorem min?_bind_get? [TransCmp cmp] :
t.min?.bind t.get? = t.min? :=
@ -872,6 +888,10 @@ theorem min_le_min_erase [TransCmp cmp] {k he} :
(t.erase k |>.min he) |>.isLE :=
DTreeMap.minKey_le_minKey_erase
theorem min?_eq_head?_toList [TransCmp cmp] :
t.min? = t.toList.head? :=
TreeMap.minKey?_eq_head?_keys
theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) :
t.min? = some t.min! :=
DTreeMap.minKey?_eq_some_minKey! he
@ -954,6 +974,10 @@ 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_head!_toList [TransCmp cmp] [Inhabited α] :
t.min! = t.toList.head! :=
TreeMap.minKey!_eq_head!_keys
theorem min?_eq_some_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} :
t.min? = some (t.minD fallback) :=
TreeMap.minKey?_eq_some_minKeyD he
@ -1036,6 +1060,14 @@ theorem minD_le_minD_erase [TransCmp cmp] {k}
cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
TreeMap.minKeyD_le_minKeyD_erase he
theorem min_eq_head_toList [TransCmp cmp] {he} :
t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) :=
DTreeMap.minKey_eq_head_keys
theorem minD_eq_headD_toList [TransCmp cmp] {fallback} :
t.minD fallback = t.toList.headD fallback :=
TreeMap.minKeyD_eq_headD_keys
end Min
end Std.TreeSet

28
src/Std/Data/TreeSet/Raw/Lemmas.lean
View file

@ -428,6 +428,10 @@ theorem distinct_toList [TransCmp cmp] (h : t.WF) :
t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) :=
DTreeMap.Raw.distinct_keys h
theorem ordered_toList [TransCmp cmp] (h : t.WF) :
t.toList.Pairwise (fun a b => cmp a b = .lt) :=
DTreeMap.Raw.ordered_keys h
section monadic
variable {δ : Type w} {m : Type w → Type w}
@ -755,6 +759,18 @@ theorem get?_min? [TransCmp cmp] (h : t.WF) {km} :
(hkm : t.min? = some km) → t.get? km = some km :=
TreeMap.Raw.getKey?_minKey? h
theorem get_min? [TransCmp cmp] (h : t.WF) {km hc} :
(hkm : t.min?.get (isSome_min?_of_contains h hc) = km) → t.get km hc = km :=
TreeMap.Raw.getKey_minKey? h
theorem get!_min? [TransCmp cmp] [Inhabited α] (h : t.WF) {km} :
(hkm : t.min? = some km) → t.get! km = km :=
TreeMap.Raw.getKey!_minKey? h
theorem getD_min? [TransCmp cmp] (h : t.WF) {km fallback} :
(hkm : t.min? = some km) → t.getD km fallback = km :=
TreeMap.Raw.getKeyD_minKey? h
@[simp]
theorem min?_bind_get? [TransCmp cmp] (h : t.WF) :
t.min?.bind t.get? = t.min? :=
@ -782,6 +798,10 @@ theorem min?_le_min?_erase [TransCmp cmp] (h : t.WF) {k km kme} :
cmp km kme |>.isLE :=
TreeMap.Raw.minKey?_le_minKey?_erase h
theorem min?_eq_head?_toList [TransCmp cmp] (h : t.WF) :
t.min? = t.toList.head? :=
TreeMap.Raw.minKey?_eq_head?_keys h
theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) :
t.min? = some t.min! :=
DTreeMap.Raw.minKey?_eq_some_minKey! h he
@ -860,6 +880,10 @@ 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_head!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) :
t.min! = t.toList.head! :=
TreeMap.Raw.minKey!_eq_head!_keys h
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
@ -942,6 +966,10 @@ theorem minD_le_minD_erase [TransCmp cmp] (h : t.WF) {k}
cmp (t.minD fallback) (t.erase k |>.minD fallback) |>.isLE :=
DTreeMap.Raw.minKeyD_le_minKeyD_erase h he
theorem minD_eq_headD_toList [TransCmp cmp] (h : t.WF) {fallback} :
t.minD fallback = t.toList.headD fallback :=
TreeMap.Raw.minKeyD_eq_headD_keys h
end Min
end Std.TreeSet.Raw