From cdfde63734a0ef08d7f707a1f8a3d6566b24af5b Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Mon, 9 Mar 2026 21:04:59 +0100 Subject: [PATCH] feat: tree map `toArray`/`keysArray` lemmas (#12481) This PR provides lemmas about `toArray` and `keysArray` on tree maps and tree sets that are analogous to the existing `toList` and `keys` lemmas. --- src/Init/Data/Array/Basic.lean | 3 + src/Init/Data/List/Lemmas.lean | 6 + src/Std/Data/DTreeMap/Internal/Lemmas.lean | 402 ++++++++++++++++++ src/Std/Data/DTreeMap/Internal/Model.lean | 2 +- src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 2 +- src/Std/Data/DTreeMap/Lemmas.lean | 315 ++++++++++++++ src/Std/Data/DTreeMap/Raw/Lemmas.lean | 304 +++++++++++++ src/Std/Data/TreeMap/Lemmas.lean | 215 ++++++++++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 208 +++++++++ src/Std/Data/TreeSet/Lemmas.lean | 107 +++++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 104 +++++ 11 files changed, 1666 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean index 7f7887b7bf..49b0ef2b2e 100644 --- a/src/Init/Data/Array/Basic.lean +++ b/src/Init/Data/Array/Basic.lean @@ -148,6 +148,9 @@ end List namespace Array +@[simp, grind =] theorem getElem!_toList [Inhabited α] {xs : Array α} {i : Nat} : xs.toList[i]! = xs[i]! := by + rw [List.getElem!_toArray] + theorem size_eq_length_toList {xs : Array α} : xs.size = xs.toList.length := rfl /-! ### Externs -/ diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 4f6b07ee94..328689ead8 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -936,6 +936,12 @@ theorem getElem_zero_eq_head {l : List α} (h : 0 < l.length) : | nil => simp at h | cons _ _ => simp +theorem head!_eq_getElem! [Inhabited α] {l : List α} : head! l = l[0]! := by + cases l <;> rfl + +theorem headD_eq_getD {l : List α} {fallback} : headD l fallback = l.getD 0 fallback := by + cases l <;> rfl + theorem head_eq_iff_head?_eq_some {xs : List α} (h) : xs.head h = a ↔ xs.head? = some a := by cases xs with | nil => simp at h diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index 23a943dd17..8a21803e62 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -8,6 +8,7 @@ module prelude public import Std.Data.HashMap.Basic public import Std.Data.DTreeMap.Internal.WF.Lemmas +public import Init.Data.Array.Perm public meta import Std.Data.HashMap.Basic import Init.Data.List.Find import Init.Data.List.Pairwise @@ -104,10 +105,13 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T ⟨`getKeyD, (``getKeyD_eq_getKeyD, #[``(getKeyD_of_perm _)])⟩, ⟨`getKey!, (``getKey!_eq_getKey!, #[``(getKey!_of_perm _)])⟩, ⟨`toList, (``toList_eq_toListModel, #[])⟩, + ⟨`toArray, (``toArray_eq_toArray, #[])⟩, ⟨`beq, (``beq_eq_beqModel, #[])⟩, ⟨`Const.beq, (``Internal.Impl.Const.beq_eq_beqModel, #[])⟩, ⟨`keys, (``keys_eq_keys, #[])⟩, + ⟨`keysArray, (``keysArray_eq_toArray_keys, #[])⟩, ⟨`Const.toList, (``Const.toList_eq_toListModel_map, #[])⟩, + ⟨`Const.toArray, (``Const.toArray_eq_toArray_map, #[])⟩, ⟨`foldlM, (``foldlM_eq_foldlM_toListModel, #[])⟩, ⟨`foldl, (``foldl_eq_foldl, #[])⟩, ⟨`foldrM, (``foldrM_eq_foldrM, #[])⟩, @@ -228,6 +232,18 @@ theorem isEmpty_iff_forall_not_mem [TransOrd α] (h : t.WF) : t.isEmpty = true ↔ ∀ a, ¬a ∈ t := by simpa only [mem_iff_contains, Bool.not_eq_true] using isEmpty_iff_forall_contains h +theorem toArray_toList : t.toList.toArray = t.toArray := by + simp_to_model [toList, toArray] + +theorem toList_toArray : t.toArray.toList = t.toList := by + simp_to_model [toList, toArray] + +theorem toArray_keys : t.keys.toArray = t.keysArray := by + simp_to_model [Const.toList, keys, keysArray] + +theorem toList_keysArray : t.keysArray.toList = t.keys := by + simp_to_model [Const.toList, keys, keysArray] + theorem contains_insert [TransOrd α] (h : t.WF) {k a : α} {v : β k} : (t.insert k v h.balanced).impl.contains a = (compare k a == .eq || t.contains a) := by simp_to_model [insert, contains] using List.containsKey_insertEntry @@ -580,6 +596,12 @@ namespace Const variable {β : Type v} {t : Impl α β} +theorem toArray_toList : (toList t).toArray = toArray t := by + simp_to_model [Const.toList, Const.toArray] + +theorem toList_toArray : (toArray t).toList = toList t := by + simp_to_model [Const.toList, Const.toArray] + theorem get?_empty [TransOrd α] {a : α} : get? (empty : Impl α β) a = none := by simp_to_model [Const.get?] using List.getValue?_nil @@ -676,6 +698,18 @@ theorem toList_insert!_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) (t.insert! k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := by simpa only [insert_eq_insert!] using toList_insert_perm h +theorem toArray_insert_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert k v h.balanced).1.toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := by + simp only [← toArray_toList, List.filter_toArray', List.push_toArray, + ← List.perm_iff_toArray_perm, List.size_toArray] + refine (toList_insert_perm h).trans ?_ + rw [← List.singleton_append] + apply List.perm_append_comm + +theorem toArray_insert!_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insert! k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := by + simpa only [insert_eq_insert!] using toArray_insert_perm h + theorem Const.toList_insert_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} : (Const.toList (t.insert k v h.balanced).1).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by simp_to_model @@ -687,6 +721,18 @@ theorem Const.toList_insert!_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq (Const.toList (t.insert! k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := by simpa only [insert_eq_insert!] using Const.toList_insert_perm h +theorem Const.toArray_insert_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} : + (Const.toArray (t.insert k v h.balanced).1).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := by + simp only [← toArray_toList, List.size_toArray, List.filter_toArray', List.push_toArray, + ← List.perm_iff_toArray_perm] + refine (toList_insert_perm h).trans ?_ + rw [← List.singleton_append] + apply List.perm_append_comm + +theorem Const.toArray_insert!_perm {β : Type v} {t : Impl α (fun _ => β)} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β} : + (Const.toArray (t.insert! k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := by + simpa only [insert_eq_insert!] using Const.toArray_insert_perm h + theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : (t.insertIfNew k v h.balanced).1.keys.Perm (if t.contains k then t.keys else k :: t.keys) := by simp_to_model @@ -698,10 +744,22 @@ theorem keys_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF apply List.keys_insertEntryIfNew_perm simp +theorem keysArray_insertIfNew_perm [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v h.balanced).1.keysArray.Perm (if t.contains k then t.keysArray else t.keysArray.push k) := by + rw [← toArray_keys, ← toArray_keys, Array.perm_iff_toList_perm, List.toList_toArray] + refine (keys_insertIfNew_perm h).trans ?_ + split + · simp + · simpa using (List.perm_append_singleton ..).symm + theorem keys_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : (t.insertIfNew! k v).keys.Perm (if t.contains k then t.keys else k :: t.keys) := by simpa only [insertIfNew_eq_insertIfNew!] using keys_insertIfNew_perm h +theorem keysArray_insertIfNew!_perm {t : Impl α β} [BEq α] [TransOrd α] [LawfulBEqOrd α] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew! k v).keysArray.Perm (if t.contains k then t.keysArray else t.keysArray.push k) := by + simpa only [insertIfNew_eq_insertIfNew!] using keysArray_insertIfNew_perm h + theorem get_insert_self [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k : α} {v : β k} : (t.insert k v h.balanced).impl.get k (contains_insert_self h) = v := by simp_to_model [insert, get] using List.getValueCast_insertEntry_self @@ -1638,22 +1696,43 @@ theorem length_keys [TransOrd α] (h : t.WF) : t.keys.length = t.size := by simp_to_model [size, keys] using List.length_keys_eq_length +theorem size_keysArray [TransOrd α] (h : t.WF) : + t.keysArray.size = t.size := by + rw [← toArray_keys, List.size_toArray, length_keys h] + theorem isEmpty_keys : t.keys.isEmpty = t.isEmpty := by simp_to_model [isEmpty, keys] using List.isEmpty_keys_eq_isEmpty +theorem isEmpty_keysArray : + t.keysArray.isEmpty = t.isEmpty := by + rw [← toArray_keys, List.isEmpty_toArray, isEmpty_keys] + theorem contains_keys [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) : t.keys.contains k = t.contains k := by simp_to_model [contains, keys] using (List.containsKey_eq_keys_contains).symm +theorem contains_keysArray [BEq α] [beqOrd : LawfulBEqOrd α] [TransOrd α] {k : α} (h : t.WF) : + t.keysArray.contains k = t.contains k := by + rw [← toArray_keys, List.contains_toArray, contains_keys h] + theorem mem_keys [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) : k ∈ t.keys ↔ k ∈ t := by simpa only [mem_iff_contains, ← List.contains_iff_mem, ← Bool.eq_iff_iff] using contains_keys h +theorem mem_keysArray [LawfulEqOrd α] [TransOrd α] {k : α} (h : t.WF) : + k ∈ t.keysArray ↔ k ∈ t := by + rw [← toArray_keys, List.mem_toArray, mem_keys h] + theorem mem_of_mem_keys [TransOrd α] (h : t.WF) {k : α} (h' : k ∈ t.keys) : k ∈ t := (contains_keys h).symm.trans (List.elem_eq_true_of_mem h') +theorem mem_of_mem_keysArray [TransOrd α] (h : t.WF) {k : α} + (h' : k ∈ t.keysArray) : k ∈ t := by + rw [← toArray_keys, List.mem_toArray] at h' + exact mem_of_mem_keys h h' + 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 @@ -1667,31 +1746,60 @@ 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 +theorem map_fst_toArray_eq_keysArray : + t.toArray.map Sigma.fst = t.keysArray := by + rw [← toArray_toList, List.map_toArray, map_fst_toList_eq_keys, toArray_keys] + theorem length_toList [TransOrd α] (h : t.WF) : t.toList.length = t.size := by simp_to_model [toList, size] +theorem size_toArray [TransOrd α] (h : t.WF) : + t.toArray.size = t.size := by + rw [← toArray_toList, List.size_toArray, length_toList h] + theorem isEmpty_toList : t.toList.isEmpty = t.isEmpty := by simp_to_model [toList, isEmpty] +theorem isEmpty_toArray : + t.toArray.isEmpty = t.isEmpty := by + rw [← toArray_toList, List.isEmpty_toArray, isEmpty_toList] + 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 [toList, get?] using List.mem_iff_getValueCast?_eq_some +theorem mem_toArray_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} (h : t.WF) : + ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v := by + rw [← toArray_toList, List.mem_toArray, mem_toList_iff_get?_eq_some h] + 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 [toList, get?] using List.find?_eq_some_iff_getValueCast?_eq_some +theorem find?_toArray_eq_some_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β k} + (h : t.WF) : + t.toArray.find? (compare ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := by + rw [← toArray_toList, List.find?_toArray, find?_toList_eq_some_iff_get?_eq_some h] + 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 [toList, contains] using List.find?_eq_none_iff_containsKey_eq_false +theorem find?_toArray_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) : + t.toArray.find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by + rw [← toArray_toList, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false h] + 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 find?_toArray_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : + t.toArray.find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toArray_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_to_model [toList] using List.pairwise_fst_eq_false @@ -1708,52 +1816,97 @@ theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := by simp_to_model [Const.toList, keys] using List.map_fst_map_toProd_eq_keys +theorem map_fst_toArray_eq_keysArray : + (toArray t).map Prod.fst = t.keysArray := by + rw [← toArray_toList, List.map_toArray, map_fst_toList_eq_keys, toArray_keys] + theorem length_toList (h : t.WF) : (toList t).length = t.size := by simp_to_model [Const.toList, size] using List.length_map +theorem size_toArray (h : t.WF) : + (toArray t).size = t.size := by + rw [← toArray_toList, List.size_toArray, length_toList h] + 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 [Const.toList, isEmpty] using List.map_eq_nil_iff +theorem isEmpty_toArray : + (toArray t).isEmpty = t.isEmpty := by + rw [← toArray_toList, List.isEmpty_toArray, isEmpty_toList] + 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 [Const.toList, Const.get?] using List.mem_map_toProd_iff_getValue?_eq_some +theorem mem_toArray_iff_get?_eq_some [TransOrd α] [LawfulEqOrd α] {k : α} {v : β} (h : t.WF) : + (k, v) ∈ toArray t ↔ get? t k = some v := by + rw [← toArray_toList, List.mem_toArray, mem_toList_iff_get?_eq_some h] + 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 [Const.toList, getKey?, Const.get?] using List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some +theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k : α} {v : β} (h : t.WF) : + (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v := by + rw [← toArray_toList, List.mem_toArray, mem_toList_iff_getKey?_eq_some_and_get?_eq_some h] + 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 [Const.toList, Const.get?] using List.getValue?_eq_some_iff_exists_beq_and_mem_toList +theorem get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransOrd α] {k : α} {v : β} (h : t.WF) : + get? t k = some v ↔ ∃ (k' : α), compare k k' = .eq ∧ (k', v) ∈ toArray t := by + simp [← toArray_toList, List.mem_toArray, ← 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 [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 [Const.toList, getKey?, Const.get?] using List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some +theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransOrd α] {k k' : α} {v : β} + (h : t.WF) : (toArray t).find? (fun a => compare a.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ get? t k = some v := by + rw [← toArray_toList, List.find?_toArray, find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some h] + 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 [Const.toList, contains] using List.find?_map_eq_none_iff_containsKey_eq_false +theorem find?_toArray_eq_none_iff_contains_eq_false [TransOrd α] {k : α} (h : t.WF) : + (toArray t).find? (compare ·.1 k == .eq) = none ↔ t.contains k = false := by + rw [← toArray_toList, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false h] + 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 find?_toArray_eq_none_iff_not_mem [TransOrd α] {k : α} (h : t.WF) : + (toArray t).find? (compare ·.1 k == .eq) = none ↔ ¬ k ∈ t := by + simpa only [Bool.not_eq_true, mem_iff_contains] using find?_toArray_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_to_model [Const.toList] using List.pairwise_fst_eq_false_map_toProd +theorem distinct_keys_toArray [TransOrd α] (h : t.WF) : + (toArray t).toList.Pairwise (fun a b => ¬ compare a.1 b.1 = .eq) := by + simp [toList_toArray, distinct_keys_toList h] + theorem ordered_keys_toList [TransOrd α] (h : t.WF) : (toList t).Pairwise (fun a b => compare a.1 b.1 = .lt) := by simp_to_model [Const.toList] exact h.ordered.map _ fun _ _ hcmp => hcmp +theorem ordered_keys_toArray [TransOrd α] (h : t.WF) : + (toArray t).toList.Pairwise (fun a b => compare a.1 b.1 = .lt) := by + simp [toList_toArray, ordered_keys_toList h] + end Const section monadic @@ -1765,53 +1918,105 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := by simp_to_model [toList, foldlM] +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] + {f : δ → (a : α) → β a → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := by + rw [foldlM_eq_foldlM_toList, ← toArray_toList, List.foldlM_toArray] + theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} : t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := by simp_to_model [toList, foldl] +theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} : + t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := by + rw [foldl_eq_foldl_toList, ← toArray_toList, List.foldl_toArray] + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := by simp_to_model [toList, foldrM] +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] + {f : (a : α) → β a → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := by + rw [foldrM_eq_foldrM_toList, ← toArray_toList, List.foldrM_toArray] + theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := by simp_to_model [toList, foldr] +theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := by + rw [foldr_eq_foldr_toList, ← toArray_toList, List.foldr_toArray] + theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} : t.forM (fun k v => f ⟨k, v⟩) = ForM.forM t.toList f := by simp_to_model [toList, forM] using rfl +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} : + t.forM (fun k v => f ⟨k, v⟩) = ForM.forM t.toArray f := by + simp [forM_eq_forM_toList, ← toArray_toList, List.forM_toArray] + theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} : t.forIn (fun k v => f ⟨k, v⟩) init = ForIn.forIn t.toList init f := by simp_to_model [toList, forIn] +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} : + t.forIn (fun k v => f ⟨k, v⟩) init = ForIn.forIn t.toArray init f := by + rw [forIn_eq_forIn_toList, ← toArray_toList, List.forIn_toArray] + theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := by simp_to_model [foldlM, keys] using List.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := by + rw [foldlM_eq_foldlM_keys, ← toArray_keys, List.foldlM_toArray] + theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} : t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := by simp_to_model [foldl, keys] using List.foldl_eq_foldl_keys +theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} : + t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := by + rw [foldl_eq_foldl_keys, ← toArray_keys, List.foldl_toArray] + theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := by simp_to_model [foldrM, keys] using List.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : + t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := by + rw [foldrM_eq_foldrM_keys, ← toArray_keys, List.foldrM_toArray] + theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} : t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := by simp_to_model [foldr, keys] using List.foldr_eq_foldr_keys +theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} : + t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := by + rw [foldr_eq_foldr_keys, ← toArray_keys, List.foldr_toArray] + theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} : t.forM (fun a _ => f a) = t.keys.forM f := by simp_to_model [forM, keys] using List.forM_eq_forM_keys +theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + t.forM (fun a _ => f a) = t.keysArray.forM f := by + rw [forM_eq_forM_keys, ← toArray_keys, List.forM_toArray' _ _ rfl] + theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : t.forIn (fun a _ d => f a d) init = ForIn.forIn t.keys init f := by simp_to_model [forIn, keys] using List.forIn_eq_forIn_keys +theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} + {init : δ} : + t.forIn (fun a _ d => f a d) init = ForIn.forIn t.keysArray init f := by + rw [forIn_eq_forIn_keys, ← toArray_keys, List.forIn_toArray] + namespace Const variable {β : Type v} {t : Impl α β} @@ -1821,28 +2026,55 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init := by simp_to_model [foldlM, Const.toList] using List.foldlM_eq_foldlM_toProd +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] + {f : δ → (a : α) → β → m δ} {init : δ} : + t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init := by + rw [foldlM_eq_foldlM_toList, ← toArray_toList, List.foldlM_toArray] + theorem foldl_eq_foldl_toList {f : δ → (a : α) → β → δ} {init : δ} : t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init := by simp_to_model [foldl, Const.toList] using List.foldl_eq_foldl_toProd +theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β → δ} {init : δ} : + t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init := by + rw [foldl_eq_foldl_toList, ← toArray_toList, List.foldl_toArray] + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β → δ → m δ} {init : δ} : t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init := by simp_to_model [foldrM, Const.toList] using List.foldrM_eq_foldrM_toProd +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] + {f : (a : α) → β → δ → m δ} {init : δ} : + t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init := by + rw [foldrM_eq_foldrM_toList, ← toArray_toList, List.foldrM_toArray] + theorem foldr_eq_foldr_toList {f : (a : α) → β → δ → δ} {init : δ} : t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init := by simp_to_model [foldr, Const.toList] using List.foldr_eq_foldr_toProd +theorem foldr_eq_foldr_toArray {f : (a : α) → β → δ → δ} {init : δ} : + t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init := by + rw [foldr_eq_foldr_toList, ← toArray_toList, List.foldr_toArray] + theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β → m PUnit} : t.forM f = (Const.toList t).forM (fun a => f a.1 a.2) := by simp_to_model [forM, Const.toList] using List.forM_eq_forM_toProd +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β → m PUnit} : + t.forM f = (Const.toArray t).forM (fun a => f a.1 a.2) := by + rw [forM_eq_forM_toList, ← toArray_toList, List.forM_toArray' _ _ rfl] + theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : t.forIn f init = ForIn.forIn (Const.toList t) init (fun a b => f a.1 a.2 b) := by simp_to_model [forIn, Const.toList] using List.forIn_eq_forIn_toProd +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α → β → δ → m (ForInStep δ)} {init : δ} : + t.forIn f init = ForIn.forIn (Const.toArray t) init (fun a b => f a.1 a.2 b) := by + rw [forIn_eq_forIn_toList, ← toArray_toList, List.forIn_toArray] + end Const end monadic @@ -7108,6 +7340,10 @@ 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?_eq_getElem?_keysArray [TransOrd α] (h : t.WF) : + t.minKey? = t.keysArray[0]? := by + simp [minKey?_eq_head?_keys h, ← toList_keysArray, List.head?_eq_getElem?, Array.getElem?_toList] + theorem minKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) : (t.modify k f).minKey? = t.minKey? := by simp_to_model [modify, minKey?] using List.minKey?_modifyKey @@ -7262,6 +7498,11 @@ 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_eq_getElem_keysArray [TransOrd α] (h : t.WF) {he} : + t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray h, isEmpty_eq_size_eq_zero h] using he)) := by + simp [minKey_eq_head_keys h, List.head_eq_iff_head?_eq_some, ← toList_keysArray, List.head?_eq_getElem?, Array.getElem?_toList, + getElem?_eq_some_getElem_iff] + 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 @@ -7460,6 +7701,10 @@ 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!_eq_getElem!_keysArray [TransOrd α] [Inhabited α] (h : t.WF) : + t.minKey! = t.keysArray[0]! := by + simp [minKey!_eq_head!_keys h, ← toList_keysArray, List.head!_eq_getElem!, Array.getElem!_eq_getD] + 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 @@ -7677,6 +7922,10 @@ 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_eq_getD_keysArray [TransOrd α] (h : t.WF) {fallback} : + t.minKeyD fallback = t.keysArray.getD 0 fallback := by + simp [minKeyD_eq_headD_keys h, ← toList_keysArray, List.head?_eq_getElem?] + 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 @@ -7945,6 +8194,10 @@ theorem maxKey?_eq_getLast?_keys [TransOrd α] (h : t.WF) : t.maxKey? = t.keys.getLast? := by simp_to_model [maxKey?, keys] using List.maxKey?_eq_getLast?_keys _ h.ordered +theorem maxKey?_eq_back?_keysArray [TransOrd α] (h : t.WF) : + t.maxKey? = t.keysArray.back? := by + simp [maxKey?_eq_getLast?_keys h, ← toList_keysArray] + theorem maxKey?_modify [TransOrd α] [LawfulEqOrd α] {k f} (h : t.WF) : (t.modify k f).maxKey? = t.maxKey? := by simp_to_model [modify, maxKey?] using List.maxKey?_modifyKey @@ -8095,6 +8348,10 @@ theorem maxKey_eq_getLast_keys [TransOrd α] (h : t.WF) {he} : t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := by simp_to_model [maxKey, keys] using List.maxKey_eq_getLast_keys h.ordered.distinctKeys h.ordered +theorem maxKey_eq_back_keysArray [TransOrd α] (h : t.WF) {he} : + t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray h, isEmpty_eq_size_eq_zero h] using he)) := by + simp [maxKey_eq_getLast_keys h, ← toArray_keys, List.back_toArray] + theorem maxKey_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) {k f he} : (t.modify k f).maxKey he = t.maxKey (isEmpty_modify h ▸ he):= by simp_to_model [maxKey, modify] using List.maxKey_modifyKey @@ -8293,6 +8550,10 @@ theorem maxKey!_eq_getLast!_keys [TransOrd α] [Inhabited α] (h : t.WF) : t.maxKey! = t.keys.getLast! := by simp_to_model [maxKey!, keys] using List.maxKey!_eq_getLast!_keys h.ordered.distinctKeys h.ordered +theorem maxKey!_eq_back!_keysArray [TransOrd α] [Inhabited α] (h : t.WF) : + t.maxKey! = t.keysArray.back! := by + simp [maxKey!_eq_getLast!_keys h, ← toArray_keys] + theorem maxKey!_modify [TransOrd α] [LawfulEqOrd α] [Inhabited α] (h : t.WF) : ∀ {k f}, (t.modify k f).maxKey! = t.maxKey! := by simp_to_model [maxKey!, modify] using List.maxKey!_modifyKey @@ -8510,6 +8771,10 @@ theorem maxKeyD_eq_getLastD_keys [TransOrd α] (h : t.WF) {fallback} : t.maxKeyD fallback = t.keys.getLastD fallback := by simp_to_model [maxKeyD, keys] using List.maxKeyD_eq_getLastD_keys h.ordered.distinctKeys h.ordered +theorem maxKeyD_eq_getD_back?_keysArray [TransOrd α] (h : t.WF) {fallback} : + t.maxKeyD fallback = t.keysArray.back?.getD fallback := by + simp [maxKeyD_eq_getLastD_keys h, ← toList_keysArray] + theorem maxKeyD_modify [TransOrd α] [LawfulEqOrd α] (h : t.WF) : ∀ {k f fallback}, (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback := by simp_to_model [maxKeyD, modify] using List.maxKeyD_modifyKey @@ -9306,13 +9571,24 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := by simp_to_model [toList, Equiv] +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := by + rw [equiv_iff_toList_perm, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂), + Array.perm_iff_toList_perm] + theorem Equiv.of_toList_perm : t₁.toList.Perm t₂.toList → t₁ ~m t₂ := equiv_iff_toList_perm.mpr +theorem Equiv.of_toArray_perm : t₁.toArray.Perm t₂.toArray → t₁ ~m t₂ := + equiv_iff_toArray_perm.mpr + theorem equiv_iff_toList_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := ⟨Equiv.toList_eq h₁ h₂, .of_toList_perm ∘ .of_eq⟩ +theorem equiv_iff_toArray_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := by + simp [equiv_iff_toList_eq h₁ h₂, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂)] + theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} (h : t₁.WF) : t₁.insertMany l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by rw [insertMany_eq_foldl] @@ -9341,12 +9617,20 @@ theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm have := h.map (fun (x, y) => (⟨x, y⟩ : (_ : α) × β)) simpa only [List.map_map, Function.comp_def, List.map_id'] using this +theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) := by + rw [Const.equiv_iff_toList_perm, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂), + Array.perm_iff_toList_perm] + theorem Const.equiv_iff_toList_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ := by simp_to_model [Const.toList] rw [List.map_inj_right fun _ _ => congrArg fun x : α × β => (⟨x.1, x.2⟩ : (_ : α) × β)] exact ⟨(·.toListModel_eq h₁.ordered h₂.ordered), .mk ∘ .of_eq⟩ +theorem Const.equiv_iff_toArray_eq [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ := by + simp [Const.equiv_iff_toList_eq h₁ h₂, ← toArray_toList (t := t₁), ← toArray_toList (t := t₂)] + theorem Const.equiv_iff_keys_perm {t₁ t₂ : Impl α Unit} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := by simp_to_model [keys, Equiv] @@ -9357,6 +9641,19 @@ theorem Const.equiv_iff_keys_perm {t₁ t₂ : Impl α Unit} : have := h.map (fun x => (⟨x, ()⟩ : (_ : α) × Unit)) simpa only [List.map_map, Function.comp_def, List.map_id'] using this +theorem Const.Equiv.of_keys_perm {t₁ t₂ : Impl α Unit} : + t₁.keys.Perm t₂.keys → t₁ ~m t₂ := + Const.equiv_iff_keys_perm.mpr + +theorem Const.equiv_iff_keysArray_perm {t₁ t₂ : Impl α Unit} : + t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := by + rw [Const.equiv_iff_keys_perm, ← toArray_keys (t := t₁), ← toArray_keys (t := t₂), + Array.perm_iff_toList_perm] + +theorem Const.Equiv.of_keysArray_perm {t₁ t₂ : Impl α Unit} : + t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ := + Const.equiv_iff_keysArray_perm.mpr + theorem Const.equiv_iff_keys_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.keys = t₂.keys := by simp_to_model [keys] @@ -9364,6 +9661,10 @@ theorem Const.equiv_iff_keys_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ : rw [List.map_inj_right fun _ _ => congrArg fun x : α => (⟨x, ()⟩ : (_ : α) × Unit)] exact ⟨(·.toListModel_eq h₁.ordered h₂.ordered), .mk ∘ .of_eq⟩ +theorem Const.equiv_iff_keysArray_eq {t₁ t₂ : Impl α Unit} [TransOrd α] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := by + simp [Const.equiv_iff_keys_eq h₁ h₂, ← toArray_keys (t := t₁), ← toArray_keys (t := t₂)] + theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} (h : t₁.WF) : insertMany t₁ l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insert! p.1 p.2) := by rw [insertMany_eq_foldl] @@ -9393,11 +9694,21 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) : t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by simp_to_model [filterMap, toList, Equiv] +theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) : + (t.filterMap f h.balanced).1.toArray = + t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by + rw [← toArray_toList, toList_filterMap h, ← toArray_toList, List.filterMap_toArray] + theorem toList_filterMap! {f : (a : α) → β a → Option (γ a)} (h : t.WF) : (t.filterMap! f).toList = t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by simpa only [filterMap_eq_filterMap!] using toList_filterMap h +theorem toArray_filterMap! {f : (a : α) → β a → Option (γ a)} (h : t.WF) : + (t.filterMap! f).toArray = + t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by + simpa only [filterMap_eq_filterMap!] using toArray_filterMap h + theorem isEmpty_filterMap_iff [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Option (γ a)} (h : t.WF) : (t.filterMap f h.balanced).1.isEmpty = true ↔ @@ -9740,11 +10051,21 @@ theorem toList_filterMap {f : α → β → Option γ} (h : t.WF) : simp_to_model [Const.toList, filterMap] simp only [List.map_filterMap, List.filterMap_map, Function.comp_def, Option.map_map] +theorem toArray_filterMap {f : α → β → Option γ} (h : t.WF) : + Const.toArray (t.filterMap f h.balanced).1 = + (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by + rw [← toArray_toList, toList_filterMap h, ← toArray_toList, List.filterMap_toArray] + theorem toList_filterMap! {f : α → β → Option γ} (h : t.WF) : Const.toList (t.filterMap! f) = (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by simpa only [filterMap_eq_filterMap!] using toList_filterMap h +theorem toArray_filterMap! {f : α → β → Option γ} (h : t.WF) : + Const.toArray (t.filterMap! f) = + (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := by + simpa only [filterMap_eq_filterMap!] using toArray_filterMap h + theorem getKey?_filterMap [TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF) : (t.filterMap f h.balanced).1.getKey? k = @@ -9808,19 +10129,36 @@ theorem toList_filter {f : (a : α) → β a → Bool} (h : t.WF) : (t.filter f h.balanced).1.toList = t.toList.filter (fun p => f p.1 p.2) := by simp_to_model [filter, toList, Equiv] +theorem toArray_filter {f : (a : α) → β a → Bool} (h : t.WF) : + (t.filter f h.balanced).1.toArray = t.toArray.filter (fun p => f p.1 p.2) := by + simp_to_model [filter, toArray, Equiv] + simp + theorem toList_filter! {f : (a : α) → β a → Bool} (h : t.WF) : (t.filter! f).toList = t.toList.filter (fun p => f p.1 p.2) := by simpa only [filter_eq_filter!] using toList_filter h +theorem toArray_filter! {f : (a : α) → β a → Bool} (h : t.WF) : + (t.filter! f).toArray = t.toArray.filter (fun p => f p.1 p.2) := by + simpa only [filter_eq_filter!] using toArray_filter h + theorem keys_filter_key {f : α → Bool} (h : t.WF) : (t.filter (fun k _ => f k) h.balanced).1.keys = t.keys.filter f := by simp_to_model [keys, filter] simp only [List.keys_eq_map, List.filter_map, Function.comp_def] +theorem keysArray_filter_key {f : α → Bool} (h : t.WF) : + (t.filter (fun k _ => f k) h.balanced).1.keysArray = t.keysArray.filter f := by + rw [← toArray_keys, keys_filter_key h, ← toArray_keys, List.filter_toArray] + theorem keys_filter!_key {f : α → Bool} (h : t.WF) : (t.filter! (fun k _ => f k)).keys = t.keys.filter f := by simpa only [filter_eq_filter!] using keys_filter_key h +theorem keysArray_filter!_key {f : α → Bool} (h : t.WF) : + (t.filter! (fun k _ => f k)).keysArray = t.keysArray.filter f := by + simpa only [filter_eq_filter!] using keysArray_filter_key h + theorem isEmpty_filter_iff [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) : (t.filter f h.balanced).1.isEmpty = true ↔ @@ -10001,11 +10339,36 @@ theorem keys_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bo rw [List.keys_filter h.ordered.distinctKeys] simp only [List.filter_map, Function.comp_def, List.unattach, List.map_map] +private theorem List.unattach_filter_eq_if {p : α → Prop} {l : List { x // p x }} + {f : { x // p x } → Bool} : + open scoped Classical in + (l.filter f).unattach = l.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by + apply List.unattach_filter + simp +contextual + +private theorem Array.unattach_filter_eq_if {p : α → Prop} {xs : Array { x // p x }} + {f : { x // p x } → Bool} : + open scoped Classical in + (xs.filter f).unattach = xs.unattach.filter (fun x => if h : p x then f ⟨x, h⟩ else false) := by + apply Array.unattach_filter + simp +contextual + +theorem keysArray_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) : + (t.filter f h.balanced).1.keysArray = + (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keysArray h h')))).unattach := by + simp only [← toArray_keys, keys_filter h, List.unattach_filter_eq_if, Array.unattach_filter_eq_if] + simp [← toArray_keys] + theorem keys_filter! [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) : (t.filter! f).keys = (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keys h h')))).unattach := by simpa only [filter_eq_filter!] using keys_filter h +theorem keysArray_filter! [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} (h : t.WF) : + (t.filter! f).keysArray = + (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (t.get x (mem_of_mem_keysArray h h')))).unattach := by + simpa only [filter_eq_filter!] using keysArray_filter h + theorem getKey?_filter [TransOrd α] [LawfulEqOrd α] {f : (a : α) → β a → Bool} {k : α} (h : t.WF) : (t.filter f h.balanced).1.getKey? k = @@ -10259,11 +10622,21 @@ theorem toList_filter {f : α → β → Bool} (h : t.WF) : simp_to_model [filter, Const.toList] simp only [List.filter_map, Function.comp_def] +theorem toArray_filter {f : α → β → Bool} (h : t.WF) : + Const.toArray (t.filter f h.balanced).1 = + (Const.toArray t).filter (fun p => f p.1 p.2) := by + rw [← toArray_toList, toList_filter h, ← toArray_toList, List.filter_toArray] + theorem toList_filter! {f : α → β → Bool} (h : t.WF) : Const.toList (t.filter! f) = (Const.toList t).filter (fun p => f p.1 p.2) := by simpa only [filter_eq_filter!] using toList_filter h +theorem toArray_filter! {f : α → β → Bool} (h : t.WF) : + Const.toArray (t.filter! f) = + (Const.toArray t).filter (fun p => f p.1 p.2) := by + simpa only [filter_eq_filter!] using toArray_filter h + theorem keys_filter [TransOrd α] {f : α → β → Bool} (h : t.WF): (t.filter f h.balanced).1.keys = (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach := by @@ -10272,11 +10645,29 @@ theorem keys_filter [TransOrd α] {f : α → β → Bool} (h : t.WF): rw [List.Const.keys_filter h.ordered.distinctKeys] simp only [List.filter_map, Function.comp_def, List.unattach, List.map_map] +theorem keysArray_filter [TransOrd α] {f : α → β → Bool} (h : t.WF): + (t.filter f h.balanced).1.keysArray = + (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keysArray h h')))).unattach := by + simp only [← toArray_keys, keys_filter h] + simp only [List.unattach_filter_eq_if, Array.unattach_filter_eq_if] + simp only [List.unattach_attach, Array.unattach_attach, ← toArray_keys, List.mem_toArray, + List.size_toArray, List.filter_toArray'] + congr; ext x + split <;> rename_i h' + all_goals + rw [← toList_keysArray, Array.mem_toList_iff] at h' + simp [h'] + theorem keys_filter! [TransOrd α] {f : α → β → Bool} (h : t.WF): (t.filter! f).keys = (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach := by simpa only [filter_eq_filter!] using keys_filter h +theorem keysArray_filter! [TransOrd α] {f : α → β → Bool} (h : t.WF): + (t.filter! f).keysArray = + (t.keysArray.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keysArray h h')))).unattach := by + simpa only [filter_eq_filter!] using keysArray_filter h + theorem getKey?_filter [TransOrd α] {f : α → β → Bool} {k : α} (h : t.WF) : (t.filter f h.balanced).1.getKey? k = @@ -10338,10 +10729,17 @@ theorem toList_map {f : (a : α) → β a → γ a} : (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) := by simp_to_model [map, toList, Equiv] +theorem toArray_map {f : (a : α) → β a → γ a} : + (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) := by + rw [← toArray_toList, toList_map, ← toArray_toList, List.map_toArray] + theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys := by simp_to_model [keys, map, Equiv] rw [List.keys_map] +theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray := by + rw [← toArray_keys, keys_map, toArray_keys] + theorem filterMap_equiv_map {f : (a : α) → β a → γ a} (h : t.WF) : (t.filterMap (fun k v => some (f k v)) h.balanced).1.Equiv (t.map f) := by @@ -10483,6 +10881,10 @@ theorem toList_map {f : α → β → γ} : simp_to_model [map, Const.toList] simp only [List.map_map, Function.comp_def] +theorem toArray_map {f : α → β → γ} : + Const.toArray (t.map f) = (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) := by + rw [← toArray_toList, toList_map, ← toArray_toList, List.map_toArray] + end Const end map diff --git a/src/Std/Data/DTreeMap/Internal/Model.lean b/src/Std/Data/DTreeMap/Internal/Model.lean index 468e8ae357..0bd744965d 100644 --- a/src/Std/Data/DTreeMap/Internal/Model.lean +++ b/src/Std/Data/DTreeMap/Internal/Model.lean @@ -661,7 +661,7 @@ theorem minKey?_eq_minEntry?_map_fst {l : Impl α β} : l.minKey? = l.minEntry?. theorem minKey_eq_minEntry_fst {l : Impl α β} {he} : l.minKey he = (l.minEntry he).fst := by induction l, he using minKey.induct_unfolding <;> simp only [minEntry] <;> trivial -theorem minKey!_eq_get!_minKey? [Inhabited α] {l : Impl α β} : +theorem minKey!_eq_getElem!_minKey? [Inhabited α] {l : Impl α β} : l.minKey! = l.minKey?.get! := by induction l using minKey!.induct_unfolding <;> simp only [minKey?] <;> trivial diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 527c6990f7..97d1868af7 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -2296,7 +2296,7 @@ theorem minKey_eq_minKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : theorem minKey!_eq_minKey! [Ord α] [TransOrd α] [Inhabited α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) : l.minKey! = List.minKey! l.toListModel := by - simp [Impl.minKey!_eq_get!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo] + simp [Impl.minKey!_eq_getElem!_minKey?, List.minKey!_eq_get!_minKey?, minKey?_eq_minKey? hlo] theorem minKeyD_eq_minKeyD [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] {l : Impl α β} (hlo : l.Ordered) {fallback} : diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 2a3b1e1a9e..c135381173 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -8,6 +8,7 @@ module prelude import Std.Data.DTreeMap.Internal.Lemmas public import Std.Data.DTreeMap.AdditionalOperations +public import Init.Data.Array.Perm import Init.Data.List.Pairwise import Init.Data.Prod @@ -362,14 +363,26 @@ end Const theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} : (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := Impl.toList_insert_perm t.wf +theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} : + (t.insert k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := + Impl.toArray_insert_perm t.wf + theorem Const.toList_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} : (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := Impl.Const.toList_insert_perm t.2 +theorem Const.toArray_insert_perm {β : Type v} {t : DTreeMap α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} : + (Const.toArray (t.insert k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := + Impl.Const.toArray_insert_perm t.2 + theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} : (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) := Impl.keys_insertIfNew_perm t.2 +theorem keysArray_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β k} : + (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) := + Impl.keysArray_insertIfNew_perm t.2 + @[simp] theorem get_insert_self [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : (t.insert k v).get k mem_insert_self = v := @@ -1094,24 +1107,47 @@ theorem length_keys [TransCmp cmp] : t.keys.length = t.size := Impl.length_keys t.wf +@[simp, grind =] +theorem size_keysArray [TransCmp cmp] : + t.keysArray.size = t.size := + Impl.size_keysArray t.wf + @[simp, grind =] theorem isEmpty_keys : t.keys.isEmpty = t.isEmpty := Impl.isEmpty_keys +@[simp, grind =] +theorem isEmpty_keysArray : + t.keysArray.isEmpty = t.isEmpty := + Impl.isEmpty_keysArray + @[simp, grind =] theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : t.keys.contains k = t.contains k := Impl.contains_keys t.wf +@[simp, grind =] +theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.keysArray.contains k = t.contains k := + Impl.contains_keysArray t.wf + @[simp, grind =] theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : k ∈ t.keys ↔ k ∈ t := Impl.mem_keys t.wf +@[simp, grind =] +theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.keysArray ↔ k ∈ t := + Impl.mem_keysArray t.wf + theorem mem_of_mem_keys [TransCmp cmp] {k : α} (h : k ∈ t.keys) : k ∈ t := Impl.mem_of_mem_keys t.wf h +theorem mem_of_mem_keysArray [TransCmp cmp] {k : α} (h : k ∈ t.keysArray) : k ∈ t := + Impl.mem_of_mem_keysArray t.wf h + theorem distinct_keys [TransCmp cmp] : t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := Impl.distinct_keys t.wf @@ -1129,34 +1165,67 @@ theorem map_fst_toList_eq_keys : t.toList.map Sigma.fst = t.keys := Impl.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + t.toArray.map Sigma.fst = t.keysArray := + Impl.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList [TransCmp cmp] : t.toList.length = t.size := Impl.length_toList t.wf +@[simp, grind =] +theorem size_toArray [TransCmp cmp] : + t.toArray.size = t.size := + Impl.size_toArray t.wf + @[simp, grind =] theorem isEmpty_toList : t.toList.isEmpty = t.isEmpty := Impl.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + t.toArray.isEmpty = t.isEmpty := + Impl.isEmpty_toArray + @[simp, grind =] 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 +@[simp, grind =] +theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v := + Impl.mem_toArray_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?_toArray_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β k} : + t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := + Impl.find?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + t.toArray.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + t.toArray.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.find?_toArray_eq_none_iff_not_mem t.wf + theorem distinct_keys_toList [TransCmp cmp] : t.toList.Pairwise (fun a b => ¬ cmp a.1 b.1 = .eq) := Impl.distinct_keys_toList t.wf @@ -1174,44 +1243,87 @@ theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := Impl.Const.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + (toArray t).map Prod.fst = t.keysArray := + Impl.Const.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList : (toList t).length = t.size := Impl.Const.length_toList t.wf +@[simp, grind =] +theorem size_toArray : + (toArray t).size = t.size := + Impl.Const.size_toArray t.wf + @[simp, grind =] theorem isEmpty_toList : (toList t).isEmpty = t.isEmpty := Impl.Const.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + (toArray t).isEmpty = t.isEmpty := + Impl.Const.isEmpty_toArray + @[simp, grind =] 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, grind =] +theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} : + (k, v) ∈ toArray t ↔ get? t k = some v := + Impl.Const.mem_toArray_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 +@[simp] +theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v := + Impl.Const.mem_toArray_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 get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] {k : α} {v : β} : + get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t := + Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray 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?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] {k k' : α} {v : β} : + (toArray t).find? (cmp ·.1 k == .eq) = some (k', v) ↔ + t.getKey? k = some k' ∧ get? t k = some v := + Impl.Const.find?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.Const.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.Const.find?_toArray_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 @@ -1231,18 +1343,35 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := Impl.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] + {f : δ → (a : α) → β a → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := + Impl.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} : t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := Impl.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} : + t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := + Impl.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := Impl.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := + Impl.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := Impl.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := + Impl.foldr_eq_foldr_toArray + @[simp, grind =] theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} : t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl @@ -1251,6 +1380,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a → ForM.forM t f = ForM.forM t.toList f := Impl.forM_eq_forM_toList +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} : + ForM.forM t f = ForM.forM t.toArray f := + Impl.forM_eq_forM_toArray + @[simp, grind =] theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : @@ -1261,32 +1394,63 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] ForIn.forIn t init f = ForIn.forIn t.toList init f := Impl.forIn_eq_forIn_toList (f := f) +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := + Impl.forIn_eq_forIn_toArray (f := f) + theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := Impl.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := + Impl.foldlM_eq_foldlM_keysArray + theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} : t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := Impl.foldl_eq_foldl_keys +theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} : + t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := + Impl.foldl_eq_foldl_keysArray + theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := Impl.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] + {f : α → δ → m δ} {init : δ} : + t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := + Impl.foldrM_eq_foldrM_keysArray + theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} : t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := Impl.foldr_eq_foldr_keys +theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} : + t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := + Impl.foldr_eq_foldr_keysArray + theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t (fun a => f a.1) = t.keys.forM f := Impl.forM_eq_forM_keys +theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t (fun a => f a.1) = t.keysArray.forM f := + Impl.forM_eq_forM_keysArray + theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f := Impl.forIn_eq_forIn_keys +theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] + {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f := + Impl.forIn_eq_forIn_keysArray + namespace Const variable {β : Type v} {t : DTreeMap α β cmp} @@ -1296,19 +1460,37 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init := Impl.Const.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] + {f : δ → α → β → m δ} {init : δ} : + t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init := + Impl.Const.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} : t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init := Impl.Const.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} : + t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init := + Impl.Const.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init := Impl.Const.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] + {f : α → β → δ → m δ} {init : δ} : + t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init := + Impl.Const.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} : t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init := Impl.Const.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} : + t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init := + Impl.Const.foldr_eq_foldr_toArray + theorem forM_eq_forMUncurried [Monad m] [LawfulMonad m] {f : α → β → m PUnit} : t.forM f = forMUncurried (fun a => f a.1 a.2) t := rfl @@ -1316,6 +1498,10 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → forMUncurried f t = (Const.toList t).forM f := Impl.Const.forM_eq_forM_toList +theorem forMUncurried_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} : + forMUncurried f t = (Const.toArray t).forM f := + Impl.Const.forM_eq_forM_toArray + theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl @@ -1325,6 +1511,11 @@ theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m] forInUncurried f init t = ForIn.forIn (Const.toList t) init f := Impl.Const.forIn_eq_forIn_toList +theorem forInUncurried_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α × β → δ → m (ForInStep δ)} {init : δ} : + forInUncurried f init t = ForIn.forIn (Const.toArray t) init f := + Impl.Const.forIn_eq_forIn_toArray + end Const end monadic @@ -4173,6 +4364,11 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} : t.minKey? = t.keys.head? := Impl.minKey?_eq_head?_keys t.wf +@[grind =_] +theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] : + t.minKey? = t.keysArray[0]? := + Impl.minKey?_eq_getElem?_keysArray t.wf + @[simp, grind =] theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} : (t.modify k f).minKey? = t.minKey? := @@ -4325,6 +4521,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} : t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := Impl.minKey_eq_head_keys t.wf +@[grind =_] theorem minKey_eq_getElem_keysArray [TransCmp cmp] {he} : + t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) := + Impl.minKey_eq_getElem_keysArray t.wf + @[simp, grind =] theorem minKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} : (t.modify k f).minKey he = t.minKey (cast (congrArg (· = false) isEmpty_modify) he) := @@ -4473,6 +4673,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] {k v} : t.minKey! = t.keys.head! := Impl.minKey!_eq_head!_keys t.wf +theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] : + t.minKey! = t.keysArray[0]! := + Impl.minKey!_eq_getElem!_keysArray t.wf + @[simp] theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} : (t.modify k f).minKey! = t.minKey! := @@ -4614,6 +4818,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} : t.minKeyD fallback = t.keys.headD fallback := Impl.minKeyD_eq_headD_keys t.wf +theorem minKeyD_eq_getD_keysArray [TransCmp cmp] {fallback} : + t.minKeyD fallback = t.keysArray.getD 0 fallback := + Impl.minKeyD_eq_getD_keysArray t.wf + @[simp, grind =] theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} : (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback := @@ -4816,6 +5024,10 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} : t.maxKey? = t.keys.getLast? := Impl.maxKey?_eq_getLast?_keys t.wf +@[grind =_] theorem maxKey?_eq_back?_keysArray [TransCmp cmp] : + t.maxKey? = t.keysArray.back? := + Impl.maxKey?_eq_back?_keysArray t.wf + @[simp, grind =] theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} : (t.modify k f).maxKey? = t.maxKey? := @@ -4969,6 +5181,10 @@ theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} : t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := Impl.maxKey_eq_getLast_keys t.wf +@[grind =_] theorem maxKey_eq_back_keysArray [TransCmp cmp] {he} : + t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) := + Impl.maxKey_eq_back_keysArray t.wf + @[simp] theorem maxKey_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f he} : (t.modify k f).maxKey he = t.maxKey (cast (congrArg (· = false) isEmpty_modify) he) := @@ -5118,6 +5334,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] : t.maxKey! = t.keys.getLast! := Impl.maxKey!_eq_getLast!_keys t.wf +theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] : + t.maxKey! = t.keysArray.back! := + Impl.maxKey!_eq_back!_keysArray t.wf + @[simp] theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] {k f} : (t.modify k f).maxKey! = t.maxKey! := @@ -5261,6 +5481,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] {fallback} : t.maxKeyD fallback = t.keys.getLastD fallback := Impl.maxKeyD_eq_getLastD_keys t.wf +theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] {fallback} : + t.maxKeyD fallback = t.keysArray.back?.getD fallback := + Impl.maxKeyD_eq_getD_back?_keysArray t.wf + @[simp] theorem maxKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f fallback} : (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback := @@ -5906,13 +6130,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff_equiv.trans Impl.equiv_iff_toList_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff_equiv.trans Impl.equiv_iff_toArray_perm + theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_toList_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_toArray_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff_equiv.trans (Impl.equiv_iff_toList_eq t₁.2 t₂.2) +theorem equiv_iff_toArray_eq [TransCmp cmp] : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff_equiv.trans (Impl.equiv_iff_toArray_eq t₁.2 t₂.2) + theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} : t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by constructor @@ -5940,22 +6174,43 @@ variable {β : Type v} {t₁ t₂ : DTreeMap α β cmp} theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm (Const.toList t₂) := equiv_iff_equiv.trans Impl.Const.equiv_iff_toList_perm +theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) := + equiv_iff_equiv.trans Impl.Const.equiv_iff_toArray_perm + theorem Const.equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ := equiv_iff_equiv.trans (Impl.Const.equiv_iff_toList_eq t₁.2 t₂.2) +theorem Const.equiv_iff_toArray_eq [TransCmp cmp] : t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ := + equiv_iff_equiv.trans (Impl.Const.equiv_iff_toArray_eq t₁.2 t₂.2) + theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := equiv_iff_equiv.trans Impl.Const.equiv_iff_keys_perm +theorem Const.equiv_iff_keysArray_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := + equiv_iff_equiv.trans Impl.Const.equiv_iff_keysArray_perm + theorem Const.equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : DTreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys = t₂.keys := equiv_iff_equiv.trans (Impl.Const.equiv_iff_keys_eq t₁.2 t₂.2) +theorem Const.equiv_iff_keysArray_unit_eq [TransCmp cmp] {t₁ t₂ : DTreeMap α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := + equiv_iff_equiv.trans (Impl.Const.equiv_iff_keysArray_eq t₁.2 t₂.2) + theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) → t₁ ~m t₂ := Const.equiv_iff_toList_perm.mpr +theorem Equiv.of_constToArray_perm : (Const.toArray t₁).Perm (Const.toArray t₂) → t₁ ~m t₂ := + Const.equiv_iff_toArray_perm.mpr + theorem Equiv.of_keys_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ := Const.equiv_iff_keys_unit_perm.mpr +theorem Equiv.of_keysArray_unit_perm {t₁ t₂ : DTreeMap α Unit cmp} : + t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ := + Const.equiv_iff_keysArray_unit_perm.mpr + theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} : insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by constructor @@ -5994,6 +6249,12 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} : t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := Impl.toList_filterMap t.wf +@[simp, grind =] +theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} : + (t.filterMap f).toArray = + t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := + Impl.toArray_filterMap t.wf + @[grind =] theorem isEmpty_filterMap_iff [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} : @@ -6221,6 +6482,12 @@ theorem toList_filterMap (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := Impl.Const.toList_filterMap t.wf +theorem toArray_filterMap + {f : α → β → Option γ} : + Const.toArray (t.filterMap fun k v => f k v) = + (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := + Impl.Const.toArray_filterMap t.wf + @[grind =] theorem getKey?_filterMap [TransCmp cmp] {f : α → β → Option γ} {k : α} : @@ -6260,10 +6527,19 @@ theorem toList_filter {f : (a : α) → β a → Bool} : (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) := Impl.toList_filter t.wf +@[simp, grind =] +theorem toArray_filter {f : (a : α) → β a → Bool} : + (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) := + Impl.toArray_filter t.wf + theorem keys_filter_key {f : α → Bool} : (t.filter fun k _ => f k).keys = t.keys.filter f := Impl.keys_filter_key t.wf +theorem keysArray_filter_key {f : α → Bool} : + (t.filter fun k _ => f k).keysArray = t.keysArray.filter f := + Impl.keysArray_filter_key t.wf + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} : @@ -6536,6 +6812,12 @@ theorem toList_filter {f : α → β → Bool} : (toList t).filter (fun p => f p.1 p.2) := Impl.Const.toList_filter t.wf +@[simp, grind =] +theorem toArray_filter {f : α → β → Bool} : + toArray (t.filter f) = + (toArray t).filter (fun p => f p.1 p.2) := + Impl.Const.toArray_filter t.wf + theorem keys_filter [TransCmp cmp] {f : α → β → Bool} : (t.filter f).keys = (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h')))).unattach := @@ -6585,10 +6867,19 @@ theorem toList_map {f : (a : α) → β a → γ a} : (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) := Impl.toList_map +@[simp, grind =] +theorem toArray_map {f : (a : α) → β a → γ a} : + (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) := + Impl.toArray_map + @[simp, grind =] theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys := Impl.keys_map +@[simp, grind =] +theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray := + Impl.keysArray_map + theorem filterMap_equiv_map [TransCmp cmp] {f : (a : α) → β a → γ a} : (t.filterMap (fun k v => some (f k v))) ~m t.map f := @@ -6757,8 +7048,32 @@ theorem toList_map {f : α → β → γ} : (Const.toList t).map (fun p => (p.1, f p.1 p.2)) := Impl.Const.toList_map +@[simp, grind =] +theorem toArray_map {f : α → β → γ} : + (Const.toArray (t.map f)) = + (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) := + Impl.Const.toArray_map + +theorem toArray_toList : (toList t).toArray = toArray t := + Impl.Const.toArray_toList + +theorem toList_toArray : (toArray t).toList = toList t := + Impl.Const.toList_toArray + end Const end map +theorem toArray_toList : t.toList.toArray = t.toArray := + Impl.toArray_toList + +theorem toList_toArray : t.toArray.toList = t.toList := + Impl.toList_toArray + +theorem toArray_keys : t.keys.toArray = t.keysArray := + Impl.toArray_keys + +theorem toList_keysArray : t.keysArray.toList = t.keys := + Impl.toList_keysArray + end Std.DTreeMap diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index b1df4bf0de..e2c2ebe369 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -8,6 +8,7 @@ module prelude import Std.Data.DTreeMap.Internal.Lemmas public import Std.Data.DTreeMap.Raw.AdditionalOperations +public import Init.Data.Array.Perm import Init.Data.List.Find import Init.Data.List.Pairwise import Init.Data.Prod @@ -100,6 +101,18 @@ theorem isEmpty_iff_forall_not_mem [TransCmp cmp] (h : t.WF) : t.isEmpty = true ↔ ∀ a, ¬a ∈ t := Impl.isEmpty_iff_forall_not_mem h +theorem toArray_toList : t.toList.toArray = t.toArray := + Impl.toArray_toList + +theorem toList_toArray : t.toArray.toList = t.toList := + Impl.toList_toArray + +theorem toArray_keys : t.keys.toArray = t.keysArray := + Impl.toArray_keys + +theorem toList_keysArray : t.keysArray.toList = t.keys := + Impl.toList_keysArray + @[simp] theorem insert_eq_insert {p : (a : α) × β a} : Insert.insert p t = t.insert p.1 p.2 := rfl @@ -286,6 +299,12 @@ namespace Const variable {β : Type v} {t : Raw α β cmp} +theorem toArray_toList : (toList t).toArray = toArray t := + Impl.Const.toArray_toList + +theorem toList_toArray : (toArray t).toList = toList t := + Impl.Const.toList_toArray + @[simp, grind =] theorem get?_emptyc [TransCmp cmp] {a : α} : get? (∅ : Raw α β cmp) a = none := @@ -357,14 +376,26 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := Impl.toList_insert!_perm h +theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insert k v).toArray.Perm (t.toArray.filter (¬k == ·.1) |>.push ⟨k, v⟩) := + Impl.toArray_insert!_perm h + theorem Const.toList_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} : (Const.toList (t.insert k v)).Perm (⟨k, v⟩ :: (Const.toList t).filter (¬k == ·.1)) := Impl.Const.toList_insert!_perm h +theorem Const.toArray_insert_perm {β : Type v} {t : Raw α (fun _ => β) cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (Const.toArray (t.insert k v)).Perm ((Const.toArray t).filter (¬k == ·.1) |>.push ⟨k, v⟩) := + Impl.Const.toArray_insert!_perm h + theorem keys_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} : (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys) := Impl.keys_insertIfNew!_perm h +theorem keysArray_insertIfNew_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + (t.insertIfNew k v).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) := + Impl.keysArray_insertIfNew!_perm h.out + @[grind =] theorem get_insert [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k a : α} {v : β k} {h₁} : (t.insert k v).get a h₁ = if h₂ : cmp k a = .eq then @@ -1106,25 +1137,49 @@ theorem length_keys [TransCmp cmp] (h : t.WF) : t.keys.length = t.size := Impl.length_keys h.out +@[simp, grind =] +theorem size_keysArray [TransCmp cmp] (h : t.WF) : + t.keysArray.size = t.size := + Impl.size_keysArray h.out + @[simp, grind =] theorem isEmpty_keys : t.keys.isEmpty = t.isEmpty := Impl.isEmpty_keys +@[simp, grind =] +theorem isEmpty_keysArray : + t.keysArray.isEmpty = t.isEmpty := + Impl.isEmpty_keysArray + @[simp, grind =] theorem contains_keys [BEq α] [LawfulBEqCmp cmp] (h : t.WF) [TransCmp cmp] {k : α} : t.keys.contains k = t.contains k := Impl.contains_keys h +@[simp, grind =] +theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} (h : t.WF) : + t.keysArray.contains k = t.contains k := + Impl.contains_keysArray h.out + @[simp, grind =] theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.keys ↔ k ∈ t := Impl.mem_keys h +@[simp, grind =] +theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.keysArray ↔ k ∈ t := + Impl.mem_keysArray h + theorem mem_of_mem_keys [TransCmp cmp] (h : t.WF) {k : α} (h' : k ∈ t.keys) : k ∈ t := Impl.mem_of_mem_keys h h' +theorem mem_of_mem_keysArray [TransCmp cmp] (h : t.WF) {k : α} + (h' : k ∈ t.keysArray) : k ∈ t := + Impl.mem_of_mem_keysArray h h' + theorem distinct_keys [TransCmp cmp] (h : t.WF) : t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := Impl.distinct_keys h.out @@ -1142,34 +1197,67 @@ theorem map_fst_toList_eq_keys : t.toList.map Sigma.fst = t.keys := Impl.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + t.toArray.map Sigma.fst = t.keysArray := + Impl.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList [TransCmp cmp] (h : t.WF) : t.toList.length = t.size := Impl.length_toList h.out +@[simp, grind =] +theorem size_toArray [TransCmp cmp] (h : t.WF) : + t.toArray.size = t.size := + Impl.size_toArray h.out + @[simp, grind =] theorem isEmpty_toList : t.toList.isEmpty = t.isEmpty := Impl.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + t.toArray.isEmpty = t.isEmpty := + Impl.isEmpty_toArray + @[simp, grind =] 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 +@[simp, grind =] +theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β k} : + ⟨k, v⟩ ∈ t.toArray ↔ t.get? k = some v := + Impl.mem_toArray_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?_toArray_eq_some_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} + {v : β k} : t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k, v⟩ ↔ t.get? k = some v := + Impl.find?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + t.toArray.find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + t.toArray.find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.find?_toArray_eq_none_iff_not_mem h.out + 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 @@ -1187,45 +1275,89 @@ theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := Impl.Const.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + (toArray t).map Prod.fst = t.keysArray := + Impl.Const.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList (h : t.WF) : (toList t).length = t.size := Impl.Const.length_toList h.out +@[simp, grind =] +theorem size_toArray (h : t.WF) : + (toArray t).size = t.size := + Impl.Const.size_toArray h.out + @[simp, grind =] theorem isEmpty_toList : (toList t).isEmpty = t.isEmpty := Impl.Const.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + (toArray t).isEmpty = t.isEmpty := + Impl.Const.isEmpty_toArray + @[simp, grind =] 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, grind =] +theorem mem_toArray_iff_get?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toArray t ↔ get? t k = some v := + Impl.Const.mem_toArray_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 +@[simp] +theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ get? t k = some v := + Impl.Const.mem_toArray_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 get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + get? t k = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t := + Impl.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray 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?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some [TransCmp cmp] (h : t.WF) + {k k' : α} {v : β} : + (toArray 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?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + Impl.Const.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + Impl.Const.find?_toArray_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 @@ -1244,18 +1376,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → (a : α) t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := Impl.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → (a : α) → β a → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := + Impl.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → (a : α) → β a → δ} {init : δ} : t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := Impl.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} : + t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := + Impl.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := Impl.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := + Impl.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : (a : α) → β a → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := Impl.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : (a : α) → β a → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := + Impl.foldr_eq_foldr_toArray + @[simp, grind =] theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : (a : α) → β a → m PUnit} : t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl @@ -1264,6 +1412,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : (a : α) × β a → ForM.forM t f = ForM.forM t.toList f := Impl.forM_eq_forM_toList +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : (a : α) × β a → m PUnit} : + ForM.forM t f = ForM.forM t.toArray f := + Impl.forM_eq_forM_toArray + @[simp, grind =] theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : (a : α) → β a → δ → m (ForInStep δ)} {init : δ} : @@ -1274,31 +1426,61 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] ForIn.forIn t init f = ForIn.forIn t.toList init f := Impl.forIn_eq_forIn_toList (f := f) +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : (a : α) × β a → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := + Impl.forIn_eq_forIn_toArray (f := f) + theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := Impl.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := + Impl.foldlM_eq_foldlM_keysArray + theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} : t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := Impl.foldl_eq_foldl_keys +theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} : + t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := + Impl.foldl_eq_foldl_keysArray + theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := Impl.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : + t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := + Impl.foldrM_eq_foldrM_keysArray + theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} : t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := Impl.foldr_eq_foldr_keys +theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} : + t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := + Impl.foldr_eq_foldr_keysArray + theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t (fun a => f a.1) = t.keys.forM f := Impl.forM_eq_forM_keys +theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t (fun a => f a.1) = t.keysArray.forM f := + Impl.forM_eq_forM_keysArray + theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f := Impl.forIn_eq_forIn_keys +theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] + {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f := + Impl.forIn_eq_forIn_keysArray + namespace Const variable {β : Type v} {t : Raw α β cmp} @@ -1307,18 +1489,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β t.foldlM f init = (Const.toList t).foldlM (fun a b => f a b.1 b.2) init := Impl.Const.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} : + t.foldlM f init = (Const.toArray t).foldlM (fun a b => f a b.1 b.2) init := + Impl.Const.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} : t.foldl f init = (Const.toList t).foldl (fun a b => f a b.1 b.2) init := Impl.Const.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} : + t.foldl f init = (Const.toArray t).foldl (fun a b => f a b.1 b.2) init := + Impl.Const.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : t.foldrM f init = (Const.toList t).foldrM (fun a b => f a.1 a.2 b) init := Impl.Const.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : + t.foldrM f init = (Const.toArray t).foldrM (fun a b => f a.1 a.2 b) init := + Impl.Const.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} : t.foldr f init = (Const.toList t).foldr (fun a b => f a.1 a.2 b) init := Impl.Const.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} : + t.foldr f init = (Const.toArray t).foldr (fun a b => f a.1 a.2 b) init := + Impl.Const.foldr_eq_foldr_toArray + theorem forM_eq_forMUncurried [Monad m] [LawfulMonad m] {f : α → β → m PUnit} : t.forM f = forMUncurried (fun a => f a.1 a.2) t := rfl @@ -1326,6 +1524,10 @@ theorem forMUncurried_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → forMUncurried f t = (Const.toList t).forM f := Impl.Const.forM_eq_forM_toList +theorem forMUncurried_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} : + forMUncurried f t = (Const.toArray t).forM f := + Impl.Const.forM_eq_forM_toArray + theorem forIn_eq_forInUncurried [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : t.forIn f init = forInUncurried (fun a b => f a.1 a.2 b) init t := rfl @@ -1335,6 +1537,11 @@ theorem forInUncurried_eq_forIn_toList [Monad m] [LawfulMonad m] forInUncurried f init t = ForIn.forIn (Const.toList t) init f := Impl.Const.forIn_eq_forIn_toList +theorem forInUncurried_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α × β → δ → m (ForInStep δ)} {init : δ} : + forInUncurried f init t = ForIn.forIn (Const.toArray t) init f := + Impl.Const.forIn_eq_forIn_toArray + end Const end monadic @@ -4383,6 +4590,11 @@ theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) : t.minKey? = t.keys.head? := Impl.minKey?_eq_head?_keys h (instOrd := ⟨cmp⟩) +@[grind =_] +theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] (h : t.WF) : + t.minKey? = t.keysArray[0]? := + Impl.minKey?_eq_getElem?_keysArray h (instOrd := ⟨cmp⟩) + @[simp, grind =] theorem minKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) : (t.modify k f).minKey? = t.minKey? := @@ -4532,6 +4744,11 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) : t.minKey! = t.keys.head! := Impl.minKey!_eq_head!_keys h (instOrd := ⟨cmp⟩) +@[grind =_] +theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.minKey! = t.keysArray[0]! := + Impl.minKey!_eq_getElem!_keysArray h (instOrd := ⟨cmp⟩) + @[simp] theorem minKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} : (t.modify k f).minKey! = t.minKey! := @@ -4678,6 +4895,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] (h : t.WF) {fallback} : t.minKeyD fallback = t.keys.headD fallback := Impl.minKeyD_eq_headD_keys h (instOrd := ⟨cmp⟩) +theorem minKeyD_eq_getD_keysArray [TransCmp cmp] (h : t.WF) {fallback} : + t.minKeyD fallback = t.keysArray.getD 0 fallback := + Impl.minKeyD_eq_getD_keysArray h (instOrd := ⟨cmp⟩) + @[simp, grind =] theorem minKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} : (t.modify k f |>.minKeyD fallback) = t.minKeyD fallback := @@ -4885,6 +5106,11 @@ theorem maxKey?_eq_getLast?_keys [TransCmp cmp] (h : t.WF) : t.maxKey? = t.keys.getLast? := Impl.maxKey?_eq_getLast?_keys h (instOrd := ⟨cmp⟩) +@[grind =_] +theorem maxKey?_eq_back?_keysArray [TransCmp cmp] (h : t.WF) : + t.maxKey? = t.keysArray.back? := + Impl.maxKey?_eq_back?_keysArray h (instOrd := ⟨cmp⟩) + @[simp, grind =] theorem maxKey?_modify [TransCmp cmp] [LawfulEqCmp cmp] {k f} (h : t.WF) : (t.modify k f).maxKey? = t.maxKey? := @@ -5032,6 +5258,11 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) : t.maxKey! = t.keys.getLast! := Impl.maxKey!_eq_getLast!_keys h (instOrd := ⟨cmp⟩) +@[grind =_] +theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.maxKey! = t.keysArray.back! := + Impl.maxKey!_eq_back!_keysArray h (instOrd := ⟨cmp⟩) + @[simp, grind =] theorem maxKey!_modify [TransCmp cmp] [LawfulEqCmp cmp] [Inhabited α] (h : t.WF) {k f} : (t.modify k f).maxKey! = t.maxKey! := @@ -5180,6 +5411,11 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] (h : t.WF) {fallback} : t.maxKeyD fallback = t.keys.getLastD fallback := Impl.maxKeyD_eq_getLastD_keys h (instOrd := ⟨cmp⟩) +@[grind =_] +theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] (h : t.WF) {fallback} : + t.maxKeyD fallback = t.keysArray.back?.getD fallback := + Impl.maxKeyD_eq_getD_back?_keysArray h (instOrd := ⟨cmp⟩) + @[simp, grind =] theorem maxKeyD_modify [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k f fallback} : (t.modify k f |>.maxKeyD fallback) = t.maxKeyD fallback := @@ -5762,13 +5998,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff.trans Impl.equiv_iff_toList_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff.trans Impl.equiv_iff_toArray_perm + theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_toList_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_toArray_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff.trans (Impl.equiv_iff_toList_eq h₁.1 h₂.1) +theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff.trans (Impl.equiv_iff_toArray_eq h₁.1 h₂.1) + theorem insertMany_list_equiv_foldl {l : List ((a : α) × β a)} : t₁.insertMany l ~m l.foldl (init := t₁) fun acc p => acc.insert p.1 p.2 := by constructor @@ -5788,24 +6034,46 @@ variable {β : Type v} {t₁ t₂ : Raw α β cmp} theorem Const.equiv_iff_toList_perm : t₁ ~m t₂ ↔ (Const.toList t₁).Perm (Const.toList t₂) := equiv_iff.trans Impl.Const.equiv_iff_toList_perm +theorem Const.equiv_iff_toArray_perm : t₁ ~m t₂ ↔ (Const.toArray t₁).Perm (Const.toArray t₂) := + equiv_iff.trans Impl.Const.equiv_iff_toArray_perm + theorem Const.equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ Const.toList t₁ = Const.toList t₂ := equiv_iff.trans (Impl.Const.equiv_iff_toList_eq h₁.1 h₂.1) +theorem Const.equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ Const.toArray t₁ = Const.toArray t₂ := + equiv_iff.trans (Impl.Const.equiv_iff_toArray_eq h₁.1 h₂.1) + theorem Const.equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := equiv_iff.trans Impl.Const.equiv_iff_keys_perm +theorem Const.equiv_iff_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := + equiv_iff.trans Impl.Const.equiv_iff_keysArray_perm + theorem Const.equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.keys = t₂.keys := equiv_iff.trans (Impl.Const.equiv_iff_keys_eq h₁.1 h₂.1) +theorem Const.equiv_iff_keysArray_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := + equiv_iff.trans (Impl.Const.equiv_iff_keysArray_eq h₁.1 h₂.1) + theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) → t₁ ~m t₂ := Const.equiv_iff_toList_perm.mpr +theorem Equiv.of_constToArray_perm : (Const.toArray t₁).Perm (Const.toArray t₂) → t₁ ~m t₂ := + Const.equiv_iff_toArray_perm.mpr + theorem Equiv.of_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ := Const.equiv_iff_keys_unit_perm.mpr +theorem Equiv.of_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} : + t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ := + Const.equiv_iff_keysArray_unit_perm.mpr + theorem Const.insertMany_list_equiv_foldl {l : List (α × β)} : insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by constructor @@ -5841,6 +6109,11 @@ theorem toList_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) : t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := Impl.toList_filterMap! h +theorem toArray_filterMap {f : (a : α) → β a → Option (γ a)} (h : t.WF) : + (t.filterMap f).toArray = + t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩)) := + Impl.toArray_filterMap! h + @[grind =] theorem isEmpty_filterMap_iff [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} (h : t.WF) : @@ -6064,6 +6337,12 @@ theorem toList_filterMap (Const.toList t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := Impl.Const.toList_filterMap! h +theorem toArray_filterMap + {f : α → β → Option γ} (h : t.WF) : + Const.toArray (t.filterMap f) = + (Const.toArray t).filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := + Impl.Const.toArray_filterMap! h + @[grind =] theorem getKey?_filterMap [TransCmp cmp] {f : α → β → Option γ} {k : α} (h : t.WF) : @@ -6108,10 +6387,18 @@ theorem toList_filter {f : (a : α) → β a → Bool} (h : t.WF) : (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) := Impl.toList_filter! h +theorem toArray_filter {f : (a : α) → β a → Bool} (h : t.WF) : + (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) := + Impl.toArray_filter! h + theorem keys_filter_key {f : α → Bool} (h : t.WF) : (t.filter fun k _ => f k).keys = t.keys.filter f := Impl.keys_filter!_key h +theorem keysArray_filter_key {f : α → Bool} (h : t.WF) : + (t.filter fun k _ => f k).keysArray = t.keysArray.filter f := + Impl.keysArray_filter!_key h + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] [LawfulEqCmp cmp] {f : (a : α) → β a → Bool} (h : t.WF) : @@ -6381,6 +6668,11 @@ theorem toList_filter {f : α → β → Bool} (h : t.WF) : (Const.toList t).filter (fun p => f p.1 p.2) := Impl.Const.toList_filter! h +theorem toArray_filter {f : α → β → Bool} (h : t.WF) : + Const.toArray (t.filter f) = + (Const.toArray t).filter (fun p => f p.1 p.2) := + Impl.Const.toArray_filter! h + theorem keys_filter [TransCmp cmp] {f : α → β → Bool} (h : t.WF) : (t.filter f).keys = (t.keys.attach.filter (fun ⟨x, h'⟩ => f x (get t x (mem_of_mem_keys h h')))).unattach := @@ -6429,9 +6721,16 @@ theorem toList_map {f : (a : α) → β a → γ a} : (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) := Impl.toList_map +theorem toArray_map {f : (a : α) → β a → γ a} : + (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) := + Impl.toArray_map + theorem keys_map {f : (a : α) → β a → γ a} : (t.map f).keys = t.keys := Impl.keys_map +theorem keysArray_map {f : (a : α) → β a → γ a} : (t.map f).keysArray = t.keysArray := + Impl.keysArray_map + theorem filterMap_equiv_map [TransCmp cmp] {f : (a : α) → β a → γ a} (h : t.WF) : (t.filterMap (fun k v => some (f k v))) ~m t.map f := @@ -6598,6 +6897,11 @@ theorem toList_map {f : α → β → γ} : (Const.toList t).map (fun p => (p.1, f p.1 p.2)) := Impl.Const.toList_map +theorem toArray_map {f : α → β → γ} : + Const.toArray (t.map f) = + (Const.toArray t).map (fun p => (p.1, f p.1 p.2)) := + Impl.Const.toArray_map + end Const end map diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index aef9fa7f42..c95c5b0241 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -8,6 +8,7 @@ module prelude import Std.Data.DTreeMap.Lemmas public import Std.Data.TreeMap.AdditionalOperations +public import Init.Data.Array.Perm import Init.Data.List.Pairwise @[expose] public section @@ -297,10 +298,17 @@ theorem getElem?_congr [TransCmp cmp] {a b : α} (hab : cmp a b = .eq) : theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} : (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := DTreeMap.Const.toList_insert_perm +theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} {v : β} : + (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) := DTreeMap.Const.toArray_insert_perm + theorem keys_insertIfNew_perm {t : TreeMap α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} : (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) := DTreeMap.keys_insertIfNew_perm +theorem keysArray_insertIfNew_perm {t : TreeMap α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} : + (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) := + DTreeMap.keysArray_insertIfNew_perm + @[simp] theorem getElem_insert_self [TransCmp cmp] {k : α} {v : β} : (t.insert k v)[k]'mem_insert_self = v := @@ -804,24 +812,47 @@ theorem length_keys [TransCmp cmp] : t.keys.length = t.size := DTreeMap.length_keys +@[simp, grind =] +theorem size_keysArray [TransCmp cmp] : + t.keysArray.size = t.size := + DTreeMap.size_keysArray + @[simp, grind =] theorem isEmpty_keys : t.keys.isEmpty = t.isEmpty := DTreeMap.isEmpty_keys +@[simp, grind =] +theorem isEmpty_keysArray : + t.keysArray.isEmpty = t.isEmpty := + DTreeMap.isEmpty_keysArray + @[simp, grind =] theorem contains_keys [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : t.keys.contains k = t.contains k := DTreeMap.contains_keys +@[simp, grind =] +theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.keysArray.contains k = t.contains k := + DTreeMap.contains_keysArray + @[simp, grind =] theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : k ∈ t.keys ↔ k ∈ t := DTreeMap.mem_keys +@[simp, grind =] +theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.keysArray ↔ k ∈ t := + DTreeMap.mem_keysArray + theorem mem_of_mem_keys [TransCmp cmp] {k : α} (h : k ∈ t.keys) : k ∈ t := DTreeMap.mem_of_mem_keys h +theorem mem_of_mem_keysArray [TransCmp cmp] {k : α} (h : k ∈ t.keysArray) : k ∈ t := + DTreeMap.mem_of_mem_keysArray h + theorem distinct_keys [TransCmp cmp] : t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := DTreeMap.distinct_keys @@ -839,45 +870,89 @@ theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := DTreeMap.Const.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + (toArray t).map Prod.fst = t.keysArray := + DTreeMap.Const.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList : (toList t).length = t.size := DTreeMap.Const.length_toList +@[simp, grind =] +theorem size_toArray : + (toArray t).size = t.size := + DTreeMap.Const.size_toArray + @[simp, grind =] theorem isEmpty_toList : (toList t).isEmpty = t.isEmpty := DTreeMap.Const.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + (toArray t).isEmpty = t.isEmpty := + DTreeMap.Const.isEmpty_toArray + @[simp, grind =] 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, grind =] +theorem mem_toArray_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t[k]? = some v := + DTreeMap.Const.mem_toArray_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 +@[simp] +theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ t[k]? = some v := + DTreeMap.Const.mem_toArray_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 getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] {k : α} {v : β} : + t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t := + DTreeMap.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray + 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?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] {k k' : α} + {v : β} : + t.toArray.find? (cmp ·.1 k == .eq) = some (k', v) ↔ + t.getKey? k = some k' ∧ t[k]? = some v := + DTreeMap.Const.find?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + DTreeMap.Const.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + DTreeMap.Const.find?_toArray_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 @@ -894,18 +969,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := DTreeMap.Const.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := + DTreeMap.Const.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} : t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := DTreeMap.Const.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} : + t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := + DTreeMap.Const.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := DTreeMap.Const.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := + DTreeMap.Const.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := DTreeMap.Const.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := + DTreeMap.Const.foldr_eq_foldr_toArray + @[simp, grind =] theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → β → m PUnit} : t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl @@ -914,6 +1005,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → m PUnit} ForM.forM t f = ForM.forM t.toList f := DTreeMap.Const.forMUncurried_eq_forM_toList (f := f) +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} : + ForM.forM t f = ForM.forM t.toArray f := + DTreeMap.Const.forMUncurried_eq_forM_toArray (f := f) + @[simp, grind =] theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : @@ -924,30 +1019,60 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] ForIn.forIn t init f = ForIn.forIn t.toList init f := DTreeMap.Const.forInUncurried_eq_forIn_toList +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α × β → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := + DTreeMap.Const.forInUncurried_eq_forIn_toArray + theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := DTreeMap.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := + DTreeMap.foldlM_eq_foldlM_keysArray + theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} : t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := DTreeMap.foldl_eq_foldl_keys +theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} : + t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := + DTreeMap.foldl_eq_foldl_keysArray + theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := DTreeMap.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] + {f : α → δ → m δ} {init : δ} : + t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := + DTreeMap.foldrM_eq_foldrM_keysArray + theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} : t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := DTreeMap.foldr_eq_foldr_keys +theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} : + t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := + DTreeMap.foldr_eq_foldr_keysArray + theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t (fun a => f a.1) = t.keys.forM f := DTreeMap.forM_eq_forM_keys +theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t (fun a => f a.1) = t.keysArray.forM f := + DTreeMap.forM_eq_forM_keysArray + theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f := DTreeMap.forIn_eq_forIn_keys +theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f := + DTreeMap.forIn_eq_forIn_keysArray + end monadic @[simp, grind =] @@ -2901,6 +3026,10 @@ theorem minKey?_insertIfNew_le_self [TransCmp cmp] {k v kmi} : t.minKey? = t.keys.head? := DTreeMap.minKey?_eq_head?_keys +@[grind =_] theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] : + t.minKey? = t.keysArray[0]? := + DTreeMap.minKey?_eq_getElem?_keysArray + 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 @@ -3049,6 +3178,10 @@ theorem minKey_insertIfNew_le_self [TransCmp cmp] {k v} : t.minKey he = t.keys.head (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := DTreeMap.minKey_eq_head_keys +theorem minKey_eq_getElem_keysArray [TransCmp cmp] {he} : + t.minKey he = t.keysArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) := + DTreeMap.minKey_eq_getElem_keysArray + 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 @@ -3184,6 +3317,10 @@ theorem minKey!_eq_head!_keys [TransCmp cmp] [Inhabited α] : t.minKey! = t.keys.head! := DTreeMap.minKey!_eq_head!_keys +theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] : + t.minKey! = t.keysArray[0]! := + DTreeMap.minKey!_eq_getElem!_keysArray + 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! := @@ -3311,6 +3448,10 @@ theorem minKeyD_eq_headD_keys [TransCmp cmp] {fallback} : t.minKeyD fallback = t.keys.headD fallback := DTreeMap.minKeyD_eq_headD_keys +theorem minKeyD_eq_getD_keysArray [TransCmp cmp] {fallback} : + t.minKeyD fallback = t.keysArray.getD 0 fallback := + DTreeMap.minKeyD_eq_getD_keysArray + theorem minKeyD_modify [TransCmp cmp] {k f} (he : (modify t k f).isEmpty = false) {fallback} : (modify t k f |>.minKeyD fallback) = @@ -3494,6 +3635,10 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] {k v kmi} : t.maxKey? = t.keys.getLast? := DTreeMap.maxKey?_eq_getLast?_keys +@[grind =_] theorem maxKey?_eq_back?_keysArray [TransCmp cmp] : + t.maxKey? = t.keysArray.back? := + DTreeMap.maxKey?_eq_back?_keysArray + @[grind =] theorem maxKey?_modify [TransCmp cmp] {k f} : (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := DTreeMap.Const.maxKey?_modify @@ -3630,6 +3775,10 @@ theorem self_le_maxKey_insertIfNew [TransCmp cmp] {k v} : t.maxKey he = t.keys.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_keys ▸ he) := DTreeMap.maxKey_eq_getLast_keys +@[grind =_] theorem maxKey_eq_back_keysArray [TransCmp cmp] {he} : + t.maxKey he = t.keysArray.back (Nat.zero_lt_of_ne_zero (by simpa [size_keysArray, isEmpty_eq_size_eq_zero, - Array.size_eq_zero_iff] using he)) := + DTreeMap.maxKey_eq_back_keysArray + theorem maxKey_modify [TransCmp cmp] {k f he} : (modify t k f).maxKey he = if cmp (t.maxKey <| cast (congrArg (· = false) isEmpty_modify) he) k = .eq then @@ -3765,6 +3914,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] : t.maxKey! = t.keys.getLast! := DTreeMap.maxKey!_eq_getLast!_keys +theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] : + t.maxKey! = t.keysArray.back! := + DTreeMap.maxKey!_eq_back!_keysArray + theorem maxKey!_modify [TransCmp cmp] [Inhabited α] {k f} (he : (modify t k f).isEmpty = false) : (modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! := @@ -3892,6 +4045,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] {fallback} : t.maxKeyD fallback = t.keys.getLastD fallback := DTreeMap.maxKeyD_eq_getLastD_keys +theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] {fallback} : + t.maxKeyD fallback = t.keysArray.back?.getD fallback := + DTreeMap.maxKeyD_eq_getD_back?_keysArray + theorem maxKeyD_modify [TransCmp cmp] {k f} (he : (modify t k f).isEmpty = false) {fallback} : (modify t k f |>.maxKeyD fallback) = @@ -4342,24 +4499,46 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toList_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toArray_perm + theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_constToList_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_constToArray_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toList_eq +theorem equiv_iff_toArray_eq [TransCmp cmp] : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_toArray_eq + theorem equiv_iff_keys_unit_perm {t₁ t₂ : TreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keys_unit_perm +theorem equiv_iff_keysArray_unit_perm {t₁ t₂ : TreeMap α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := + equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keysArray_unit_perm + theorem equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys = t₂.keys := equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keys_unit_eq +theorem equiv_iff_keysArray_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := + equiv_iff_equiv.trans DTreeMap.Const.equiv_iff_keysArray_unit_eq + theorem Equiv.of_keys_unit_perm {t₁ t₂ : TreeMap α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ := equiv_iff_keys_unit_perm.mpr +theorem Equiv.of_keysArray_unit_perm {t₁ t₂ : TreeMap α Unit cmp} : + t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ := + equiv_iff_keysArray_unit_perm.mpr + theorem insertMany_list_equiv_foldl {l : List (α × β)} : insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by constructor @@ -4394,6 +4573,12 @@ theorem toList_filterMap {f : (a : α) → β → Option γ} : t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := DTreeMap.Const.toList_filterMap +@[simp, grind =] +theorem toArray_filterMap {f : α → β → Option γ} : + (t.filterMap f).toArray = + t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => (p.1, x))) := + DTreeMap.Const.toArray_filterMap + @[grind =] theorem isEmpty_filterMap_iff [TransCmp cmp] {f : α → β → Option γ} : @@ -4561,10 +4746,19 @@ theorem toList_filter {f : α → β → Bool} : (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) := DTreeMap.Const.toList_filter +@[simp, grind =] +theorem toArray_filter {f : α → β → Bool} : + (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) := + DTreeMap.Const.toArray_filter + theorem keys_filter_key {f : α → Bool} : (t.filter fun k _ => f k).keys = t.keys.filter f := DTreeMap.keys_filter_key +theorem keysArray_filter_key {f : α → Bool} : + (t.filter fun k _ => f k).keysArray = t.keysArray.filter f := + DTreeMap.keysArray_filter_key + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] {f : α → β → Bool} : @@ -4748,10 +4942,19 @@ theorem toList_map {f : α → β → γ} : (t.map f).toList = t.toList.map (fun p => (p.1, f p.1 p.2)) := DTreeMap.Const.toList_map +@[simp, grind =] +theorem toArray_map {f : α → β → γ} : + (t.map f).toArray = t.toArray.map (fun p => (p.1, f p.1 p.2)) := + DTreeMap.Const.toArray_map + @[simp, grind =] theorem keys_map {f : α → β → γ} : (t.map f).keys = t.keys := DTreeMap.keys_map +@[simp, grind =] +theorem keysArray_map {f : α → β → γ} : (t.map f).keysArray = t.keysArray := + DTreeMap.keysArray_map + theorem filterMap_equiv_map [TransCmp cmp] {f : α → β → γ} : (t.filterMap (fun k v => some (f k v))) ~m t.map f := @@ -4891,4 +5094,16 @@ theorem getKeyD_map [TransCmp cmp] end map +theorem toArray_toList : t.toList.toArray = t.toArray := + DTreeMap.Const.toArray_toList + +theorem toList_toArray : t.toArray.toList = t.toList := + DTreeMap.Const.toList_toArray + +theorem toArray_keys : t.keys.toArray = t.keysArray := + DTreeMap.toArray_keys + +theorem toList_keysArray : t.keysArray.toList = t.keys := + DTreeMap.toList_keysArray + end Std.TreeMap diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index 7525446ff1..bc493d5554 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -8,6 +8,7 @@ module prelude import Std.Data.DTreeMap.Raw.Lemmas public import Std.Data.TreeMap.Raw.AdditionalOperations +public import Init.Data.Array.Perm import Init.Data.List.Find import Init.Data.List.Impl import Init.Data.List.Pairwise @@ -293,10 +294,18 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) (t.insert k v).toList.Perm (⟨k, v⟩ :: t.toList.filter (¬k == ·.1)) := DTreeMap.Raw.Const.toList_insert_perm h +theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (t.insert k v).toArray.Perm ((t.toArray.filter (¬k == ·.1)).push ⟨k, v⟩) := + DTreeMap.Raw.Const.toArray_insert_perm h + theorem keys_insertIfNew_perm {t : Raw α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} : (t.insertIfNew k ()).keys.Perm (if k ∈ t then t.keys else k :: t.keys) := DTreeMap.Raw.keys_insertIfNew_perm h +theorem keysArray_insertIfNew_perm {t : Raw α Unit cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} : + (t.insertIfNew k ()).keysArray.Perm (if k ∈ t then t.keysArray else t.keysArray.push k) := + DTreeMap.Raw.keysArray_insertIfNew_perm h + @[simp] theorem getElem_insert_self [TransCmp cmp] (h : t.WF) {k : α} {v : β} : (t.insert k v)[k]'(mem_insert_self h) = v := @@ -806,25 +815,49 @@ theorem length_keys [TransCmp cmp] (h : t.WF) : t.keys.length = t.size := DTreeMap.Raw.length_keys h +@[simp, grind =] +theorem size_keysArray [TransCmp cmp] (h : t.WF) : + t.keysArray.size = t.size := + DTreeMap.Raw.size_keysArray h + @[simp, grind =] theorem isEmpty_keys : t.keys.isEmpty = t.isEmpty := DTreeMap.Raw.isEmpty_keys +@[simp, grind =] +theorem isEmpty_keysArray : + t.keysArray.isEmpty = t.isEmpty := + DTreeMap.Raw.isEmpty_keysArray + @[simp, grind =] 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, grind =] +theorem contains_keysArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + t.keysArray.contains k = t.contains k := + DTreeMap.Raw.contains_keysArray h + @[simp, grind =] theorem mem_keys [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.keys ↔ k ∈ t := DTreeMap.Raw.mem_keys h +@[simp, grind =] +theorem mem_keysArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.keysArray ↔ k ∈ t := + DTreeMap.Raw.mem_keysArray h + theorem mem_of_mem_keys [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.keys → k ∈ t := DTreeMap.Raw.mem_of_mem_keys h +theorem mem_of_mem_keysArray [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.keysArray → k ∈ t := + DTreeMap.Raw.mem_of_mem_keysArray h + theorem distinct_keys [TransCmp cmp] (h : t.WF) : t.keys.Pairwise (fun a b => ¬ cmp a b = .eq) := DTreeMap.Raw.distinct_keys h @@ -842,46 +875,91 @@ theorem map_fst_toList_eq_keys : (toList t).map Prod.fst = t.keys := DTreeMap.Raw.Const.map_fst_toList_eq_keys +@[simp, grind _=_] +theorem map_fst_toArray_eq_keysArray : + (toArray t).map Prod.fst = t.keysArray := + DTreeMap.Raw.Const.map_fst_toArray_eq_keysArray + @[simp, grind =] theorem length_toList (h : t.WF) : (toList t).length = t.size := DTreeMap.Raw.Const.length_toList h +@[simp, grind =] +theorem size_toArray (h : t.WF) : + (toArray t).size = t.size := + DTreeMap.Raw.Const.size_toArray h + @[simp, grind =] theorem isEmpty_toList : (toList t).isEmpty = t.isEmpty := DTreeMap.Raw.Const.isEmpty_toList +@[simp, grind =] +theorem isEmpty_toArray : + (toArray t).isEmpty = t.isEmpty := + DTreeMap.Raw.Const.isEmpty_toArray + @[simp, grind =] 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, grind =] +theorem mem_toArray_iff_getElem?_eq_some [TransCmp cmp] [LawfulEqCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t[k]? = some v := + DTreeMap.Raw.Const.mem_toArray_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 +@[simp] +theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) {k : α} {v : β} : + (k, v) ∈ toArray t ↔ t.getKey? k = some k ∧ t[k]? = some v := + DTreeMap.Raw.Const.mem_toArray_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 getElem?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray [TransCmp cmp] (h : t.WF) {k : α} + {v : β} : + t[k]? = some v ↔ ∃ (k' : α), cmp k k' = .eq ∧ (k', v) ∈ toArray t := + DTreeMap.Raw.Const.get?_eq_some_iff_exists_compare_eq_eq_and_mem_toArray 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?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some [TransCmp cmp] (h : t.WF) + {k k' : α} {v : β} : + t.toArray.find? (cmp ·.1 k == .eq) = some ⟨k', v⟩ ↔ + t.getKey? k = some k' ∧ t[k]? = some v := + DTreeMap.Raw.Const.find?_toArray_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 +theorem find?_toArray_eq_none_iff_contains_eq_false [TransCmp cmp] (h : t.WF) {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ t.contains k = false := + DTreeMap.Raw.Const.find?_toArray_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 +@[simp] +theorem find?_toArray_eq_none_iff_not_mem [TransCmp cmp] (h : t.WF) {k : α} : + (toArray t).find? (cmp ·.1 k == .eq) = none ↔ ¬ k ∈ t := + DTreeMap.Raw.Const.find?_toArray_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 @@ -898,18 +976,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → β t.foldlM f init = t.toList.foldlM (fun a b => f a b.1 b.2) init := DTreeMap.Raw.Const.foldlM_eq_foldlM_toList +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM (fun a b => f a b.1 b.2) init := + DTreeMap.Raw.Const.foldlM_eq_foldlM_toArray + theorem foldl_eq_foldl_toList {f : δ → α → β → δ} {init : δ} : t.foldl f init = t.toList.foldl (fun a b => f a b.1 b.2) init := DTreeMap.Raw.Const.foldl_eq_foldl_toList +theorem foldl_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} : + t.foldl f init = t.toArray.foldl (fun a b => f a b.1 b.2) init := + DTreeMap.Raw.Const.foldl_eq_foldl_toArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM (fun a b => f a.1 a.2 b) init := DTreeMap.Raw.Const.foldrM_eq_foldrM_toList +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM (fun a b => f a.1 a.2 b) init := + DTreeMap.Raw.Const.foldrM_eq_foldrM_toArray + theorem foldr_eq_foldr_toList {f : α → β → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr (fun a b => f a.1 a.2 b) init := DTreeMap.Raw.Const.foldr_eq_foldr_toList +theorem foldr_eq_foldr_toArray {f : α → β → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr (fun a b => f a.1 a.2 b) init := + DTreeMap.Raw.Const.foldr_eq_foldr_toArray + @[simp, grind =] theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → β → m PUnit} : t.forM f = ForM.forM t (fun a => f a.1 a.2) := rfl @@ -918,6 +1012,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α × β → m PUnit} ForM.forM t f = t.toList.forM f := DTreeMap.Raw.Const.forMUncurried_eq_forM_toList (f := f) +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α × β → m PUnit} : + ForM.forM t f = t.toArray.forM f := + DTreeMap.Raw.Const.forMUncurried_eq_forM_toArray (f := f) + @[simp, grind =] theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : α → β → δ → m (ForInStep δ)} {init : δ} : t.forIn f init = ForIn.forIn t init (fun a d => f a.1 a.2 d) := rfl @@ -927,31 +1025,61 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] ForIn.forIn t init f = ForIn.forIn t.toList init f := DTreeMap.Raw.Const.forInUncurried_eq_forIn_toList +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α × β → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := + DTreeMap.Raw.Const.forInUncurried_eq_forIn_toArray + theorem foldlM_eq_foldlM_keys [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : t.foldlM (fun d a _ => f d a) init = t.keys.foldlM f init := DTreeMap.Raw.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_keysArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM (fun d a _ => f d a) init = t.keysArray.foldlM f init := + DTreeMap.Raw.foldlM_eq_foldlM_keysArray + theorem foldl_eq_foldl_keys {f : δ → α → δ} {init : δ} : t.foldl (fun d a _ => f d a) init = t.keys.foldl f init := DTreeMap.Raw.foldl_eq_foldl_keys +theorem foldl_eq_foldl_keysArray {f : δ → α → δ} {init : δ} : + t.foldl (fun d a _ => f d a) init = t.keysArray.foldl f init := + DTreeMap.Raw.foldl_eq_foldl_keysArray + theorem foldrM_eq_foldrM_keys [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM (fun a _ d => f a d) init = t.keys.foldrM f init := DTreeMap.Raw.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_keysArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : + t.foldrM (fun a _ d => f a d) init = t.keysArray.foldrM f init := + DTreeMap.Raw.foldrM_eq_foldrM_keysArray + theorem foldr_eq_foldr_keys {f : α → δ → δ} {init : δ} : t.foldr (fun a _ d => f a d) init = t.keys.foldr f init := DTreeMap.Raw.foldr_eq_foldr_keys +theorem foldr_eq_foldr_keysArray {f : α → δ → δ} {init : δ} : + t.foldr (fun a _ d => f a d) init = t.keysArray.foldr f init := + DTreeMap.Raw.foldr_eq_foldr_keysArray + theorem forM_eq_forM_keys [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t (fun a => f a.1) = t.keys.forM f := DTreeMap.Raw.forM_eq_forM_keys +theorem forM_eq_forM_keysArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t (fun a => f a.1) = t.keysArray.forM f := + DTreeMap.Raw.forM_eq_forM_keysArray + theorem forIn_eq_forIn_keys [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keys init f := DTreeMap.Raw.forIn_eq_forIn_keys +theorem forIn_eq_forIn_keysArray [Monad m] [LawfulMonad m] + {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init (fun a d => f a.1 d) = ForIn.forIn t.keysArray init f := + DTreeMap.Raw.forIn_eq_forIn_keysArray + end monadic @[simp, grind =] @@ -2961,6 +3089,10 @@ theorem minKey?_eq_head?_keys [TransCmp cmp] (h : t.WF) : t.minKey? = t.keys.head? := DTreeMap.Raw.minKey?_eq_head?_keys h +theorem minKey?_eq_getElem?_keysArray [TransCmp cmp] (h : t.WF) : + t.minKey? = t.keysArray[0]? := + DTreeMap.Raw.minKey?_eq_getElem?_keysArray h + @[grind =] 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 := @@ -3102,6 +3234,10 @@ theorem minKey!_insertIfNew_le_self [TransCmp cmp] [Inhabited α] (h : t.WF) {k t.minKey! = t.keys.head! := DTreeMap.Raw.minKey!_eq_head!_keys h +theorem minKey!_eq_getElem!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.minKey! = t.keysArray[0]! := + DTreeMap.Raw.minKey!_eq_getElem!_keysArray 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! := @@ -3229,6 +3365,10 @@ 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_eq_getD_keysArray [TransCmp cmp] (h : t.WF) {fallback} : + t.minKeyD fallback = t.keysArray.getD 0 fallback := + DTreeMap.Raw.minKeyD_eq_getD_keysArray 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) = @@ -3414,6 +3554,11 @@ theorem self_le_maxKey?_insertIfNew [TransCmp cmp] (h : t.WF) {k v kmi} : t.maxKey? = t.keys.getLast? := DTreeMap.Raw.maxKey?_eq_getLast?_keys h +@[grind =_] +theorem maxKey?_eq_back?_keysArray [TransCmp cmp] (h : t.WF) : + t.maxKey? = t.keysArray.back? := + DTreeMap.Raw.maxKey?_eq_back?_keysArray h + theorem maxKey?_modify [TransCmp cmp] (h : t.WF) {k f} : (t.modify k f).maxKey? = t.maxKey?.map fun km => if cmp km k = .eq then k else km := DTreeMap.Raw.Const.maxKey?_modify h @@ -3542,6 +3687,10 @@ theorem maxKey!_eq_getLast!_keys [TransCmp cmp] [Inhabited α] (h : t.WF) : t.maxKey! = t.keys.getLast! := DTreeMap.Raw.maxKey!_eq_getLast!_keys h +theorem maxKey!_eq_back!_keysArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.maxKey! = t.keysArray.back! := + DTreeMap.Raw.maxKey!_eq_back!_keysArray h + theorem maxKey!_modify [TransCmp cmp] [Inhabited α] (h : t.WF) {k f} (he : (modify t k f).isEmpty = false) : (modify t k f).maxKey! = if cmp t.maxKey! k = .eq then k else t.maxKey! := @@ -3669,6 +3818,10 @@ theorem maxKeyD_eq_getLastD_keys [TransCmp cmp] (h : t.WF) {fallback} : t.maxKeyD fallback = t.keys.getLastD fallback := DTreeMap.Raw.maxKeyD_eq_getLastD_keys h +theorem maxKeyD_eq_getD_back?_keysArray [TransCmp cmp] (h : t.WF) {fallback} : + t.maxKeyD fallback = t.keysArray.back?.getD fallback := + DTreeMap.Raw.maxKeyD_eq_getD_back?_keysArray h + theorem maxKeyD_modify [TransCmp cmp] (h : t.WF) {k f} (he : (modify t k f).isEmpty = false) {fallback} : (modify t k f |>.maxKeyD fallback) = @@ -4087,24 +4240,46 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toList_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_toArray_perm + theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_constToList_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_constToArray_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toList_eq h₁.1 h₂.1) +theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_toArray_eq h₁.1 h₂.1) + theorem equiv_iff_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁ ~m t₂ ↔ t₁.keys.Perm t₂.keys := equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_keys_unit_perm +theorem equiv_iff_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} : + t₁ ~m t₂ ↔ t₁.keysArray.Perm t₂.keysArray := + equiv_iff.trans DTreeMap.Raw.Const.equiv_iff_keysArray_unit_perm + theorem equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.keys = t₂.keys := equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_keys_unit_eq h₁.1 h₂.1) +theorem equiv_iff_keysArray_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.keysArray = t₂.keysArray := + equiv_iff.trans (DTreeMap.Raw.Const.equiv_iff_keysArray_unit_eq h₁.1 h₂.1) + theorem Equiv.of_keys_unit_perm {t₁ t₂ : Raw α Unit cmp} : t₁.keys.Perm t₂.keys → t₁ ~m t₂ := equiv_iff_keys_unit_perm.mpr +theorem Equiv.of_keysArray_unit_perm {t₁ t₂ : Raw α Unit cmp} : + t₁.keysArray.Perm t₂.keysArray → t₁ ~m t₂ := + equiv_iff_keysArray_unit_perm.mpr + theorem insertMany_list_equiv_foldl {l : List (α × β)} : insertMany t₁ l ~m l.foldl (init := t₁) (fun acc p => acc.insert p.1 p.2) := by constructor @@ -4136,6 +4311,11 @@ theorem toList_filterMap {f : α → β → Option γ} (h : t.WF) : (t.toList.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) := DTreeMap.Raw.Const.toList_filterMap h +theorem toArray_filterMap {f : α → β → Option γ} (h : t.WF) : + (t.filterMap f).toArray = + (t.toArray.filterMap (fun p => (f p.1 p.2).map (fun x => ⟨p.1, x⟩))) := + DTreeMap.Raw.Const.toArray_filterMap h + @[grind =] theorem isEmpty_filterMap_iff [TransCmp cmp] {f : α → β → Option γ} (h : t.WF) : @@ -4303,10 +4483,19 @@ theorem toList_filter (t.filter f).toList = t.toList.filter (fun p => f p.1 p.2) := DTreeMap.Raw.Const.toList_filter h.out +theorem toArray_filter + {f : (a : α) → β → Bool} (h : t.WF) : + (t.filter f).toArray = t.toArray.filter (fun p => f p.1 p.2) := + DTreeMap.Raw.Const.toArray_filter h.out + theorem keys_filter_key {f : α → Bool} (h : t.WF) : (t.filter fun k _ => f k).keys = t.keys.filter f := DTreeMap.Raw.keys_filter_key h.out +theorem keysArray_filter_key {f : α → Bool} (h : t.WF) : + (t.filter fun k _ => f k).keysArray = t.keysArray.filter f := + DTreeMap.Raw.keysArray_filter_key h.out + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] {f : α → β → Bool} (h : t.WF) : @@ -4485,9 +4674,16 @@ theorem toList_map {f : (a : α) → β → γ} : (t.map f).toList = t.toList.map (fun p => ⟨p.1, f p.1 p.2⟩) := DTreeMap.Raw.Const.toList_map +theorem toArray_map {f : (a : α) → β → γ} : + (t.map f).toArray = t.toArray.map (fun p => ⟨p.1, f p.1 p.2⟩) := + DTreeMap.Raw.Const.toArray_map + theorem keys_map {f : α → β → γ} : (t.map f).keys = t.keys := DTreeMap.Raw.keys_map +theorem keysArray_map {f : α → β → γ} : (t.map f).keysArray = t.keysArray := + DTreeMap.Raw.keysArray_map + theorem filterMap_equiv_map [TransCmp cmp] {f : α → β → γ} (h : t.WF) : (t.filterMap (fun k v => Option.some (f k v))) ~m (t.map f) := @@ -4626,4 +4822,16 @@ theorem getD_map_of_getKey?_eq_some [TransCmp cmp] end map +theorem toArray_toList : t.toList.toArray = t.toArray := + DTreeMap.Raw.Const.toArray_toList + +theorem toList_toArray : t.toArray.toList = t.toList := + DTreeMap.Raw.Const.toList_toArray + +theorem toArray_keys : t.keys.toArray = t.keysArray := + DTreeMap.Raw.toArray_keys + +theorem toList_keysArray : t.keysArray.toList = t.keys := + DTreeMap.Raw.toList_keysArray + end Std.TreeMap.Raw diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 78fc76700e..2fdb9e7ccd 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -8,6 +8,7 @@ module prelude import Std.Data.TreeMap.Lemmas import Std.Data.DTreeMap.Lemmas +public import Init.Data.Array.Perm public import Std.Data.TreeSet.AdditionalOperations @[expose] public section @@ -91,6 +92,12 @@ theorem isEmpty_iff_forall_not_mem [TransCmp cmp] : t.isEmpty = true ↔ ∀ a, ¬a ∈ t := TreeMap.isEmpty_iff_forall_not_mem +theorem toArray_toList : t.toList.toArray = t.toArray := + TreeMap.toArray_keys + +theorem toList_toArray : t.toArray.toList = t.toList := + TreeMap.toList_keysArray + @[simp] theorem insert_eq_insert {p : α} : Insert.insert p t = t.insert p := rfl @@ -286,6 +293,10 @@ theorem toList_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} : (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList) := DTreeMap.keys_insertIfNew_perm +theorem toArray_insert_perm [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] {k : α} : + (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k) := + DTreeMap.keysArray_insertIfNew_perm + @[simp, grind =] theorem get_erase [TransCmp cmp] {k a : α} {h'} : (t.erase k).get a h' = t.get a (mem_of_mem_erase h') := TreeMap.getKey_erase @@ -453,25 +464,49 @@ theorem length_toList [TransCmp cmp] : t.toList.length = t.size := TreeMap.length_keys +@[simp, grind =] +theorem size_toArray [TransCmp cmp] : + t.toArray.size = t.size := by + simp [← toArray_toList, length_toList] + @[simp, grind =] theorem isEmpty_toList : t.toList.isEmpty = t.isEmpty := TreeMap.isEmpty_keys +@[simp, grind =] +theorem isEmpty_toArray : + t.toArray.isEmpty = t.isEmpty := by + simp [← toArray_toList, isEmpty_toList] + @[simp, grind =] theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : t.toList.contains k = t.contains k := TreeMap.contains_keys +@[simp, grind =] +theorem contains_toArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] {k : α} : + t.toArray.contains k = t.contains k := by + simp [← toArray_toList, contains_toList] + @[simp, grind =] theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : k ∈ t.toList ↔ k ∈ t := TreeMap.mem_keys +@[simp, grind =] +theorem mem_toArray [LawfulEqCmp cmp] [TransCmp cmp] {k : α} : + k ∈ t.toArray ↔ k ∈ t := + TreeMap.mem_keysArray + theorem mem_of_mem_toList [TransCmp cmp] {k : α} : k ∈ t.toList → k ∈ t := TreeMap.mem_of_mem_keys +theorem mem_of_mem_toArray [TransCmp cmp] {k : α} : + k ∈ t.toArray → k ∈ t := by + simpa [← toArray_toList] using mem_of_mem_toList + theorem distinct_toList [TransCmp cmp] : t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) := TreeMap.distinct_keys @@ -948,18 +983,34 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] {f : δ → α → m t.foldlM f init = t.toList.foldlM f init := TreeMap.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM f init := by + simp [foldlM_eq_foldlM_toList, ← toArray_toList] + theorem foldl_eq_foldl_toList {f : δ → α → δ} {init : δ} : t.foldl f init = t.toList.foldl f init := TreeMap.foldl_eq_foldl_keys +theorem foldl_eq_foldl_toArray {f : δ → α → δ} {init : δ} : + t.foldl f init = t.toArray.foldl f init := by + simp [foldl_eq_foldl_toList, ← toArray_toList] + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM f init := TreeMap.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM f init := by + simp [foldrM_eq_foldrM_toList, ← toArray_toList] + theorem foldr_eq_foldr_toList {f : α → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr f init := TreeMap.foldr_eq_foldr_keys +theorem foldr_eq_foldr_toArray {f : α → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr f init := by + simp [foldr_eq_foldr_toList, ← toArray_toList] + @[simp, grind =] theorem forM_eq_forM [Monad m] [LawfulMonad m] {f : α → m PUnit} : t.forM f = ForM.forM t f := rfl @@ -968,6 +1019,10 @@ theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t f = t.toList.forM f := TreeMap.forM_eq_forM_keys +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t f = t.toArray.forM f := + TreeMap.forM_eq_forM_keysArray + @[simp, grind =] theorem forIn_eq_forIn [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : t.forIn f init = ForIn.forIn t init f := rfl @@ -976,6 +1031,10 @@ theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : α → δ → m (Fo ForIn.forIn t init f = ForIn.forIn t.toList init f := TreeMap.forIn_eq_forIn_keys +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := by + simp [forIn_eq_forIn_toList, ← toArray_toList] + end monadic @[simp, grind =] @@ -1361,6 +1420,10 @@ theorem min?_le_min?_erase [TransCmp cmp] {k km kme} : t.min? = t.toList.head? := TreeMap.minKey?_eq_head?_keys +@[grind =_] theorem min?_eq_getElem?_toArray [TransCmp cmp] : + t.min? = t.toArray[0]? := + TreeMap.minKey?_eq_getElem?_keysArray + theorem min_eq_get_min? [TransCmp cmp] {he} : t.min he = t.min?.get (isSome_min?_iff_isEmpty_eq_false.mpr he) := TreeMap.minKey_eq_get_minKey? @@ -1455,6 +1518,10 @@ theorem min_eq_head_toList [TransCmp cmp] {he} : t.min he = t.toList.head (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) := TreeMap.minKey_eq_head_keys +theorem min_eq_getElem_toArray [TransCmp cmp] {he} : + t.min he = t.toArray[0]'(Nat.zero_lt_of_ne_zero (by simpa [isEmpty_eq_size_eq_zero] using he)) := + TreeMap.minKey_eq_getElem_keysArray + theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) : t.min? = some t.min! := TreeMap.minKey?_eq_some_minKey! he @@ -1547,6 +1614,10 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] : t.min! = t.toList.head! := TreeMap.minKey!_eq_head!_keys +theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] : + t.min! = t.toArray[0]! := + TreeMap.minKey!_eq_getElem!_keysArray + theorem min?_eq_some_minD [TransCmp cmp] (he : t.isEmpty = false) {fallback} : t.min? = some (t.minD fallback) := TreeMap.minKey?_eq_some_minKeyD he @@ -1635,6 +1706,10 @@ theorem minD_eq_headD_toList [TransCmp cmp] {fallback} : t.minD fallback = t.toList.headD fallback := TreeMap.minKeyD_eq_headD_keys +theorem minD_eq_getD_toArray [TransCmp cmp] {fallback} : + t.minD fallback = t.toArray.getD 0 fallback := + TreeMap.minKeyD_eq_getD_keysArray + end Min section Max @@ -1769,6 +1844,10 @@ theorem max?_eq_getLast?_toList [TransCmp cmp] : t.max? = t.toList.getLast? := TreeMap.maxKey?_eq_getLast?_keys +theorem max?_eq_back?_toArray [TransCmp cmp] : + t.max? = t.toArray.back? := by + rw [max?_eq_getLast?_toList, ← Array.getLast?_toList, toList_toArray] + theorem max_eq_get_max? [TransCmp cmp] {he} : t.max he = t.max?.get (isSome_max?_iff_isEmpty_eq_false.mpr he) := TreeMap.maxKey_eq_get_maxKey? @@ -1864,6 +1943,11 @@ theorem max_eq_getLast_toList [TransCmp cmp] {he} : t.max he = t.toList.getLast (List.isEmpty_eq_false_iff.mp <| isEmpty_toList ▸ he) := TreeMap.maxKey_eq_getLast_keys +@[grind =_] +theorem max_eq_back_toArray [TransCmp cmp] {he} : + t.max he = t.toArray.back (Nat.zero_lt_of_ne_zero (by simpa [isEmpty_eq_size_eq_zero] using he)) := by + exact TreeMap.maxKey_eq_back_keysArray + theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (he : t.isEmpty = false) : t.max? = some t.max! := TreeMap.maxKey?_eq_some_maxKey! he @@ -1957,6 +2041,11 @@ theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] : t.max! = t.toList.getLast! := TreeMap.maxKey!_eq_getLast!_keys +@[grind =_] +theorem max!_eq_back!_toArray [TransCmp cmp] [Inhabited α] : + t.max! = t.toArray.back! := by + rw [max!_eq_getLast!_toList, ← Array.getLast!_toList, toList_toArray] + theorem max?_eq_some_maxD [TransCmp cmp] (he : t.isEmpty = false) {fallback} : t.max? = some (t.maxD fallback) := TreeMap.maxKey?_eq_some_maxKeyD he @@ -2045,6 +2134,10 @@ theorem maxD_eq_getLastD_toList [TransCmp cmp] {fallback} : t.maxD fallback = t.toList.getLastD fallback := TreeMap.maxKeyD_eq_getLastD_keys +theorem maxD_eq_getD_back?_toArray [TransCmp cmp] {fallback} : + t.maxD fallback = t.toArray.back?.getD fallback := + TreeMap.maxKeyD_eq_getD_back?_keysArray + end Max namespace Equiv @@ -2298,6 +2391,9 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_unit_perm + theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] : t₁ ~m t₂ ↔ (∀ k, k ∈ t₁ ↔ k ∈ t₂) := ⟨fun h _ => h.mem_iff, Equiv.of_forall_mem_iff⟩ @@ -2305,10 +2401,17 @@ theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] : theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_keys_unit_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_keysArray_unit_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff_equiv.trans TreeMap.equiv_iff_keys_unit_eq +theorem equiv_iff_toArray_eq [TransCmp cmp] : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff_equiv.trans TreeMap.equiv_iff_keysArray_unit_eq + theorem insertMany_list_equiv_foldl {l : List α} : insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by constructor @@ -2330,6 +2433,10 @@ theorem toList_filter {f : α → Bool} : (t.filter f).toList = t.toList.filter f := TreeMap.keys_filter_key +theorem toArray_filter {f : α → Bool} : + (t.filter f).toArray = t.toArray.filter f := + TreeMap.keysArray_filter_key + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] {f : α → Bool} : (t.filter f).isEmpty ↔ ∀ k h, f (t.get k h) = false := diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index b804f87e2f..d19513fc06 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -10,6 +10,7 @@ import Std.Data.TreeMap.Raw.Lemmas import Std.Data.DTreeMap.Raw.Lemmas public import Std.Data.TreeSet.Raw.Basic public import Init.Data.List.BasicAux +public import Init.Data.Array.Perm public import Init.Data.Order.ClassesExtra public import Init.Data.Order.Classes @@ -289,6 +290,10 @@ theorem toList_insert_perm {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCm (t.insert k).toList.Perm (if k ∈ t then t.toList else k :: t.toList) := TreeMap.Raw.keys_insertIfNew_perm h +theorem toArray_insert_perm {t : Raw α cmp} [BEq α] [TransCmp cmp] [LawfulBEqCmp cmp] (h : t.WF) {k : α} : + (t.insert k).toArray.Perm (if k ∈ t then t.toArray else t.toArray.push k) := + TreeMap.Raw.keysArray_insertIfNew_perm h + @[simp, grind =] theorem get_erase [TransCmp cmp] (h : t.WF) {k a : α} {h'} : (t.erase k).get a h' = t.get a (mem_of_mem_erase h h') := @@ -459,25 +464,49 @@ theorem length_toList [TransCmp cmp] (h : t.WF) : t.toList.length = t.size := TreeMap.Raw.length_keys h +@[simp, grind =] +theorem size_toArray [TransCmp cmp] (h : t.WF) : + t.toArray.size = t.size := + TreeMap.Raw.size_keysArray h + @[simp, grind =] theorem isEmpty_toList : t.toList.isEmpty = t.isEmpty := TreeMap.Raw.isEmpty_keys +@[simp, grind =] +theorem isEmpty_toArray : + t.toArray.isEmpty = t.isEmpty := + TreeMap.Raw.isEmpty_keysArray + @[simp, grind =] theorem contains_toList [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : t.toList.contains k = t.contains k := TreeMap.Raw.contains_keys h +@[simp, grind =] +theorem contains_toArray [BEq α] [LawfulBEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + t.toArray.contains k = t.contains k := + TreeMap.Raw.contains_keysArray h + @[simp, grind =] theorem mem_toList [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.toList ↔ k ∈ t := TreeMap.Raw.mem_keys h +@[simp, grind =] +theorem mem_toArray [LawfulEqCmp cmp] [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.toArray ↔ k ∈ t := + TreeMap.Raw.mem_keysArray h + theorem mem_of_mem_toList [TransCmp cmp] (h : t.WF) {k : α} : k ∈ t.toList → k ∈ t := TreeMap.Raw.mem_of_mem_keys h +theorem mem_of_mem_toArray [TransCmp cmp] (h : t.WF) {k : α} : + k ∈ t.toArray → k ∈ t := + TreeMap.Raw.mem_of_mem_keysArray h + theorem distinct_toList [TransCmp cmp] (h : t.WF) : t.toList.Pairwise (fun a b => ¬ cmp a b = .eq) := TreeMap.Raw.distinct_keys h @@ -1005,28 +1034,55 @@ theorem foldlM_eq_foldlM_toList [Monad m] [LawfulMonad m] t.foldlM f init = t.toList.foldlM f init := TreeMap.Raw.foldlM_eq_foldlM_keys +theorem foldlM_eq_foldlM_toArray [Monad m] [LawfulMonad m] + {f : δ → α → m δ} {init : δ} : + t.foldlM f init = t.toArray.foldlM f init := + TreeMap.Raw.foldlM_eq_foldlM_keysArray + theorem foldl_eq_foldl_toList {f : δ → α → δ} {init : δ} : t.foldl f init = t.toList.foldl f init := TreeMap.Raw.foldl_eq_foldl_keys +theorem foldl_eq_foldl_toArray {f : δ → α → δ} {init : δ} : + t.foldl f init = t.toArray.foldl f init := + TreeMap.Raw.foldl_eq_foldl_keysArray + theorem foldrM_eq_foldrM_toList [Monad m] [LawfulMonad m] {f : α → δ → m δ} {init : δ} : t.foldrM f init = t.toList.foldrM f init := TreeMap.Raw.foldrM_eq_foldrM_keys +theorem foldrM_eq_foldrM_toArray [Monad m] [LawfulMonad m] + {f : α → δ → m δ} {init : δ} : + t.foldrM f init = t.toArray.foldrM f init := + TreeMap.Raw.foldrM_eq_foldrM_keysArray + theorem foldr_eq_foldr_toList {f : α → δ → δ} {init : δ} : t.foldr f init = t.toList.foldr f init := TreeMap.Raw.foldr_eq_foldr_keys +theorem foldr_eq_foldr_toArray {f : α → δ → δ} {init : δ} : + t.foldr f init = t.toArray.foldr f init := + TreeMap.Raw.foldr_eq_foldr_keysArray + theorem forM_eq_forM_toList [Monad m] [LawfulMonad m] {f : α → m PUnit} : ForM.forM t f = t.toList.forM f := TreeMap.Raw.forM_eq_forM_keys +theorem forM_eq_forM_toArray [Monad m] [LawfulMonad m] {f : α → m PUnit} : + ForM.forM t f = t.toArray.forM f := + TreeMap.Raw.forM_eq_forM_keysArray + theorem forIn_eq_forIn_toList [Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ} : ForIn.forIn t init f = ForIn.forIn t.toList init f := TreeMap.Raw.forIn_eq_forIn_keys +theorem forIn_eq_forIn_toArray [Monad m] [LawfulMonad m] + {f : α → δ → m (ForInStep δ)} {init : δ} : + ForIn.forIn t init f = ForIn.forIn t.toArray init f := + TreeMap.Raw.forIn_eq_forIn_keysArray + end monadic @[simp, grind =] @@ -1413,6 +1469,11 @@ theorem min?_eq_head?_toList [TransCmp cmp] (h : t.WF) : t.min? = t.toList.head? := TreeMap.Raw.minKey?_eq_head?_keys h +@[grind =_] +theorem min?_eq_getElem?_toArray [TransCmp cmp] (h : t.WF) : + t.min? = t.toArray[0]? := + TreeMap.Raw.minKey?_eq_getElem?_keysArray h + theorem min?_eq_some_min! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.min? = some t.min! := TreeMap.Raw.minKey?_eq_some_minKey! h he @@ -1498,6 +1559,11 @@ theorem min!_eq_head!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) : t.min! = t.toList.head! := TreeMap.Raw.minKey!_eq_head!_keys h +@[grind =_] +theorem min!_eq_getElem!_toArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.min! = t.toArray[0]! := + TreeMap.Raw.minKey!_eq_getElem!_keysArray h + theorem min?_eq_some_minD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} : t.min? = some (t.minD fallback) := TreeMap.Raw.minKey?_eq_some_minKeyD h he @@ -1587,6 +1653,10 @@ 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 +theorem minD_eq_getD_toArray [TransCmp cmp] (h : t.WF) {fallback} : + t.minD fallback = t.toArray.getD 0 fallback := + TreeMap.Raw.minKeyD_eq_getD_keysArray h + end Min section Max @@ -1722,6 +1792,10 @@ theorem max?_erase_le_max? [TransCmp cmp] (h : t.WF) {k km kme} : t.max? = t.toList.getLast? := TreeMap.Raw.maxKey?_eq_getLast?_keys h +@[grind =_] theorem max?_eq_back?_toArray [TransCmp cmp] (h : t.WF) : + t.max? = t.toArray.back? := + TreeMap.Raw.maxKey?_eq_back?_keysArray h + theorem max?_eq_some_max! [TransCmp cmp] [Inhabited α] (h : t.WF) (he : t.isEmpty = false) : t.max? = some t.max! := TreeMap.Raw.maxKey?_eq_some_maxKey! h he @@ -1807,6 +1881,11 @@ theorem max!_eq_getLast!_toList [TransCmp cmp] [Inhabited α] (h : t.WF) : t.max! = t.toList.getLast! := TreeMap.Raw.maxKey!_eq_getLast!_keys h +@[grind =_] +theorem max!_eq_back!_toArray [TransCmp cmp] [Inhabited α] (h : t.WF) : + t.max! = t.toArray.back! := + TreeMap.Raw.maxKey!_eq_back!_keysArray h + theorem max?_eq_some_maxD [TransCmp cmp] (h : t.WF) (he : t.isEmpty = false) {fallback} : t.max? = some (t.maxD fallback) := TreeMap.Raw.maxKey?_eq_some_maxKeyD h he @@ -1896,6 +1975,11 @@ theorem maxD_eq_getLastD_toList [TransCmp cmp] (h : t.WF) {fallback} : t.maxD fallback = t.toList.getLastD fallback := TreeMap.Raw.maxKeyD_eq_getLastD_keys h +@[grind =_] +theorem maxD_eq_getD_back?_toArray [TransCmp cmp] (h : t.WF) {fallback} : + t.maxD fallback = t.toArray.back?.getD fallback := + TreeMap.Raw.maxKeyD_eq_getD_back?_keysArray h + end Max namespace Equiv @@ -2139,13 +2223,23 @@ theorem empty_equiv_iff_isEmpty : empty ~m t ↔ t.isEmpty := theorem equiv_iff_toList_perm : t₁ ~m t₂ ↔ t₁.toList.Perm t₂.toList := equiv_iff.trans TreeMap.Raw.equiv_iff_keys_unit_perm +theorem equiv_iff_toArray_perm : t₁ ~m t₂ ↔ t₁.toArray.Perm t₂.toArray := + equiv_iff.trans TreeMap.Raw.equiv_iff_keysArray_unit_perm + theorem Equiv.of_toList_perm (h : t₁.toList.Perm t₂.toList) : t₁ ~m t₂ := ⟨.of_keys_unit_perm h⟩ +theorem Equiv.of_toArray_perm (h : t₁.toArray.Perm t₂.toArray) : t₁ ~m t₂ := + ⟨.of_keysArray_unit_perm h⟩ + theorem equiv_iff_toList_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ t₁.toList = t₂.toList := equiv_iff.trans (TreeMap.Raw.equiv_iff_keys_unit_eq h₁.1 h₂.1) +theorem equiv_iff_toArray_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : + t₁ ~m t₂ ↔ t₁.toArray = t₂.toArray := + equiv_iff.trans (TreeMap.Raw.equiv_iff_keysArray_unit_eq h₁.1 h₂.1) + theorem equiv_iff_forall_mem_iff [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : t₁ ~m t₂ ↔ (∀ k, k ∈ t₁ ↔ k ∈ t₂) := ⟨fun h _ => h.mem_iff h₁ h₂, Equiv.of_forall_mem_iff h₁ h₂⟩ @@ -2169,6 +2263,10 @@ theorem toList_filter {f : α → Bool} (h : t.WF) : (t.filter f).toList = t.toList.filter f := TreeMap.Raw.keys_filter_key h +theorem toArray_filter {f : α → Bool} (h : t.WF) : + (t.filter f).toArray = t.toArray.filter f := + TreeMap.Raw.keysArray_filter_key h + @[grind =] theorem isEmpty_filter_iff [TransCmp cmp] {f : α → Bool} (h : t.WF) : (t.filter f).isEmpty ↔ @@ -2236,4 +2334,10 @@ theorem get_filter [TransCmp cmp] end filter +theorem toArray_toList : t.toList.toArray = t.toArray := + TreeMap.Raw.toArray_keys + +theorem toList_toArray : t.toArray.toList = t.toList := + TreeMap.Raw.toList_keysArray + end Std.TreeSet.Raw