From 200f65649ac094b7aea4b53d962e91aa80bddaa7 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Tue, 17 Feb 2026 13:03:01 +0100 Subject: [PATCH] feat: relate `HashSet.ofList` to a fold (#12521) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR shows `HashSet.ofList l ~m l.foldl (init := ∅) fun acc a => acc.insert a` (which is "just" the definition). We also include the analogous statement about `insertMany`, and prove this lemmas for dependent hash maps, normal hash maps, hash sets, as well as the raw and extensional versions, and of course we also give the corresponding tree map statements. --- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 30 +++++++++++ src/Std/Data/DHashMap/Internal/WF.lean | 20 +++++++ src/Std/Data/DHashMap/Lemmas.lean | 39 ++++++++++++++ src/Std/Data/DHashMap/RawLemmas.lean | 33 ++++++++++++ src/Std/Data/DTreeMap/Internal/Lemmas.lean | 53 +++++++++++++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 47 ++++++++++++++++ src/Std/Data/DTreeMap/Raw/Lemmas.lean | 44 +++++++++++++-- src/Std/Data/ExtDHashMap/Lemmas.lean | 38 +++++++++++++ src/Std/Data/ExtDTreeMap/Lemmas.lean | 38 +++++++++++++ src/Std/Data/ExtHashMap/Lemmas.lean | 24 +++++++++ src/Std/Data/ExtHashSet/Lemmas.lean | 14 +++-- src/Std/Data/ExtTreeMap/Lemmas.lean | 24 +++++++++ src/Std/Data/ExtTreeSet/Lemmas.lean | 14 +++-- src/Std/Data/HashMap/Lemmas.lean | 27 ++++++++++ src/Std/Data/HashMap/RawLemmas.lean | 27 ++++++++++ src/Std/Data/HashSet/Lemmas.lean | 18 +++++-- src/Std/Data/HashSet/RawLemmas.lean | 18 +++++-- src/Std/Data/TreeMap/Lemmas.lean | 25 +++++++++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 26 +++++++++ src/Std/Data/TreeSet/Lemmas.lean | 15 ++++-- src/Std/Data/TreeSet/Raw/Lemmas.lean | 15 ++++-- 21 files changed, 568 insertions(+), 21 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 05f37bc422..9aac27f7e8 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -4301,6 +4301,20 @@ theorem filterMap_equiv_congr {γ : α → Type w} (h : m₁.1 ~m m₂.1) {f : (a : α) → β a → Option (γ a)} : (m₁.filterMap f).1 ~m (m₂.filterMap f).1 := by simp_to_model [filterMap, Equiv] using h.1.filterMap _ +theorem insertMany_list_equiv_foldl [BEq α] [Hashable α] {l : List ((a : α) × β a)} : + (m₁.insertMany l).1 ~m (l.foldl (init := m₁) (fun acc p => acc.insert p.1 p.2)) := by + rw [insertMany_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insert p.1 p.2) Subtype.val] + · simp_to_model [Equiv] using List.Perm.refl + · intro x y + simp [Raw.insert, x.property] + +theorem insertManyIfNew_list_equiv_foldl [BEq α] [Hashable α] {l : List ((a : α) × β a)} : + (m₁.insertManyIfNew l).1 ~m (l.foldl (init := m₁) (fun acc p => acc.insertIfNew p.1 p.2)) := by + rw [insertManyIfNew_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insertIfNew p.1 p.2) Subtype.val] + · simp_to_model [Equiv] using List.Perm.refl + · intro x y + simp [Raw.insertIfNew, x.property] + namespace Const theorem equiv_iff_toList_perm_toList {β : Type v} (m₁ m₂ : Raw α fun _ => β) : @@ -4420,6 +4434,22 @@ theorem equiv_of_forall_get?_eq [LawfulBEq α] (h₁ : m₁.1.WF) (h₂ : m₂.1 namespace Const variable {β : Type v} (m₁ m₂ : Raw₀ α fun _ => β) + +theorem insertMany_list_equiv_foldl {l : List (α × β)} : + (insertMany m₁ l).1 ~m (l.foldl (init := m₁) (fun (acc : Raw α fun _ => β) p => acc.insert p.1 p.2)) := by + rw [insertMany_list_eq_foldl, ← List.foldl_hom (g₂ := fun acc p => acc.insert p.1 p.2) Subtype.val] + · simp_to_model [Equiv] using List.Perm.refl + · intro x y + simp [Raw.insert, x.property] + +theorem insertManyIfNewUnit_list_equiv_foldl (m₁ : Raw₀ α fun _ => Unit) {l : List α} : + (insertManyIfNewUnit m₁ l).1 ~m (l.foldl (init := m₁) (fun acc a => acc.insertIfNew a ())) := by + rw [insertManyIfNewUnit_list_eq_foldl, + ← List.foldl_hom (g₂ := fun acc a => acc.insertIfNew a ()) Subtype.val] + · simp_to_model [Equiv] using List.Perm.refl + · intro x y + simp [Raw.insertIfNew, x.property] + variable [EquivBEq α] [LawfulHashable α] theorem get?_eq_of_equiv (h₁ : m₁.1.WF) (h₂ : m₂.1.WF) (h : m₁.1 ~m m₂.1) {k : α} : diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index b62c66248c..50609a718f 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -1347,6 +1347,11 @@ theorem toListModel_insertMany_list [BEq α] [Hashable α] [EquivBEq α] [Lawful apply toListModel_insertListₘ exact h +theorem insertMany_list_eq_foldl [BEq α] [Hashable α] + {m : Raw₀ α β} {l : List ((a : α) × β a)} : + (insertMany m l).1 = l.foldl (init := m) fun a b => a.insert b.1 b.2 := by + simpa [insertMany] using (List.foldl_hom Subtype.val (by simp)).symm + /-! # `eraseMany` -/ theorem WF.eraseManyEntries [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} @@ -1445,6 +1450,11 @@ theorem toListModel_insertManyIfNew_list [BEq α] [Hashable α] [EquivBEq α] [L apply toListModel_insertListIfNewₘ exact h +theorem insertManyIfNew_list_eq_foldl [BEq α] [Hashable α] + {m : Raw₀ α β} {l : List ((a : α) × β a)} : + (insertManyIfNew m l).1 = l.foldl (init := m) fun a b => a.insertIfNew b.1 b.2 := by + simpa [insertManyIfNew] using (List.foldl_hom Subtype.val (by simp)).symm + /-! # `union` -/ theorem wf_union₀ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] @@ -1567,6 +1577,11 @@ theorem Const.wf_insertMany₀ {β : Type v} [BEq α] [Hashable α] [EquivBEq α {l : ρ} (h' : m.WF) : (Const.insertMany ⟨m, h⟩ l).1.1.WF := (Raw₀.Const.insertMany ⟨m, h⟩ l).2 _ Raw.WF.insert₀ h' +theorem Const.insertMany_list_eq_foldl {β : Type v} [BEq α] [Hashable α] + {m : Raw₀ α (fun _ => β)} {l : List (α × β)} : + (Const.insertMany m l).1 = l.foldl (init := m) fun a b => a.insert b.1 b.2 := by + simpa [Const.insertMany] using (List.foldl_hom Subtype.val (by simp)).symm + /-! # `Const.insertListIfNewUnitₘ` -/ theorem Const.toListModel_insertListIfNewUnitₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] @@ -1600,6 +1615,11 @@ theorem Const.wf_insertManyIfNewUnit₀ [BEq α] [Hashable α] [EquivBEq α] [La {l : ρ} (h' : m.WF) : (Const.insertManyIfNewUnit ⟨m, h⟩ l).1.1.WF := (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).2 _ Raw.WF.insertIfNew₀ h' +theorem Const.insertManyIfNewUnit_list_eq_foldl [BEq α] [Hashable α] + {m : Raw₀ α (fun _ => Unit)} {l : List α} : + (Const.insertManyIfNewUnit m l).1 = l.foldl (init := m) fun a b => a.insertIfNew b () := by + simpa [Const.insertManyIfNewUnit] using (List.foldl_hom Subtype.val (by simp)).symm + theorem beq_eq_beqModel [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) : beq m₁ m₂ = beqModel (toListModel m₁.1.buckets) (toListModel m₂.1.buckets) := by simp [beq, beqModel, Raw.size_eq_length h₁, Raw.size_eq_length h₂, Raw.all_eq_all_toListModel, diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 467ce1e49b..1ea82a9674 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -3577,6 +3577,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : DHashMap α (fun _ => Unit)).insertIfNew hd ()) tl := ext <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons (α := α)) +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := (rfl) + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -4572,6 +4575,42 @@ theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap α β} [EquivBEq α] [Lawful m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩ +theorem insertMany_list_equiv_foldl {m : DHashMap α β} {l : List ((a : α) × β a)} : + m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact Raw₀.insertMany_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l) + · exact fun m _ => by simp [Raw.insert_eq m.2, insert] + +theorem ofList_equiv_foldl {l : List ((a : α) × β a)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl + +theorem Const.insertMany_list_equiv_foldl {β : Type v} {m : DHashMap α fun _ => β} + {l : List (α × β)} : + insertMany m l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact Raw₀.Const.insertMany_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l) + · exact fun m _ => by simp [Raw.insert_eq m.2, insert] + +theorem Const.ofList_equiv_foldl {β : Type v} {l : List (α × β)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl + +theorem Const.insertManyIfNewUnit_list_equiv_foldl {m : DHashMap α fun _ => Unit} + {l : List α} : + insertManyIfNewUnit m l ~m + l.foldl (init := m) fun acc a => acc.insertIfNew a () := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl ⟨m.1, m.2.size_buckets_pos⟩ (l := l) + · exact fun m _ => by simp [Raw.insertIfNew_eq m.2, insertIfNew] + +theorem Const.unitOfList_equiv_foldl {l : List α} : + unitOfList l ~m l.foldl (init := ∅) fun acc p => acc.insertIfNew p () := + insertManyIfNewUnit_list_equiv_foldl + namespace Const variable {β : Type v} {m₁ m₂ : DHashMap α fun _ => β} diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index f81d7eb622..76eb6cf820 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -4148,6 +4148,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} : simp_to_raw rw [Raw₀.Const.insertManyIfNewUnit_emptyWithCapacity_list_cons] +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := (rfl) + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -5229,6 +5232,36 @@ theorem equiv_iff_toList_perm {m₁ m₂ : DHashMap.Raw α β} [EquivBEq α] [La m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩ +theorem insertMany_list_equiv_foldl {m : DHashMap.Raw α β} {l : List ((a : α) × β a)} (h : m.WF) : + m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + rw [insertMany_eq h] + exact (Raw₀.insertMany_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l)) + +theorem ofList_equiv_foldl {l : List ((a : α) × β a)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl .empty + +theorem Const.insertMany_list_equiv_foldl {β : Type v} {m : DHashMap.Raw α fun _ => β} + {l : List (α × β)} (h : m.WF) : + insertMany m l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + rw [Const.insertMany_eq h] + exact (Raw₀.Const.insertMany_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l)) + +theorem Const.ofList_equiv_foldl {β : Type v} {l : List (α × β)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl .empty + +theorem Const.insertManyIfNewUnit_list_equiv_foldl {m : DHashMap.Raw α fun _ => Unit} + {l : List α} (h : m.WF) : + insertManyIfNewUnit m l ~m + l.foldl (init := m) fun acc a => acc.insertIfNew a () := by + rw [Const.insertManyIfNewUnit_eq h] + exact (Raw₀.Const.insertManyIfNewUnit_list_equiv_foldl ⟨m, h.size_buckets_pos⟩ (l := l)) + +theorem Const.unitOfList_equiv_foldl {l : List α} : + unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := + insertManyIfNewUnit_list_equiv_foldl .empty + namespace Const variable {β : Type v} {m₁ m₂ : DHashMap.Raw α fun _ => β} diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index ad89db5a18..136e6a9f3b 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -2187,6 +2187,13 @@ theorem isEmpty_insertMany!_list [TransOrd α] (h : t.WF) (t.insertMany! l).1.isEmpty = (t.isEmpty && l.isEmpty) := by simpa only [insertMany_eq_insertMany!] using isEmpty_insertMany_list h +theorem ofList_eq_insertMany {l : List ((a : α) × β a)} : + ofList l = insertMany .empty l balanced_empty := rfl + +theorem ofList_eq_insertMany! {l : List ((a : α) × β a)} : + ofList l = insertMany! .empty l := by + rw [ofList_eq_insertMany, insertMany_eq_insertMany!] + namespace Const variable {β : Type v} {t : Impl α β} @@ -2590,6 +2597,13 @@ theorem get!_insertMany!_list [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabite (l.findSomeRev? (fun ⟨a, b⟩ => if compare a k =.eq then some b else none)).getD (get! t k) := by simpa only [insertMany_eq_insertMany!] using get!_insertMany_list h +theorem ofList_eq_insertMany {l : List (α × β)} : + ofList l = insertMany .empty l balanced_empty := rfl + +theorem ofList_eq_insertMany! {l : List (α × β)} : + ofList l = insertMany! .empty l := by + rw [ofList_eq_insertMany, insertMany_eq_insertMany!] + variable {t : Impl α Unit} theorem insertManyIfNewUnit_cons (h : t.WF) {l : List α} {k : α} : @@ -2862,6 +2876,13 @@ theorem getD_insertManyIfNewUnit!_list getD (insertManyIfNewUnit! t l).1 k fallback = () := rfl +theorem unitOfList_eq_insertManyIfNewUnit {l : List α} : + unitOfList l = insertManyIfNewUnit .empty l balanced_empty := rfl + +theorem unitOfList_eq_insertManyIfNewUnit! {l : List α} : + unitOfList l = insertManyIfNewUnit! .empty l := by + rw [unitOfList_eq_insertManyIfNewUnit, insertManyIfNewUnit_eq_insertManyIfNewUnit!] + end Const @[simp] @@ -9286,6 +9307,22 @@ 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 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] + +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 + rw [insertMany!_eq_foldl] + +theorem insertManyIfNew_list_equiv_foldl {l : List ((a : α) × β a)} (h : t₁.WF) : + t₁.insertManyIfNew l h.balanced ~m (l.foldl (init := t₁) fun acc p => acc.insertIfNew! p.1 p.2) := by + rw [insertManyIfNew_eq_foldl] + +theorem insertManyIfNew!_list_equiv_foldl {l : List ((a : α) × β a)} : + t₁.insertManyIfNew! l ~m (l.foldl (init := t₁) fun acc p => acc.insertIfNew! p.1 p.2) := by + rw [insertManyIfNew!_eq_foldl] + section Const variable {β : Type v} {t₁ t₂ : Impl α β} @@ -9321,6 +9358,22 @@ 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.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] + +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 + rw [insertMany!_eq_foldl] + +theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : Impl α Unit} {l : List α} (h : t₁.WF) : + insertManyIfNewUnit t₁ l h.balanced ~m (l.foldl (init := t₁) fun acc a => acc.insertIfNew! a ()) := by + rw [insertManyIfNewUnit_eq_foldl] + +theorem Const.insertManyIfNewUnit!_list_equiv_foldl {t₁ : Impl α Unit} {l : List α} : + insertManyIfNewUnit! t₁ l ~m (l.foldl (init := t₁) fun acc a => acc.insertIfNew! a ()) := by + rw [insertManyIfNewUnit!_eq_foldl] + end Const end Equiv diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 286cebe2d8..1c2a8fcb75 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -2140,6 +2140,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : DTreeMap α Unit cmp).insertIfNew hd ()) tl := ext Impl.Const.insertManyIfNewUnit_empty_list_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := rfl + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -5904,6 +5907,26 @@ 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 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 + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)] + · exact Impl.insertMany_list_equiv_foldl t₁.wf + · exact fun _ _ => Impl.insert_eq_insert!.symm + +theorem ofList_equiv_foldl {l : List ((a : α) × β a)} : + ofList l cmp ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + +theorem insertManyIfNew_list_equiv_foldl {l : List ((a : α) × β a)} : + t₁.insertManyIfNew l ~m l.foldl (init := t₁) fun acc p => acc.insertIfNew p.1 p.2 := by + constructor + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insertIfNew! p.1 p.2)] + · exact Impl.insertManyIfNew_list_equiv_foldl t₁.wf + · exact fun _ _ => Impl.insertIfNew_eq_insertIfNew!.symm + section Const variable {β : Type v} {t₁ t₂ : DTreeMap α β cmp} @@ -5927,6 +5950,30 @@ theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) 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 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 + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)] + · exact Impl.Const.insertMany_list_equiv_foldl t₁.wf + · exact fun _ _ => Impl.insert_eq_insert!.symm + +theorem Const.ofList_equiv_foldl {l : List (α × β)} : + ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + +theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : DTreeMap α Unit cmp} {l : List α} : + insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) (fun acc a => acc.insertIfNew a ()) := by + constructor + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew! a ())] + · exact Impl.Const.insertManyIfNewUnit_list_equiv_foldl t₁.wf + · exact fun _ _ => Impl.insertIfNew_eq_insertIfNew!.symm + +theorem Const.unitOfList_equiv_foldl {l : List α} : + unitOfList l cmp ~m l.foldl (init := ∅) (fun acc a => acc.insertIfNew a ()) := by + simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl + end Const end Equiv diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index adee7aae69..7c387f65ab 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -1894,9 +1894,7 @@ theorem ofList_cons {k : α} {v : β k} {tl : List ((a : α) × (β a))} : theorem ofList_eq_insertMany_empty {l : List ((a : α) × (β a))} : ofList l cmp = insertMany (∅ : Raw α β cmp) l := - match l with - | [] => by simp - | ⟨k, v⟩ :: tl => by simp [ofList_cons, insertMany_cons] + ext Impl.ofList_eq_insertMany! @[simp, grind =] theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] @@ -2190,6 +2188,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl := ext Impl.Const.insertManyIfNewUnit_empty_list_cons_eq_insertManyIfNewUnit! +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := + ext Impl.Const.unitOfList_eq_insertManyIfNewUnit! + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -5760,6 +5762,18 @@ 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 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 + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)] + · exact Impl.insertMany!_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List ((a : α) × β a)} : + ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + section Const variable {β : Type v} {t₁ t₂ : Raw α β cmp} @@ -5785,6 +5799,30 @@ theorem Equiv.of_constToList_perm : (Const.toList t₁).Perm (Const.toList t₂) 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 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 + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert! p.1 p.2)] + · exact Impl.Const.insertMany!_list_equiv_foldl + · exact fun _ _ => rfl + +theorem Const.ofList_equiv_foldl {l : List (α × β)} : + ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + +theorem Const.insertManyIfNewUnit_list_equiv_foldl {t₁ : Raw α Unit cmp} {l : List α} : + insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by + constructor + let : Ord α := ⟨cmp⟩ + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew! a ())] + · exact Impl.Const.insertManyIfNewUnit!_list_equiv_foldl + · exact fun _ _ => rfl + +theorem Const.unitOfList_equiv_foldl {l : List α} : + unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl + end Const end Equiv diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean index d546275334..8af4e17da6 100644 --- a/src/Std/Data/ExtDHashMap/Lemmas.lean +++ b/src/Std/Data/ExtDHashMap/Lemmas.lean @@ -1230,6 +1230,13 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : m.insertMany l = ∅ → m = ∅ := insertMany_ind m l id fun _ _ _ _ h => absurd h not_insert_eq_empty +theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : + m.insertMany l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + refine m.inductionOn fun m => ?_ + rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)] + · exact sound DHashMap.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + namespace Const variable {β : Type v} {m : ExtDHashMap α (fun _ => β)} @@ -1496,6 +1503,13 @@ theorem getD_insertMany_list_of_mem [EquivBEq α] [LawfulHashable α] simp only [insertMany_list_mk] exact DHashMap.Const.getD_insertMany_list_of_mem k_beq distinct mem +theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : + insertMany m l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + refine m.inductionOn fun m => ?_ + rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)] + · exact sound DHashMap.Const.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + variable {m : ExtDHashMap α (fun _ => Unit)} variable {ρ : Type w} [ForIn Id ρ α] @@ -1713,6 +1727,13 @@ theorem getD_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] getD (insertManyIfNewUnit m l) k fallback = () := rfl +theorem insertManyIfNewUnit_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + insertManyIfNewUnit m l = l.foldl (init := m) fun acc a => acc.insertIfNew a () := by + refine m.inductionOn fun m => ?_ + rw [insertManyIfNewUnit_list_mk, List.foldl_hom (g₁ := fun acc a => acc.insertIfNew a ())] + · exact sound DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + end Const end insertMany @@ -1868,6 +1889,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List ((a : α simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using DHashMap.isEmpty_ofList +theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List ((a : α) × β a)} : + ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + namespace Const variable {β : Type v} @@ -2021,6 +2046,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using DHashMap.Const.isEmpty_ofList +theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : + ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + @[simp] theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] : unitOfList ([] : List α) = ∅ := @@ -2037,6 +2066,11 @@ theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List conv => rhs; apply insertManyIfNewUnit_list_mk exact congrArg mk DHashMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty [EquivBEq α] [LawfulHashable α] {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := by + conv => rhs; apply insertManyIfNewUnit_list_mk + exact congrArg mk DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -2136,6 +2170,10 @@ theorem getD_unitOfList [EquivBEq α] [LawfulHashable α] getD (unitOfList l) k fallback = () := DHashMap.Const.getD_unitOfList +theorem unitOfList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + unitOfList l = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl] + end Const section Union diff --git a/src/Std/Data/ExtDTreeMap/Lemmas.lean b/src/Std/Data/ExtDTreeMap/Lemmas.lean index 29ae68d420..ebe6e505f6 100644 --- a/src/Std/Data/ExtDTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtDTreeMap/Lemmas.lean @@ -1525,6 +1525,13 @@ theorem insertMany_list_eq_empty_iff [TransCmp cmp] {l : List ((a : α) × β a) t.insertMany l = ∅ ↔ t = ∅ ∧ l = [] := by simp only [← isEmpty_iff, isEmpty_insertMany_list, Bool.and_eq_true, List.isEmpty_iff] +theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List ((a : α) × β a)} : + t.insertMany l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by + refine t.inductionOn fun m => ?_ + rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)] + · exact sound DTreeMap.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + namespace Const variable {β : Type v} {t : ExtDTreeMap α β cmp} @@ -1775,6 +1782,13 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] simp only [insertMany_list_mk] exact DTreeMap.Const.getD_insertMany_list_of_mem k_eq distinct mem +theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List (α × β)} : + insertMany t l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by + refine t.inductionOn fun m => ?_ + rw [insertMany_list_mk, List.foldl_hom (g₁ := fun acc p => acc.insert p.1 p.2)] + · exact sound DTreeMap.Const.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + variable {t : ExtDTreeMap α Unit cmp} @[simp] @@ -1968,6 +1982,13 @@ theorem getD_insertManyIfNewUnit_list [TransCmp cmp] getD (insertManyIfNewUnit t l) k fallback = () := rfl +theorem insertManyIfNewUnit_list_eq_foldl [TransCmp cmp] {l : List α} : + insertManyIfNewUnit t l = l.foldl (init := t) fun acc a => acc.insertIfNew a () := by + refine t.inductionOn fun t => ?_ + rw [insertManyIfNewUnit_list_mk, List.foldl_hom (g₁ := fun acc a => acc.insertIfNew a ())] + · exact sound DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + end Const @[simp, grind =] @@ -2114,6 +2135,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List ((a : α) × β a)} : ofList l cmp = ∅ ↔ l = [] := by simpa [← isEmpty_iff, ← List.isEmpty_iff] using DTreeMap.isEmpty_ofList +theorem ofList_eq_foldl [TransCmp cmp] {l : List ((a : α) × β a)} : + ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + namespace Const variable {β : Type v} @@ -2260,6 +2285,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List (α × β)} : ofList l cmp = ∅ ↔ l = [] := by simpa only [← isEmpty_iff, ← List.isEmpty_iff, Bool.coe_iff_coe] using DTreeMap.Const.isEmpty_ofList +theorem ofList_eq_foldl [TransCmp cmp] {l : List (α × β)} : + ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + @[simp] theorem unitOfList_nil : unitOfList ([] : List α) cmp = (∅ : ExtDTreeMap α Unit cmp) := rfl @@ -2274,6 +2303,11 @@ theorem unitOfList_cons [TransCmp cmp] {hd : α} {tl : List α} : conv => rhs; apply insertManyIfNewUnit_list_mk exact congrArg mk DTreeMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty [TransCmp cmp] {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := by + conv => rhs; apply insertManyIfNewUnit_list_mk + exact congrArg mk DTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -2364,6 +2398,10 @@ theorem getD_unitOfList [TransCmp cmp] {l : List α} {k : α} {fallback : Unit} getD (unitOfList l cmp) k fallback = () := rfl +theorem unitOfList_eq_foldl [TransCmp cmp] {l : List α} : + unitOfList l cmp = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl] + end Const section Union diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean index 43c885f264..e26960d412 100644 --- a/src/Std/Data/ExtHashMap/Lemmas.lean +++ b/src/Std/Data/ExtHashMap/Lemmas.lean @@ -929,6 +929,12 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : m.insertMany l = ∅ → m = ∅ := by simpa only [ext_iff] using ExtDHashMap.Const.eq_empty_of_insertMany_eq_empty +theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : + m.insertMany l = l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + rw [ext_iff, ← List.foldl_hom ExtHashMap.inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact ExtDHashMap.Const.insertMany_list_eq_foldl + · exact fun _ _ => rfl + variable {m : ExtHashMap α Unit} variable {ρ : Type w} [ForIn Id ρ α] @@ -1097,6 +1103,12 @@ theorem eq_empty_of_insertManyIfNewUnit_eq_empty [EquivBEq α] [LawfulHashable insertManyIfNewUnit m l = ∅ → m = ∅ := by simpa only [ext_iff] using ExtDHashMap.Const.eq_empty_of_insertManyIfNewUnit_eq_empty +theorem insertManyIfNewUnit_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + insertManyIfNewUnit m l = l.foldl (init := m) fun acc a => acc.insertIfNew a () := by + rw [ext_iff, ← List.foldl_hom ExtHashMap.inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact ExtDHashMap.Const.insertManyIfNewUnit_list_eq_foldl + · exact fun _ _ => rfl + end section @@ -1247,6 +1259,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List (α × ofList l = ∅ ↔ l = [] := ext_iff.trans ExtDHashMap.Const.ofList_eq_empty_iff +theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List (α × β)} : + ofList l = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + @[simp] theorem unitOfList_nil [EquivBEq α] [LawfulHashable α] : unitOfList ([] : List α) = ∅ := @@ -1262,6 +1278,10 @@ theorem unitOfList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List insertManyIfNewUnit ((∅ : ExtHashMap α Unit).insertIfNew hd ()) tl := ext ExtDHashMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty [EquivBEq α] [LawfulHashable α] {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := + ext ExtDHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -1360,6 +1380,10 @@ theorem unitOfList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} unitOfList l = ∅ ↔ l = [] := ext_iff.trans ExtDHashMap.Const.unitOfList_eq_empty_iff +theorem unitOfList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + unitOfList l = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl] + end section Union diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean index e15720822f..7d394342ee 100644 --- a/src/Std/Data/ExtHashSet/Lemmas.lean +++ b/src/Std/Data/ExtHashSet/Lemmas.lean @@ -566,6 +566,12 @@ theorem eq_empty_of_insertMany_eq_empty [EquivBEq α] [LawfulHashable α] {l : m.insertMany l = ∅ → m = ∅ := by simpa only [ext_iff] using ExtHashMap.eq_empty_of_insertManyIfNewUnit_eq_empty +theorem insertMany_list_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + m.insertMany l = l.foldl (init := m) fun acc a => acc.insert a := by + rw [ext_iff, ← List.foldl_hom ExtHashSet.inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact ExtHashMap.insertManyIfNewUnit_list_eq_foldl + · exact fun _ _ => rfl + end section @@ -588,9 +594,7 @@ theorem ofList_cons [EquivBEq α] [LawfulHashable α] {hd : α} {tl : List α} : theorem ofList_eq_insertMany_empty [EquivBEq α] [LawfulHashable α] {l : List α} : ofList l = insertMany (∅ : ExtHashSet α) l := - match l with - | [] => by simp - | hd :: tl => by simp [ofList_cons, insertMany_cons] + ext ExtHashMap.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [EquivBEq α] [LawfulHashable α] @@ -667,6 +671,10 @@ theorem ofList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} : ofList l = ∅ ↔ l = [] := ext_iff.trans ExtHashMap.unitOfList_eq_empty_iff +theorem ofList_eq_foldl [EquivBEq α] [LawfulHashable α] {l : List α} : + ofList l = l.foldl (init := ∅) fun acc a => acc.insert a := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + end section Ext diff --git a/src/Std/Data/ExtTreeMap/Lemmas.lean b/src/Std/Data/ExtTreeMap/Lemmas.lean index f0b558f49a..bd227bd3f3 100644 --- a/src/Std/Data/ExtTreeMap/Lemmas.lean +++ b/src/Std/Data/ExtTreeMap/Lemmas.lean @@ -1111,6 +1111,12 @@ theorem getD_insertMany_list_of_mem [TransCmp cmp] (t.insertMany l).getD k' fallback = v := ExtDTreeMap.Const.getD_insertMany_list_of_mem k_eq distinct mem +theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List (α × β)} : + t.insertMany l = l.foldl (init := t) fun acc p => acc.insert p.1 p.2 := by + rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact ExtDTreeMap.Const.insertMany_list_eq_foldl + · exact fun _ _ => rfl + section Unit variable {t : ExtTreeMap α Unit cmp} @@ -1261,6 +1267,12 @@ theorem getD_insertManyIfNewUnit_list [TransCmp cmp] getD (insertManyIfNewUnit t l) k fallback = () := rfl +theorem insertManyIfNewUnit_list_eq_foldl [TransCmp cmp] {l : List α} : + insertManyIfNewUnit t l = l.foldl (init := t) fun acc a => acc.insertIfNew a () := by + rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact ExtDTreeMap.Const.insertManyIfNewUnit_list_eq_foldl + · exact fun _ _ => rfl + end Unit @[simp, grind =] @@ -1405,6 +1417,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List (α × β)} : ofList l cmp = ∅ ↔ l = [] := ext_iff.trans ExtDTreeMap.Const.ofList_eq_empty_iff +theorem ofList_eq_foldl [TransCmp cmp] {l : List (α × β)} : + ofList l cmp = l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + @[simp] theorem unitOfList_nil : unitOfList ([] : List α) cmp = @@ -1421,6 +1437,10 @@ theorem unitOfList_cons [TransCmp cmp] {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : ExtTreeMap α Unit cmp).insertIfNew hd ()) tl := ext ExtDTreeMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty [TransCmp cmp] {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := + ext ExtDTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -1511,6 +1531,10 @@ theorem getD_unitOfList [TransCmp cmp] {l : List α} {k : α} {fallback : Unit} getD (unitOfList l cmp) k fallback = () := rfl +theorem unitOfList_eq_foldl [TransCmp cmp] {l : List α} : + unitOfList l cmp = l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + rw [unitOfList_eq_insertManyIfNewUnit_empty, insertManyIfNewUnit_list_eq_foldl] + section Union variable {t₁ t₂ : ExtTreeMap α β cmp} diff --git a/src/Std/Data/ExtTreeSet/Lemmas.lean b/src/Std/Data/ExtTreeSet/Lemmas.lean index b08e9ba406..9b5d727029 100644 --- a/src/Std/Data/ExtTreeSet/Lemmas.lean +++ b/src/Std/Data/ExtTreeSet/Lemmas.lean @@ -1017,6 +1017,12 @@ theorem insertMany_list_eq_empty_iff [TransCmp cmp] {l : List α} : t.insertMany l = ∅ ↔ t = ∅ ∧ l = [] := by simpa only [ext_iff] using ExtTreeMap.insertManyIfNewUnit_list_eq_empty_iff +theorem insertMany_list_eq_foldl [TransCmp cmp] {l : List α} : + t.insertMany l = l.foldl (init := t) fun acc a => acc.insert a := by + rw [ext_iff, ← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact ExtTreeMap.insertManyIfNewUnit_list_eq_foldl + · exact fun _ _ => rfl + @[simp, grind =] theorem ofList_nil : ofList ([] : List α) cmp = @@ -1036,9 +1042,7 @@ theorem ofList_cons [TransCmp cmp] {hd : α} {tl : List α} : theorem ofList_eq_insertMany_empty [TransCmp cmp] {l : List α} : ofList l cmp = insertMany (∅ : ExtTreeSet α cmp) l := - match l with - | [] => by simp - | hd :: tl => by simp [ofList_cons, insertMany_cons] + ext ExtTreeMap.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : @@ -1112,6 +1116,10 @@ theorem ofList_eq_empty_iff [TransCmp cmp] {l : List α} : ofList l cmp = ∅ ↔ l = [] := ext_iff.trans ExtTreeMap.unitOfList_eq_empty_iff +theorem ofList_eq_foldl [TransCmp cmp] {l : List α} : + ofList l cmp = l.foldl (init := ∅) fun acc a => acc.insert a := by + rw [ofList_eq_insertMany_empty, insertMany_list_eq_foldl] + section Min @[simp, grind =] diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 8b23eb5102..f10d3323bc 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -2540,6 +2540,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : HashMap α Unit).insertIfNew hd ()) tl := ext DHashMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := + ext DHashMap.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -3165,6 +3169,29 @@ theorem equiv_iff_keys_unit_perm {m₁ m₂ : HashMap α Unit} [EquivBEq α] [La m₁ ~m m₂ ↔ m₁.keys.Perm m₂.keys := ⟨Equiv.keys_perm, Equiv.of_keys_unit_perm⟩ +theorem insertMany_list_equiv_foldl {m : HashMap α β} {l : List (α × β)} : + m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact DHashMap.Const.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List (α × β)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl + +theorem insertManyIfNewUnit_list_equiv_foldl {m : HashMap α Unit} + {l : List α} : + insertManyIfNewUnit m l ~m l.foldl (init := m) fun acc a=> acc.insertIfNew a () := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact DHashMap.Const.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem unitOfList_equiv_foldl {l : List α} : + unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := + insertManyIfNewUnit_list_equiv_foldl + end Equiv section filterMap diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 37bbc386ee..e154b2e3fa 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -2598,6 +2598,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} : unitOfList (hd :: tl) = insertManyIfNewUnit ((∅ : Raw α Unit).insertIfNew hd ()) tl := ext DHashMap.Raw.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l = insertManyIfNewUnit ∅ l := + ext DHashMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [EquivBEq α] [LawfulHashable α] {l : List α} {k : α} : @@ -3231,6 +3235,29 @@ theorem equiv_iff_keys_unit_perm [EquivBEq α] [LawfulHashable α] {m₁ m₂ : m₁ ~m m₂ ↔ m₁.keys.Perm m₂.keys := ⟨Equiv.keys_perm, Equiv.of_keys_unit_perm⟩ +theorem insertMany_list_equiv_foldl {m : HashMap.Raw α β} {l : List (α × β)} (h : m.WF) : + m.insertMany l ~m l.foldl (init := m) fun acc p => acc.insert p.1 p.2 := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact DHashMap.Raw.Const.insertMany_list_equiv_foldl h.1 + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List (α × β)} : + ofList l ~m l.foldl (init := ∅) fun acc p => acc.insert p.1 p.2 := + insertMany_list_equiv_foldl .empty + +theorem insertManyIfNewUnit_list_equiv_foldl {m : HashMap.Raw α Unit} + {l : List α} (h : m.WF) : + insertManyIfNewUnit m l ~m l.foldl (init := m) fun acc a => acc.insertIfNew a () := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact DHashMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl h.1 + · exact fun _ _ => rfl + +theorem unitOfList_equiv_foldl {l : List α} : + unitOfList l ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := + insertManyIfNewUnit_list_equiv_foldl .empty + section filterMap theorem toList_filterMap {f : α → β → Option γ} (h : m.WF) : diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 661baf78cf..005a9edae7 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -1271,9 +1271,7 @@ theorem ofList_singleton {k : α} : theorem ofList_eq_insertMany_empty {l : List α} : ofList l = insertMany (∅ : HashSet α) l := - match l with - | [] => by simp - | hd :: tl => by simp [ofList_cons, insertMany_cons] + ext HashMap.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [EquivBEq α] [LawfulHashable α] @@ -1460,6 +1458,20 @@ theorem equiv_iff_toList_perm [EquivBEq α] [LawfulHashable α] : m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩ +theorem insertMany_list_equiv_foldl {m : HashSet α} {l : List α} : + m.insertMany l ~m l.foldl (init := m) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact HashMap.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List α} : + ofList l ~m l.foldl (init := ∅) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact HashMap.unitOfList_equiv_foldl + · exact fun _ _ => rfl + end Equiv section filter diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index bfb5b13e7f..db38785692 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -1353,9 +1353,7 @@ theorem ofList_cons {hd : α} {tl : List α} : theorem ofList_eq_insertMany_empty {l : List α} : ofList l = insertMany (∅ : Raw α) l := - match l with - | [] => by simp [insertMany_nil .empty] - | hd :: tl => by simp [ofList_cons, insertMany_cons .empty] + ext HashMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [EquivBEq α] [LawfulHashable α] @@ -1539,6 +1537,20 @@ theorem equiv_iff_toList_perm {m₁ m₂ : Raw α} [EquivBEq α] [LawfulHashable m₁ ~m m₂ ↔ m₁.toList.Perm m₂.toList := ⟨Equiv.toList_perm, Equiv.of_toList_perm⟩ +theorem insertMany_list_equiv_foldl {l : List α} (h : m.WF) : + insertMany m l ~m l.foldl (init := m) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact HashMap.Raw.insertManyIfNewUnit_list_equiv_foldl h.1 + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List α} : + ofList l ~m l.foldl (init := ∅) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact HashMap.Raw.unitOfList_equiv_foldl + · exact fun _ _ => rfl + section filter theorem toList_filter {f : α → Bool} (h : m.WF) : diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index f771b0b2f6..4476a7aae6 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -1440,6 +1440,9 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : TreeMap α Unit cmp).insertIfNew hd ()) tl := ext DTreeMap.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := rfl + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -4354,6 +4357,28 @@ theorem equiv_iff_keys_unit_eq [TransCmp cmp] {t₁ t₂ : TreeMap α Unit cmp} 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 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 + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact DTreeMap.Const.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List (α × β)} : + ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + +theorem insertManyIfNewUnit_list_equiv_foldl {t₁ : TreeMap α Unit cmp} {l : List α} : + insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact DTreeMap.Const.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem unitOfList_equiv_foldl {l : List α} : + unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl + end Equiv section filterMap diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index a302501b92..debe687b75 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -1465,6 +1465,10 @@ theorem unitOfList_cons {hd : α} {tl : List α} : insertManyIfNewUnit ((∅ : Raw α Unit cmp).insertIfNew hd ()) tl := ext DTreeMap.Raw.Const.unitOfList_cons +theorem unitOfList_eq_insertManyIfNewUnit_empty {l : List α} : + unitOfList l cmp = insertManyIfNewUnit ∅ l := + ext DTreeMap.Raw.Const.unitOfList_eq_insertManyIfNewUnit_empty + @[simp] theorem contains_unitOfList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : (unitOfList l cmp).contains k = l.contains k := @@ -4098,6 +4102,28 @@ theorem equiv_iff_keys_unit_eq {t₁ t₂ : Raw α Unit cmp} [TransCmp cmp] (h 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 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 + rw [← List.foldl_hom inner (g₂ := fun acc p => acc.insert p.1 p.2)] + · exact DTreeMap.Raw.Const.insertMany_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List (α × β)} : + ofList l cmp ~m l.foldl (init := ∅) (fun acc p => acc.insert p.1 p.2) := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + +theorem insertManyIfNewUnit_list_equiv_foldl {t₁ : Raw α Unit cmp} {l : List α} : + insertManyIfNewUnit t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insertIfNew a () := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact DTreeMap.Raw.Const.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem unitOfList_equiv_foldl {l : List α} : + unitOfList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insertIfNew a () := by + simpa only [unitOfList_eq_insertManyIfNewUnit_empty] using insertManyIfNewUnit_list_equiv_foldl + end Equiv section filterMap diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index d71ac6edd9..bb89b63391 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -1126,9 +1126,7 @@ theorem ofList_cons {hd : α} {tl : List α} : theorem ofList_eq_insertMany_empty {l : List α} : ofList l cmp = insertMany (∅ : TreeSet α cmp) l := - match l with - | [] => by simp - | hd :: tl => by simp [ofList_cons, insertMany_cons] + ext TreeMap.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : @@ -2304,6 +2302,17 @@ 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 insertMany_list_equiv_foldl {l : List α} : + insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact TreeMap.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List α} : + ofList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insert a := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + end Equiv section filter diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 8ddb016bd7..1a8e8b9f3a 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -1176,9 +1176,7 @@ theorem ofList_cons {hd : α} {tl : List α} : theorem ofList_eq_insertMany_empty {l : List α} : ofList l cmp = insertMany (∅ : Raw α cmp) l := - match l with - | [] => by simp - | hd :: tl => by simp [ofList_cons, insertMany_cons] + ext TreeMap.Raw.unitOfList_eq_insertManyIfNewUnit_empty @[simp, grind =] theorem contains_ofList [TransCmp cmp] [BEq α] [LawfulBEqCmp cmp] {l : List α} {k : α} : @@ -2145,6 +2143,17 @@ 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 insertMany_list_equiv_foldl {l : List α} : + insertMany t₁ l ~m l.foldl (init := t₁) fun acc a => acc.insert a := by + constructor + rw [← List.foldl_hom inner (g₂ := fun acc a => acc.insertIfNew a ())] + · exact TreeMap.Raw.insertManyIfNewUnit_list_equiv_foldl + · exact fun _ _ => rfl + +theorem ofList_equiv_foldl {l : List α} : + ofList l cmp ~m l.foldl (init := ∅) fun acc a => acc.insert a := by + simpa only [ofList_eq_insertMany_empty] using insertMany_list_equiv_foldl + end Equiv section filter