From 17987b09743026f71b0508488d1904f49109d8a0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Jun 2024 06:52:19 +0100 Subject: [PATCH] chore: squeeze simps in HashMap.WF (#833) --- Batteries/Data/HashMap/WF.lean | 85 +++++++++++++++++++++------------- 1 file changed, 53 insertions(+), 32 deletions(-) diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean index d535685691..fb2635b8fe 100644 --- a/Batteries/Data/HashMap/WF.lean +++ b/Batteries/Data/HashMap/WF.lean @@ -23,22 +23,25 @@ theorem update_data (self : Buckets α β) (i d h) : theorem exists_of_update (self : Buckets α β) (i d h) : ∃ l₁ l₂, self.1.data = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧ (self.update i d h).1.data = l₁ ++ d :: l₂ := by - simp [Array.getElem_eq_data_get]; exact List.exists_of_set' h + simp only [Array.data_length, Array.ugetElem_eq_getElem, Array.getElem_eq_data_get] + exact List.exists_of_set' h theorem update_update (self : Buckets α β) (i d d' h h') : (self.update i d h).update i d' h' = self.update i d' h := by - simp [update]; congr 1; rw [Array.set_set] + simp only [update, Array.uset, Array.data_length] + congr 1 + rw [Array.set_set] theorem size_eq (data : Buckets α β) : size data = .sum (data.1.data.map (·.toList.length)) := rfl theorem mk_size (h) : (mk n h : Buckets α β).size = 0 := by - simp [Buckets.size_eq, Buckets.mk, mkArray]; clear h + simp only [mk, mkArray, size_eq]; clear h induction n <;> simp [*] theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF := by refine ⟨fun _ h => ?_, fun i h => ?_⟩ - · simp [Buckets.mk, empty', mkArray, List.mem_replicate] at h + · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h simp [h, List.Pairwise.nil] · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_data_get, AssocList.All] @@ -53,16 +56,19 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : · exact match List.mem_or_eq_of_mem_set hl with | .inl hl => H.1 _ hl | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_data ..)) - · revert hp; simp [update_data, Array.getElem_eq_data_get, List.get_set] + · revert hp + simp only [Array.getElem_eq_data_get, update_data, List.get_set, Array.data_length, update_size] split <;> intro hp · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp - · simp at hi; exact H.2 i hi _ hp + · simp only [update_size, Array.data_length] at hi + exact H.2 i hi _ hp end Buckets theorem reinsertAux_size [Hashable α] (data : Buckets α β) (a : α) (b : β) : (reinsertAux data a b).size = data.size.succ := by - simp [Buckets.size_eq, reinsertAux] + simp only [reinsertAux, Array.data_length, Array.ugetElem_eq_getElem, Buckets.size_eq, + Nat.succ_eq_add_one] refine have ⟨l₁, l₂, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_ simp [h₁, Nat.succ_add]; rfl @@ -88,12 +94,13 @@ where · next H => refine (go (i+1) _ _ fun j hj => ?a).trans ?b <;> simp · case a => - simp [List.getD_eq_get?, List.get?_set]; split + simp only [List.getD_eq_get?, List.get?_set, Option.map_eq_map]; split · cases List.get? .. <;> rfl · next H => exact hs _ (Nat.lt_of_le_of_ne (Nat.le_of_lt_succ hj) (Ne.symm H)) · case b => refine have ⟨l₁, l₂, h₁, _, eq⟩ := List.exists_of_set' H; eq ▸ ?_ - simp [h₁, Buckets.size_eq] + simp only [Buckets.size_eq, h₁, List.map_append, List.map_cons, AssocList.toList, + List.length_nil, Nat.sum_append, Nat.sum_cons, Nat.zero_add, Array.data_length] rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1 (conv => rhs; rw [Nat.add_left_comm]); congr 1 rw [← Array.getElem_eq_data_get] @@ -102,9 +109,10 @@ where · next H => rw [(_ : Nat.sum _ = 0), Nat.zero_add] rw [← (_ : source.data.map (fun _ => .nil) = source.data)] - · simp; induction source.data <;> simp [*] + · simp only [List.map_map] + induction source.data <;> simp [*] refine List.ext_get (by simp) fun j h₁ h₂ => ?_ - simp + simp only [List.get_map, Array.data_length] have := (hs j (Nat.lt_of_lt_of_le h₂ (Nat.not_lt.1 H))).symm rwa [List.getD_eq_get?, List.get?_eq_get, Option.getD_some] at this termination_by source.size - i @@ -126,7 +134,8 @@ theorem expand_WF.foldl [BEq α] [Hashable α] (rank : α → Nat) {l : List (α refine ih hl₁.2 hl₂.2 (reinsertAux_WF ht₁ fun _ h => (ht₂ _ (Array.getElem_mem_data ..) _ h).2.1) (fun _ h => ?_) - simp [reinsertAux, Buckets.update] at h + simp only [reinsertAux, Buckets.update, Array.uset, Array.data_length, + Array.ugetElem_eq_getElem, Array.data_set] at h match List.mem_or_eq_of_mem_set h with | .inl h => intro _ hf @@ -157,7 +166,9 @@ where · match List.mem_or_eq_of_mem_set hl with | .inl hl => exact hs₁ _ hl | .inr e => exact e ▸ .nil - · simp [Array.getElem_eq_data_get, List.get_set]; split + · simp only [Array.data_length, Array.size_set, Array.getElem_eq_data_get, Array.data_set, + List.get_set] + split · nofun · exact hs₂ _ (by simp_all) · let rank (k : α) := ((hash k).toUSize % source.size).toNat @@ -182,7 +193,7 @@ theorem insert_size [BEq α] [Hashable α] {m : Imp α β} {k v} · unfold Buckets.size refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_ simp [h, h₁, Buckets.size_eq, Nat.succ_add]; rfl - · rw [expand_size]; simp [h, expand, Buckets.size] + · rw [expand_size]; simp only [expand, h, Buckets.size, Array.data_length, Buckets.update_size] refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_ simp [h₁, Buckets.size_eq, Nat.succ_add]; rfl @@ -191,7 +202,8 @@ private theorem mem_replaceF {l : List (α × β)} {x : α × β} {p : α × β induction l with | nil => exact .inr | cons a l ih => - simp; generalize e : cond .. = z; revert e + simp only [List.replaceF, List.mem_cons] + generalize e : cond .. = z; revert e unfold cond; split <;> (intro h; subst h; simp) · intro | .inl eq => exact eq ▸ .inl rfl @@ -208,7 +220,7 @@ private theorem pairwise_replaceF [BEq α] [PartialEquivBEq α] induction l with | nil => simp [H] | cons a l ih => - simp at H ⊢ + simp only [List.pairwise_cons, List.replaceF] at H ⊢ generalize e : cond .. = z; unfold cond at e; revert e split <;> (intro h; subst h; simp) · next e => exact ⟨(H.1 · · ∘ PartialEquivBEq.trans e), H.2⟩ @@ -222,15 +234,17 @@ theorem insert_WF [BEq α] [Hashable α] {m : Imp α β} {k v} (h : m.buckets.WF) : (insert m k v).buckets.WF := by dsimp [insert, cond]; split · next h₁ => - simp at h₁; have ⟨x, hx₁, hx₂⟩ := h₁ + simp only [AssocList.contains_eq, List.any_eq_true] at h₁; have ⟨x, hx₁, hx₂⟩ := h₁ refine h.update (fun H => ?_) (fun H a h => ?_) - · simp; exact pairwise_replaceF H - · simp [AssocList.All] at H h ⊢ + · simp only [AssocList.toList_replace] + exact pairwise_replaceF H + · simp only [AssocList.All, Array.ugetElem_eq_getElem, AssocList.toList_replace] at H h ⊢ match mem_replaceF h with | .inl rfl => rfl | .inr h => exact H _ h · next h₁ => - rw [Bool.eq_false_iff] at h₁; simp at h₁ + rw [Bool.eq_false_iff] at h₁ + simp only [AssocList.contains_eq, ne_eq, List.any_eq_true, not_exists, not_and] at h₁ suffices _ by split <;> [exact this; refine expand_WF this] refine h.update (.cons ?_) (fun H a h => ?_) · exact fun a h h' => h₁ a h (PartialEquivBEq.symm h') @@ -243,12 +257,13 @@ theorem erase_size [BEq α] [Hashable α] {m : Imp α β} {k} (erase m k).size = (erase m k).buckets.size := by dsimp [erase, cond]; split · next H => - simp [h, Buckets.size] + simp only [h, Buckets.size] refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_ - simp [h, h₁, Buckets.size_eq] + simp only [h₁, Array.data_length, Array.ugetElem_eq_getElem, List.map_append, List.map_cons, + Nat.sum_append, Nat.sum_cons, AssocList.toList_erase] rw [(_ : List.length _ = _ + 1), Nat.add_right_comm]; {rfl} clear h₁ eq - simp [AssocList.contains_eq] at H + simp only [AssocList.contains_eq, List.any_eq_true] at H have ⟨a, h₁, h₂⟩ := H refine have ⟨_, _, _, _, _, h, eq⟩ := List.exists_of_eraseP h₁ h₂; eq ▸ ?_ simp [h]; rfl @@ -257,7 +272,7 @@ theorem erase_size [BEq α] [Hashable α] {m : Imp α β} {k} theorem erase_WF [BEq α] [Hashable α] {m : Imp α β} {k} (h : m.buckets.WF) : (erase m k).buckets.WF := by dsimp [erase, cond]; split - · refine h.update (fun H => ?_) (fun H a h => ?_) <;> simp at h ⊢ + · refine h.update (fun H => ?_) (fun H a h => ?_) <;> simp only [AssocList.toList_erase] at h ⊢ · exact H.sublist (List.eraseP_sublist _) · exact H _ (List.mem_of_mem_eraseP h) · exact h @@ -266,7 +281,7 @@ theorem modify_size [BEq α] [Hashable α] {m : Imp α β} {k} (h : m.size = m.buckets.size) : (modify m k f).size = (modify m k f).buckets.size := by dsimp [modify, cond]; rw [Buckets.update_update] - simp [h, Buckets.size] + simp only [h, Buckets.size] refine have ⟨_, _, h₁, _, eq⟩ := Buckets.exists_of_update ..; eq ▸ ?_ simp [h, h₁, Buckets.size_eq] @@ -275,7 +290,7 @@ theorem modify_WF [BEq α] [Hashable α] {m : Imp α β} {k} dsimp [modify, cond]; rw [Buckets.update_update] refine h.update (fun H => ?_) (fun H a h => ?_) <;> simp at h ⊢ · exact pairwise_replaceF H - · simp [AssocList.All] at H h ⊢ + · simp only [AssocList.All, Array.ugetElem_eq_getElem] at H h ⊢ match mem_replaceF h with | .inl rfl => rfl | .inr h => exact H _ h @@ -296,12 +311,13 @@ theorem WF_iff [BEq α] [Hashable α] {m : Imp α β} : theorem WF.mapVal {α β γ} {f : α → β → γ} [BEq α] [Hashable α] {m : Imp α β} (H : WF m) : WF (mapVal f m) := by have ⟨h₁, h₂⟩ := H.out - simp [Imp.mapVal, Buckets.mapVal, WF_iff, h₁]; refine ⟨?_, ?_, fun i h => ?_⟩ - · simp [Buckets.size]; congr; funext l; simp + simp only [Imp.mapVal, h₁, Buckets.mapVal, WF_iff]; refine ⟨?_, ?_, fun i h => ?_⟩ + · simp only [Buckets.size, Array.map_data, List.map_map]; congr; funext l; simp · simp only [Array.map_data, List.forall_mem_map_iff] simp only [AssocList.toList_mapVal, List.pairwise_map] exact fun _ => h₂.1 _ - · simp [AssocList.All] at h ⊢ + · simp only [Array.size_map, AssocList.All, Array.getElem_map, AssocList.toList_mapVal, + List.mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂] at h ⊢ intro a m apply h₂.2 _ _ _ m @@ -313,7 +329,11 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable induction l generalizing n acc with simp [filterMap.go, g₁, *] | cons a b l => match f a b with | none => rfl - | some c => simp; rw [Nat.add_right_comm]; rfl + | some c => + simp only [Option.map_some', List.reverse_cons, List.append_assoc, List.singleton_append, + List.length_cons, Nat.succ_eq_add_one, Prod.mk.injEq, true_and] + rw [Nat.add_right_comm] + rfl let g l := (g₁ l).reverse.toAssocList let M := StateT (ULift Nat) Id have H2 (l : List (AssocList α β)) n : @@ -334,7 +354,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable suffices ∀ bk sz (h : 0 < bk.length), m.buckets.val.mapM (m := M) (filterMap.go f .nil) ⟨0⟩ = (⟨bk⟩, ⟨sz⟩) → WF ⟨sz, ⟨bk⟩, h⟩ from this _ _ _ rfl - simp [Array.mapM_eq_mapM_data, bind, StateT.bind, H2, g] + simp only [Array.mapM_eq_mapM_data, bind, StateT.bind, H2, List.map_map, Nat.zero_add, g] intro bk sz h e'; cases e' refine .mk (by simp [Buckets.size]) ⟨?_, fun i h => ?_⟩ · simp only [List.forall_mem_map_iff, List.toList_toAssocList] @@ -345,7 +365,8 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable · simp only [Array.size_mk, List.length_map, Array.data_length, Array.getElem_eq_data_get, List.get_map] at h ⊢ have := H.out.2.2 _ h - simp [AssocList.All, g₁] at this ⊢ + simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap, + Option.map_eq_some', forall_exists_index, and_imp, g₁] at this ⊢ rintro _ _ h' _ _ rfl exact this _ h'