From 0342a973fd3b85ebb7f666cf4d3a890bd5dc948c Mon Sep 17 00:00:00 2001 From: Paul Reichert <6992158+datokrat@users.noreply.github.com> Date: Fri, 10 Jan 2025 14:08:53 +0100 Subject: [PATCH] more cleanups --- .../DHashMap/Internal/AssocList/Lemmas.lean | 4 ++-- .../DHashMap/Internal/List/Associative.lean | 19 ++++++++++--------- src/Std/Data/DHashMap/Internal/WF.lean | 4 ++-- 3 files changed, 14 insertions(+), 13 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index 4d5bad1e7727..98d9814bf1ae 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -221,7 +221,7 @@ namespace Const variable {β : Type v} theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} - {l : AssocList α (fun _ => β) } : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by + {l : AssocList α (fun _ => β)} : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by rw [Const.alterKey] split · next heq => @@ -256,7 +256,7 @@ theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option refine insertEntry_cons_of_false (Bool.not_eq_true _ ▸ heq₂) |>.symm |> Perm.trans ?_ exact Perm.cons _ <| ih heq -theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β) } : +theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β)} : modify a f l = alter a (·.map f) l := by induction l · rfl diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index c751540dc0a3..91f38371a645 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -969,7 +969,8 @@ def insertEntry [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : Li @[simp] theorem insertEntry_nil [BEq α] {k : α} {v : β k} : - insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] := by simp [insertEntry] + insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] := + by simp [insertEntry] theorem insertEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} (h : (k' == k) = false) : @@ -1902,9 +1903,9 @@ theorem alterKey_nil [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Opt | none => [] | some b => [⟨a, b⟩] := rfl -theorem containsKey_alterKey_iff [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} +theorem containsKey_alterKey [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} {l : List ((a : α) × β a)} (hl : DistinctKeys l) : - containsKey a (alterKey a f l) ↔ (f (getValueCast? a l)).isSome := by + containsKey a (alterKey a f l) = (f (getValueCast? a l)).isSome := by match l with | [] => simp only [getValueCast?_nil, Bool.coe_iff_coe, alterKey_nil] @@ -2012,10 +2013,10 @@ def alterKey [BEq α] (k : α) (f : Option β → Option β) theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : (alterKey k f l).length = - if h : containsKey k l then - if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1 - else - if f none |>.isSome then l.length + 1 else l.length := by + if h : containsKey k l then + if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1 + else + if f none |>.isSome then l.length + 1 else l.length := by rw [alterKey] cases h : getValue? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry, containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none] @@ -2082,8 +2083,8 @@ theorem mem_insertEntry_of_key_ne [BEq α] [EquivBEq α] {a : α} {b : β} exact fun x => hne (beq_of_eq x.1) |> False.elim theorem mem_eraseKey_of_key_ne [BEq α] [EquivBEq α] {a : α} - {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) - : p ∈ eraseKey a l ↔ p ∈ l := by + {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) : + p ∈ eraseKey a l ↔ p ∈ l := by induction l · simp only [eraseKey_nil] · next ih => diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index dd8f5b653b5b..015dbb420c52 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -563,7 +563,7 @@ theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} simp only [buckets_withComputedSize] simp only [containsKey_of_perm <| toListModel_updateBucket_alter h] rw [← getValueCast?_eq_some_getValueCast h₁] - conv => lhs; congr; rw [containsKey_alterKey_iff (a := a) (f := f) h.distinct]; + conv => lhs; congr; rw [containsKey_alterKey h.distinct]; · next h₁ => rw [containsₘ_eq_containsKey h] at h₁ rw [alterKey] @@ -586,7 +586,7 @@ variable {β : Type v} theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f))) - (Const.alterKey a f (toListModel m.1.buckets)) := by + (Const.alterKey a f (toListModel m.1.buckets)) := by exact toListModel_updateBucket h AssocList.Const.toList_alter List.Const.alterKey_of_perm List.Const.alterKey_append_of_containsKey_right_eq_false