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>
This commit is contained in:
Paul Reichert
GitHub
parent
7dd5e957da
commit
909ee719aa
16 changed files with 687 additions and 14 deletions
|
|
@ -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₂
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 α] :
|
||||
|
|
|
|||
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
/-!
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 α]
|
||||
|
|
|
|||
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue