feat: relate HashSet.ofList to a fold (#12521)
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.
This commit is contained in:
Markus Himmel
GitHub
parent
bfc5d43ad3
commit
200f65649a
21 changed files with 568 additions and 21 deletions
|
|
@ -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 : α} :
|
||||
|
|
|
|||
|
|
@ -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,
|
||||
|
|
|
|||
|
|
@ -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 _ => β}
|
||||
|
|
|
|||
|
|
@ -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 _ => β}
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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}
|
||||
|
|
|
|||
|
|
@ -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 =]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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) :
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue