From 909ee719aac55a4ab01538e282d73c31f6fea45e Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Fri, 28 Feb 2025 11:14:13 +0100 Subject: [PATCH] feat: tree map lemmas for `keys` and `toList` (#7260) This PR provides lemmas about the tree map functions `keys` and `toList` and their interactions with other functions for which lemmas already exist. Moreover, a bug in `foldr` (calling `foldlM` instead of `foldrM`) is fixed. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> --- src/Std/Classes/Ord.lean | 58 +++++++++ src/Std/Data/DHashMap/Internal/RawLemmas.lean | 6 +- src/Std/Data/DHashMap/Lemmas.lean | 14 ++- src/Std/Data/DHashMap/RawLemmas.lean | 14 ++- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 108 +++++++++++++++- src/Std/Data/DTreeMap/Internal/Queries.lean | 4 +- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 57 +++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 114 +++++++++++++++++ src/Std/Data/DTreeMap/Raw/Lemmas.lean | 115 ++++++++++++++++++ src/Std/Data/HashMap/Lemmas.lean | 9 +- src/Std/Data/HashMap/RawLemmas.lean | 7 +- src/Std/Data/Internal/List/Associative.lean | 2 +- src/Std/Data/TreeMap/Lemmas.lean | 72 +++++++++++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 73 +++++++++++ src/Std/Data/TreeSet/Lemmas.lean | 24 ++++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 24 ++++ 16 files changed, 687 insertions(+), 14 deletions(-) diff --git a/src/Std/Classes/Ord.lean b/src/Std/Classes/Ord.lean index 7af038e0fc..aaa628605b 100644 --- a/src/Std/Classes/Ord.lean +++ b/src/Std/Classes/Ord.lean @@ -253,6 +253,9 @@ section LawfulEq /-- A typeclass for comparison functions satisfying `cmp a b = .eq` if and only if the logical equality `a = b` holds. + +This typeclass distinguishes itself from `LawfulBEqCmp` by using logical equality (`=`) instead of +boolean equality (`==`). -/ class LawfulEqCmp {α : Type u} (cmp : α → α → Ordering) : Prop extends ReflCmp cmp where /-- If two values compare equal, then they are logically equal. -/ @@ -261,6 +264,9 @@ class LawfulEqCmp {α : Type u} (cmp : α → α → Ordering) : Prop extends Re /-- A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if the logical equality `a = b` holds. + +This typeclass distinguishes itself from `LawfulBEqOrd` by using logical equality (`=`) instead of +boolean equality (`==`). -/ abbrev LawfulEqOrd (α : Type u) [Ord α] := LawfulEqCmp (compare : α → α → Ordering) @@ -276,6 +282,48 @@ theorem compare_beq_iff_eq {a b : α} : cmp a b == .eq ↔ a = b := end LawfulEq +section LawfulBEq + +/-- +A typeclass for comparison functions satisfying `cmp a b = .eq` if and only if the boolean equality +`a == b` holds. + +This typeclass distinguishes itself from `LawfulEqCmp` by using boolean equality (`==`) instead of +logical equality (`=`). +-/ +class LawfulBEqCmp {α : Type u} [BEq α] (cmp : α → α → Ordering) : Prop where + /-- If two values compare equal, then they are logically equal. -/ + compare_eq_iff_beq {a b : α} : cmp a b = .eq ↔ a == b + +/-- +A typeclass for types with a comparison function that satisfies `compare a b = .eq` if and only if +the boolean equality `a == b` holds. + +This typeclass distinguishes itself from `LawfulEqOrd` by using boolean equality (`==`) instead of +logical equality (`=`). +-/ +abbrev LawfulBEqOrd (α : Type u) [BEq α] [Ord α] := LawfulBEqCmp (compare : α → α → Ordering) + +variable {α : Type u} [BEq α] {cmp : α → α → Ordering} + +instance [LawfulEqCmp cmp] [LawfulBEq α] : + LawfulBEqCmp cmp where + compare_eq_iff_beq := compare_eq_iff_eq.trans beq_iff_eq.symm + +theorem LawfulBEqCmp.equivBEq [inst : LawfulBEqCmp cmp] [TransCmp cmp] : EquivBEq α where + refl := inst.compare_eq_iff_beq.mp ReflCmp.compare_self + symm := by + simp only [← inst.compare_eq_iff_beq] + exact OrientedCmp.eq_symm + trans := by + simp only [← inst.compare_eq_iff_beq] + exact TransCmp.eq_trans + +instance LawfulBEqOrd.equivBEq [Ord α] [LawfulBEqOrd α] [TransOrd α] : EquivBEq α := + LawfulBEqCmp.equivBEq (cmp := compare) + +end LawfulBEq + namespace Internal variable {α : Type u} @@ -292,6 +340,16 @@ def beqOfOrd [Ord α] : BEq α where theorem beq_eq [Ord α] {a b : α} : (a == b) = (compare a b == .eq) := rfl +theorem beq_iff [Ord α] {a b : α} : (a == b) = true ↔ compare a b = .eq := by + rw [beq_eq, beq_iff_eq] + +theorem eq_beqOfOrd_of_lawfulBEqOrd [Ord α] (inst : BEq α) [instLawful : LawfulBEqOrd α] : + inst = beqOfOrd := by + cases inst; rename_i instBEq + congr; ext a b + rw [Bool.eq_iff_iff, beq_iff_eq, instLawful.compare_eq_iff_beq] + rfl + theorem equivBEq_of_transOrd [Ord α] [TransOrd α] : EquivBEq α where symm {a b} h := by simp_all [OrientedCmp.eq_comm] trans h₁ h₂ := by simp_all only [beq_eq, beq_iff_eq]; exact TransCmp.eq_trans h₁ h₂ diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 393c6f6d4a..5d68f7b763 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -858,7 +858,7 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : m.1.keys.Pairwise (fun a b => (a == b) = false) := by simp_to_model using (Raw.WF.out h).distinct.distinct -theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : m.1.toList.map Sigma.fst = m.1.keys := by simp_to_model rw [List.keys_eq_map] @@ -894,9 +894,9 @@ namespace Const variable {β : Type v} (m : Raw₀ α (fun _ => β)) -theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : (Raw.Const.toList m.1).map Prod.fst = m.1.keys := by - simp_to_model using List.map_prod_fst_map_toProd_eq_keys + simp_to_model using List.map_fst_map_toProd_eq_keys theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : (Raw.Const.toList m.1).length = m.1.size := by diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 3d31b7a2b1..fe0653c87d 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -964,9 +964,14 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] : Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2 @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : + m.1.toList.map Sigma.fst = m.1.keys := + Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : m.1.toList.map Sigma.fst = m.1.keys := - Raw₀.map_sigma_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ + Raw₀.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] : @@ -1010,9 +1015,14 @@ namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : + (toList m).map Prod.fst = m.keys := + Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : (toList m).map Prod.fst = m.keys := - Raw₀.Const.map_prod_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ + Raw₀.Const.map_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩ @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] : diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index eabf420c15..db20deea46 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -1053,9 +1053,14 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.toList.map Sigma.fst = m.keys := by + apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.toList.map Sigma.fst = m.keys := by - apply Raw₀.map_sigma_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ + apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) : @@ -1099,9 +1104,14 @@ namespace Const variable {β : Type v} {m : Raw α (fun _ => β)} @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : + (Raw.Const.toList m).map Prod.fst = m.keys := by + apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : (Raw.Const.toList m).map Prod.fst = m.keys := by - apply Raw₀.Const.map_prod_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ + apply Raw₀.Const.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩ @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) : diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 1eb6909601..820117aebe 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -59,7 +59,8 @@ private def queryNames : Array Name := ``get!_eq_getValueCast!, ``Const.get!_eq_getValue!, ``getD_eq_getValueCastD, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?, ``getKey_eq_getKey, - ``getKey!_eq_getKey!, ``getKeyD_eq_getKeyD] + ``getKey!_eq_getKey!, ``getKeyD_eq_getKeyD, + ``keys_eq_keys, ``toList_eq_toListModel, ``Const.toList_eq_toListModel_map] private def modifyMap : Std.HashMap Name Name := .ofList @@ -1465,4 +1466,109 @@ theorem getThenInsertIfNew?!_snd [TransOrd α] (h : t.WF) {k : α} {v : β} : end Const +theorem length_keys [TransOrd α] (h : t.WF) : + t.keys.length = t.size := by + simp_to_model using List.length_keys_eq_length + +theorem isEmpty_keys : + t.keys.isEmpty = t.isEmpty := by + simp_to_model using List.isEmpty_keys_eq_isEmpty + +theorem contains_keys [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) : + t.keys.contains k = t.contains k := by + rw [contains_eq_containsKey h.ordered, ← eq_beqOfOrd_of_lawfulBEqOrd] + simp_to_model using (List.containsKey_eq_keys_contains (a := k) (l := t.toListModel)).symm + +theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) : + k ∈ t.keys ↔ k ∈ t := by + simpa only [mem_iff_contains, ← List.contains_iff, ← Bool.eq_iff_iff] using contains_keys h + +theorem distinct_keys [TransOrd α] (h : t.WF) : + t.keys.Pairwise (fun a b => ¬ compare a b = .eq) := by + simp only [← not_congr beq_iff_eq, ← beq_eq, Bool.not_eq_true] + simp_to_model using h.ordered.distinctKeys.distinct + +theorem map_fst_toList_eq_keys : + t.toList.map Sigma.fst = t.keys := by + simp_to_model using (List.keys_eq_map ..).symm + +theorem length_toList [TransOrd α] (h : t.WF) : + t.toList.length = t.size := by + simp_to_model + +theorem isEmpty_toList : + t.toList.isEmpty = t.isEmpty := by + simp_to_model + +theorem mem_toList_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) : + ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v := by + simp_to_model using List.mem_iff_getValueCast?_eq_some + +theorem find?_toList_eq_some_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} + (h : t.WF) : + t.toList.find? (compare ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := by + simp_to_model using List.find?_eq_some_iff_getValueCast?_eq_some + +theorem find?_toList_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) : + t.toList.find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by + simp_to_model using List.find?_eq_none_iff_containsKey_eq_false + +theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : + t.toList.find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h + +theorem distinct_keys_toList [TransOrd α] (h : t.WF) : + t.toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by + simp only [← beq_iff, Bool.not_eq_true] + simp_to_model using List.pairwise_fst_eq_false + +namespace Const + +variable {β : Type v} {t : Impl α β} + +theorem map_fst_toList_eq_keys : + (toList t).map Prod.fst = t.keys := by + simp_to_model using List.map_fst_map_toProd_eq_keys + +theorem length_toList (h : t.WF) : + (toList t).length = t.size := by + simp_to_model using List.length_map + +theorem isEmpty_toList : + (toList t).isEmpty = t.isEmpty := by + rw [Bool.eq_iff_iff, List.isEmpty_iff, isEmpty_eq_isEmpty, List.isEmpty_iff] + simp_to_model using List.map_eq_nil_iff + +theorem mem_toList_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} (h : t.WF) : + (k, v) ∈ toList t ↔ get? t k = some v := by + simp_to_model using List.mem_map_toProd_iff_getValue?_eq_some + +theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k : α} {v : β} (h : t.WF) : + (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v := by + simp_to_model using List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some + +theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransOrd α] {k : α} {v : β} (h : t.WF) : + get? t k = some v ↔ ∃ (k' : α), compare k k' = .eq ∧ (k', v) ∈ toList t := by + simp_to_model using List.getValue?_eq_some_iff_exists_beq_and_mem_toList + +theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k k' : α} {v : β} + (h : t.WF) : (toList t).find? (fun a => compare a.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ get? t k = some v := by + simp_to_model using List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some + +theorem find?_toList_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) : + (toList t).find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by + simp_to_model using List.find?_map_eq_none_iff_containsKey_eq_false + +theorem find?_toList_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : + (toList t).find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h + +theorem distinct_keys_toList [TransOrd α] (h : t.WF) : + (toList t).Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by + simp only [← beq_iff, Bool.not_eq_true] + simp_to_model using List.pairwise_fst_eq_false_map_toProd + +end Const + end Std.DTreeMap.Internal.Impl diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean index 8099cb71a3..2529028653 100644 --- a/src/Std/Data/DTreeMap/Internal/Queries.lean +++ b/src/Std/Data/DTreeMap/Internal/Queries.lean @@ -201,9 +201,9 @@ def foldl (f : δ → (a : α) → β a → δ) (init : δ) (t : Impl α β) : def foldrM {m} [Monad m] (f : δ → (a : α) → β a → m δ) (init : δ) : Impl α β → m δ | .leaf => pure init | .inner _ k v l r => do - let right ← foldlM f init r + let right ← foldrM f init r let middle ← f right k v - foldlM f middle l + foldrM f middle l /-- Folds the given function over the mappings in the tree in descending order. -/ @[inline] diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index e9f074ce92..2ae3cc8d38 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1105,6 +1105,7 @@ theorem ordered_mergeWith [Ord α] [TransOrd α] [LawfulEqOrd α] {t₁ t₂ : I induction t₂ generalizing t₁ with | leaf => exact hto | inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto)) + /-! ### foldlM -/ @@ -1125,6 +1126,51 @@ theorem foldl_eq_foldl {t : Impl α β} {δ} {f : δ → (a : α) → β a → t.foldl (init := init) f = t.toListModel.foldl (init := init) fun acc p => f acc p.1 p.2 := by rw [foldl, foldlM_eq_foldlM, List.foldl_eq_foldlM, Id.run] +/-! +### foldrM +-/ + +theorem foldrM_eq_foldrM {t : Impl α β} {m δ} [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init} : + t.foldrM (init := init) f = t.toListModel.foldrM (init := init) fun p acc => f acc p.1 p.2 := by + induction t generalizing init with + | leaf => rfl + | inner sz k v l r ihl ihr => + simp only [foldrM, toListModel_inner, List.foldr_append, List.foldr_cons] + simp [ihl, ihr] + +/-! +### foldr +-/ + +theorem foldr_eq_foldr {t : Impl α β} {δ} {f : δ → (a : α) → β a → δ} {init} : + t.foldr (init := init) f = t.toListModel.foldr (init := init) fun p acc => f acc p.1 p.2 := by + rw [foldr, foldrM_eq_foldrM, List.foldr_eq_foldrM, Id.run] + +/-! +### toList +-/ + +theorem toList_eq_toListModel {t : Impl α β} : + t.toList = t.toListModel := by + rw [toList, foldr_eq_foldr] + induction t with + | leaf => rfl + | inner sz k v l r ihl ihr => simp + +/-! +### keys +-/ + +theorem keys_eq_keys {t : Impl α β} : + t.keys = t.toListModel.keys := by + rw [keys, foldr_eq_foldr, List.keys.eq_def] + simp + induction t.toListModel with + | nil => rfl + | cons e es ih => + simp [ih] + rw [List.keys.eq_def] + namespace Const variable {β : Type v} @@ -1243,6 +1289,17 @@ theorem ordered_mergeWith [Ord α] [TransOrd α] {t₁ t₂ : Impl α β} {f} | leaf => exact hto | inner sz k v l r ihl ihr => exact ihr _ (ordered_alter _ (ihl htb hto)) +/-! +### toList +-/ + +theorem toList_eq_toListModel_map {t : Impl α β} : + Const.toList t = t.toListModel.map fun ⟨k, v⟩ => (k, v) := by + rw [toList, foldr_eq_foldr] + induction t with + | leaf => rfl + | inner sz k v l r ihl ihr => simp + end Const /-! diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 172b98fc5a..1848ea6713 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -922,4 +922,118 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] {k : α} {v : β} : end Const +@[simp] +theorem length_keys [TransCmp cmp] : + t.keys.length = t.size := + Impl.length_keys t.wf + +@[simp] +theorem isEmpty_keys : + t.keys.isEmpty = t.isEmpty := + Impl.isEmpty_keys + +@[simp] +theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.keys.contains k = t.contains k := + Impl.contains_keys t.wf + +@[simp] +theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.keys ↔ k ∈ t := + Impl.mem_keys t.wf + +theorem distinct_keys [TransCmp cmp] : + t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := + Impl.distinct_keys t.wf + +@[simp] +theorem map_fst_toList_eq_keys : + t.toList.map Sigma.fst = t.keys := + Impl.map_fst_toList_eq_keys + +@[simp] +theorem length_toList [TransCmp cmp] : + t.toList.length = t.size := + Impl.length_toList t.wf + +@[simp] +theorem isEmpty_toList : + t.toList.isEmpty = t.isEmpty := + Impl.isEmpty_toList + +@[simp] +theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v := + Impl.mem_toList_iff_get?_eq_some t.wf + +theorem find?_toList_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + t.toList.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := + Impl.find?_toList_eq_some_iff_get?_eq_some t.wf + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + t.toList.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.find?_toList_eq_none_iff_contains_eq_false t.wf + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + t.toList.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false + +theorem distinct_keys_toList [TransCmp cmp] : + t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) := + Impl.distinct_keys_toList t.wf + +namespace Const + +variable {β : Type v} {t : DTreeMap α β cmp} + +@[simp] +theorem map_fst_toList_eq_keys : + (toList t).map Prod.fst = t.keys := + Impl.Const.map_fst_toList_eq_keys + +@[simp] +theorem length_toList : + (toList t).length = t.size := + Impl.Const.length_toList t.wf + +@[simp] +theorem isEmpty_toList : + (toList t).isEmpty = t.isEmpty := + Impl.Const.isEmpty_toList + +@[simp] +theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} : + (k, v) ∈ toList t ↔ get? t k = some v := + Impl.Const.mem_toList_iff_get?_eq_some t.wf + +@[simp] +theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k : α} {v : β} : + (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v := + Impl.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some t.wf + +theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] {k : α} {v : β} : + get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t := + Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList t.wf + +theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k k' : α} {v : β} : + (toList t).find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ get? t k = some v := + Impl.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some t.wf + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.Const.find?_toList_eq_none_iff_contains_eq_false t.wf + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.Const.find?_toList_eq_none_iff_not_mem t.wf + +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 + +end Const + end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 0b9d995641..471ed49b24 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -930,4 +930,119 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β} : end Const +@[simp] +theorem length_keys [TransCmp cmp] (h : t.WF) : + t.keys.length = t.size := + Impl.length_keys h.out + +@[simp] +theorem isEmpty_keys : + t.keys.isEmpty = t.isEmpty := + Impl.isEmpty_keys + +@[simp] +theorem contains_keys [BEq α] [LawfulBEqCmp cmp] (h : t.WF) [TransCmp cmp] {k : α} : + t.keys.contains k = t.contains k := + Impl.contains_keys h + +@[simp] +theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.keys ↔ k ∈ t := + Impl.mem_keys h + +theorem distinct_keys [TransCmp cmp] (h : t.WF) : + t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := + Impl.distinct_keys h.out + +@[simp] +theorem map_fst_toList_eq_keys : + t.toList.map Sigma.fst = t.keys := + Impl.map_fst_toList_eq_keys + +@[simp] +theorem length_toList [TransCmp cmp] (h : t.WF) : + t.toList.length = t.size := + Impl.length_toList h.out + +@[simp] +theorem isEmpty_toList : + t.toList.isEmpty = t.isEmpty := + Impl.isEmpty_toList + +@[simp] +theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + ⟨k, v⟩ ∈ t.toList ↔ t.get? k = some v := + Impl.mem_toList_iff_get?_eq_some h.out + +theorem find?_toList_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} + {v : β k} : t.toList.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := + Impl.find?_toList_eq_some_iff_get?_eq_some h.out + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + t.toList.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.find?_toList_eq_none_iff_contains_eq_false h.out + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + t.toList.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toList_eq_none_iff_contains_eq_false h + +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 + +namespace Const + +variable {β : Type v} {t : Raw α β cmp} + +@[simp] +theorem map_fst_toList_eq_keys : + (toList t).map Prod.fst = t.keys := + Impl.Const.map_fst_toList_eq_keys + +@[simp] +theorem length_toList (h : t.WF) : + (toList t).length = t.size := + Impl.Const.length_toList h.out + +@[simp] +theorem isEmpty_toList : + (toList t).isEmpty = t.isEmpty := + Impl.Const.isEmpty_toList + +@[simp] +theorem mem_toList_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toList t ↔ get? t k = some v := + Impl.Const.mem_toList_iff_get?_eq_some h + +@[simp] +theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ get? t k = some v := + Impl.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some h + +theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t := + Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList h + +theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) + {k k' : α} {v : β} : + (toList t).find? (fun a => cmp a.1 k = .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ get? t k = some v := + Impl.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.Const.find?_toList_eq_none_iff_contains_eq_false h.out + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.Const.find?_toList_eq_none_iff_not_mem h.out + +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 + +end Const + end Std.DTreeMap.Raw diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 894c28e044..74c057c54a 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -699,9 +699,14 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] : DHashMap.distinct_keys @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : + m.toList.map Prod.fst = m.keys := + DHashMap.Const.map_fst_toList_eq_keys + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] : m.toList.map Prod.fst = m.keys := - DHashMap.Const.map_prod_fst_toList_eq_keys + DHashMap.Const.map_fst_toList_eq_keys @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] : @@ -733,7 +738,7 @@ theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} : m.toList.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔ - m.getKey? k = some k' ∧ get? m k = some v := + m.getKey? k = some k' ∧ m[k]? = some v := DHashMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α] diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 6f3b07c9ed..e0d06f9942 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -706,9 +706,14 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : DHashMap.Raw.distinct_keys h.out @[simp] +theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : + m.toList.map Prod.fst = m.keys := + DHashMap.Raw.Const.map_fst_toList_eq_keys h.out + +@[simp, deprecated map_fst_toList_eq_keys (since := "2025-02-28")] theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) : m.toList.map Prod.fst = m.keys := - DHashMap.Raw.Const.map_prod_fst_toList_eq_keys h.out + DHashMap.Raw.Const.map_fst_toList_eq_keys h.out @[simp] theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) : diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 18231341f4..c8fae5881b 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -1997,7 +1997,7 @@ theorem pairwise_fst_eq_false [BEq α] {l : List ((a : α) × β a)} (h : Distin rw [DistinctKeys.def] at h assumption -theorem map_prod_fst_map_toProd_eq_keys {β : Type v} {l : List ((_ : α) × β)} : +theorem map_fst_map_toProd_eq_keys {β : Type v} {l : List ((_ : α) × β)} : List.map Prod.fst (List.map (fun x => (x.fst, x.snd)) l) = List.keys l := by induction l with | nil => simp diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index ea405a7d85..616909d056 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -655,4 +655,76 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] {k : α} {v : β} : (getThenInsertIfNew? t k v).2 = t.insertIfNew k v := ext <| DTreeMap.Const.getThenInsertIfNew?_snd +@[simp] +theorem length_keys [TransCmp cmp] : + t.keys.length = t.size := + DTreeMap.length_keys + +@[simp] +theorem isEmpty_keys : + t.keys.isEmpty = t.isEmpty := + DTreeMap.isEmpty_keys + +@[simp] +theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.keys.contains k = t.contains k := + DTreeMap.contains_keys + +@[simp] +theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.keys ↔ k ∈ t := + DTreeMap.mem_keys + +theorem distinct_keys [TransCmp cmp] : + t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := + DTreeMap.distinct_keys + +@[simp] +theorem map_fst_toList_eq_keys : + (toList t).map Prod.fst = t.keys := + DTreeMap.Const.map_fst_toList_eq_keys + +@[simp] +theorem length_toList : + (toList t).length = t.size := + DTreeMap.Const.length_toList + +@[simp] +theorem isEmpty_toList : + (toList t).isEmpty = t.isEmpty := + DTreeMap.Const.isEmpty_toList + +@[simp] +theorem mem_toList_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} : + (k, v) ∈ toList t ↔ t[k]? = some v := + DTreeMap.Const.mem_toList_iff_get?_eq_some + +@[simp] +theorem mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k : α} {v : β} : + (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ t[k]? = some v := + DTreeMap.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some + +theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] {k : α} {v : β} : + t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t := + DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList + +theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k k' : α} + {v : β} : + t.toList.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ t[k]? = some v := + DTreeMap.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + DTreeMap.Const.find?_toList_eq_none_iff_contains_eq_false + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + DTreeMap.Const.find?_toList_eq_none_iff_not_mem + +theorem distinct_keys_toList [TransCmp cmp] : + (toList t).Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) := + DTreeMap.Const.distinct_keys_toList + end Std.TreeMap diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 6f3922d603..4e245daae1 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -662,4 +662,77 @@ theorem getThenInsertIfNew?_snd [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (getThenInsertIfNew? t k v).2 = t.insertIfNew k v := ext <| DTreeMap.Raw.Const.getThenInsertIfNew?_snd h +@[simp] +theorem length_keys [TransCmp cmp] (h : t.WF) : + t.keys.length = t.size := + DTreeMap.Raw.length_keys h + +@[simp] +theorem isEmpty_keys : + t.keys.isEmpty = t.isEmpty := + DTreeMap.Raw.isEmpty_keys + +@[simp] +theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + t.keys.contains k = t.contains k := + DTreeMap.Raw.contains_keys h + +@[simp] +theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.keys ↔ k ∈ t := + DTreeMap.Raw.mem_keys h + +theorem distinct_keys [TransCmp cmp] (h : t.WF) : + t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := + DTreeMap.Raw.distinct_keys h + +@[simp] +theorem map_fst_toList_eq_keys : + (toList t).map Prod.fst = t.keys := + DTreeMap.Raw.Const.map_fst_toList_eq_keys + +@[simp] +theorem length_toList (h : t.WF) : + (toList t).length = t.size := + DTreeMap.Raw.Const.length_toList h + +@[simp] +theorem isEmpty_toList : + (toList t).isEmpty = t.isEmpty := + DTreeMap.Raw.Const.isEmpty_toList + +@[simp] +theorem mem_toList_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toList t ↔ t[k]? = some v := + DTreeMap.Raw.Const.mem_toList_iff_get?_eq_some h + +@[simp] +theorem mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toList t ↔ t.getKey? k = some k ∧ t[k]? = some v := + DTreeMap.Raw.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some h + +theorem getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toList [TransCmp cmp] (h : t.WF) {k : α} + {v : β} : + t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toList t := + DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toList h + +theorem find?_toList_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) + {k k' : α} {v : β} : + t.toList.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ t[k]? = some v := + DTreeMap.Raw.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h + +theorem find?_toList_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + DTreeMap.Raw.Const.find?_toList_eq_none_iff_contains_eq_false h + +@[simp] +theorem find?_toList_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + (toList t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + DTreeMap.Raw.Const.find?_toList_eq_none_iff_not_mem h + +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 + end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 5c4927b7c4..7a29e12163 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -334,4 +334,28 @@ theorem containsThenInsert_snd [TransCmp cmp] {k : α} : (t.containsThenInsert k).2 = t.insert k := ext <| TreeMap.containsThenInsertIfNew_snd +@[simp] +theorem length_toList [TransCmp cmp] : + t.toList.length = t.size := + DTreeMap.length_keys + +@[simp] +theorem isEmpty_toList : + t.toList.isEmpty = t.isEmpty := + DTreeMap.isEmpty_keys + +@[simp] +theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.toList.contains k = t.contains k := + DTreeMap.contains_keys + +@[simp] +theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.toList ↔ k ∈ t := + DTreeMap.mem_keys + +theorem distinct_toList [TransCmp cmp] : + t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) := + DTreeMap.distinct_keys + end Std.TreeSet diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 20bc6a1d42..7aaf9418e9 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -335,4 +335,28 @@ theorem containsThenInsert_snd [TransCmp cmp] (h : t.WF) {k : α} : (t.containsThenInsert k).2 = t.insert k := ext <| TreeMap.Raw.containsThenInsertIfNew_snd h +@[simp] +theorem length_toList [TransCmp cmp] (h : t.WF) : + t.toList.length = t.size := + DTreeMap.Raw.length_keys h + +@[simp] +theorem isEmpty_toList : + t.toList.isEmpty = t.isEmpty := + DTreeMap.Raw.isEmpty_keys + +@[simp] +theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + t.toList.contains k = t.contains k := + DTreeMap.Raw.contains_keys h + +@[simp] +theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.toList ↔ k ∈ t := + DTreeMap.Raw.mem_keys h + +theorem distinct_toList [TransCmp cmp] (h : t.WF) : + t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) := + DTreeMap.Raw.distinct_keys h + end Std.TreeSet.Raw