From 17987b09743026f71b0508488d1904f49109d8a0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Jun 2024 06:52:19 +0100 Subject: [PATCH 1/6] 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' From 218e3a290a77d46367649513e5cbc9279805752c Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Tue, 11 Jun 2024 09:06:03 +0000 Subject: [PATCH 2/6] chore: bump to nightly-2024-06-11 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index d8c33b3609..c868e61f55 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-06-09 +leanprover/lean4:nightly-2024-06-11 From 24ab71f07ccb2356bcca24d24db9d81e33eee8d2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Jun 2024 20:01:43 +1000 Subject: [PATCH 3/6] deprecations --- Batteries/Data/Char.lean | 14 +++---------- Batteries/Data/String/Lemmas.lean | 34 ++++++++++++++++--------------- 2 files changed, 21 insertions(+), 27 deletions(-) diff --git a/Batteries/Data/Char.lean b/Batteries/Data/Char.lean index c94b35ac44..5a9110ae12 100644 --- a/Batteries/Data/Char.lean +++ b/Batteries/Data/Char.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Jannis Limperg -/ import Batteries.Data.UInt +import Batteries.Tactic.Alias @[ext] theorem Char.ext : {a b : Char} → a.val = b.val → a = b | ⟨_,_⟩, ⟨_,_⟩, rfl => rfl @@ -21,16 +22,7 @@ instance : Batteries.LawfulOrd Char := .compareOfLessAndEq namespace String -private theorem csize_eq (c) : - csize c = 1 ∨ csize c = 2 ∨ csize c = 3 ∨ - csize c = 4 := by - simp only [csize, Char.utf8Size] - repeat (first | split | (solve | simp (config := {decide := true}))) - -theorem csize_pos (c) : 0 < csize c := by - rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true}) - -theorem csize_le_4 (c) : csize c ≤ 4 := by - rcases csize_eq c with _|_|_|_ <;> simp_all (config := {decide := true}) +@[deprecated (since := "2024-06-11")] alias csize_pos := Char.utf8Size_pos +@[deprecated (since := "2024-06-11")] alias csize_le_4 := Char.utf8Size_le_four end String diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index 8a9376fe05..0b779d30ad 100644 --- a/Batteries/Data/String/Lemmas.lean +++ b/Batteries/Data/String/Lemmas.lean @@ -33,13 +33,13 @@ instance : Batteries.BEqOrd String := .compareOfLessAndEq String.lt_irrefl attribute [simp] toList -- prefer `String.data` over `String.toList` in lemmas -private theorem add_csize_pos : 0 < i + csize c := - Nat.add_pos_right _ (csize_pos c) +private theorem add_csize_pos : 0 < i + Char.utf8Size c := + Nat.add_pos_right _ (Char.utf8Size_pos c) -private theorem ne_add_csize_add_self : i ≠ n + csize c + i := +private theorem ne_add_csize_add_self : i ≠ n + Char.utf8Size c + i := Nat.ne_of_lt (Nat.lt_add_of_pos_left add_csize_pos) -private theorem ne_self_add_add_csize : i ≠ i + (n + csize c) := +private theorem ne_self_add_add_csize : i ≠ i + (n + Char.utf8Size c) := Nat.ne_of_lt (Nat.lt_add_of_pos_right add_csize_pos) /-- The UTF-8 byte length of a list of characters. (This is intended for specification purposes.) -/ @@ -51,7 +51,7 @@ private theorem ne_self_add_add_csize : i ≠ i + (n + csize c) := @[simp] theorem utf8Len_nil : utf8Len [] = 0 := rfl -@[simp] theorem utf8Len_cons (c cs) : utf8Len (c :: cs) = utf8Len cs + csize c := rfl +@[simp] theorem utf8Len_cons (c cs) : utf8Len (c :: cs) = utf8Len cs + c.utf8Size := rfl @[simp] theorem utf8Len_append (cs₁ cs₂) : utf8Len (cs₁ ++ cs₂) = utf8Len cs₁ + utf8Len cs₂ := by induction cs₁ <;> simp [*, Nat.add_right_comm] @@ -88,7 +88,7 @@ namespace Pos attribute [ext] ext -theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (csize_pos _) +theorem lt_addChar (p : Pos) (c : Char) : p < p + c := Nat.lt_add_of_pos_right (Char.utf8Size_pos _) private theorem zero_ne_addChar {i : Pos} {c : Char} : 0 ≠ i + c := ne_of_lt add_csize_pos @@ -197,11 +197,11 @@ theorem modify_of_valid (cs cs' : List Char) : rw [modify, set_of_valid, get_of_valid]; cases cs' <;> rfl theorem next_of_valid' (cs cs' : List Char) : - next ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + csize (cs'.headD default)⟩ := by + next ⟨cs ++ cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + (cs'.headD default).utf8Size⟩ := by simp only [next, get_of_valid]; rfl theorem next_of_valid (cs : List Char) (c : Char) (cs' : List Char) : - next ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + csize c⟩ := next_of_valid' .. + next ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs⟩ = ⟨utf8Len cs + c.utf8Size⟩ := next_of_valid' .. @[simp] theorem atEnd_iff (s : String) (p : Pos) : atEnd s p ↔ s.endPos ≤ p := decide_eq_true_iff _ @@ -214,7 +214,7 @@ theorem valid_next {p : Pos} (h : p.Valid s) (h₂ : p < s.endPos) : (next s p). simpa using Pos.Valid.mk (cs ++ [c]) cs' theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat} - (hp : i + (utf8Len cs + csize c) = p) : + (hp : i + (utf8Len cs + c.utf8Size) = p) : utf8PrevAux (cs ++ c :: cs') ⟨i⟩ ⟨p⟩ = ⟨i + utf8Len cs⟩ := by match cs with | [] => simp [utf8PrevAux, ← hp, Pos.addChar_eq] @@ -226,7 +226,7 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat} simp [Nat.add_assoc, Nat.add_comm] theorem prev_of_valid (cs : List Char) (c : Char) (cs' : List Char) : - prev ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs + csize c⟩ = ⟨utf8Len cs⟩ := by + prev ⟨cs ++ c :: cs'⟩ ⟨utf8Len cs + c.utf8Size⟩ = ⟨utf8Len cs⟩ := by simp [prev]; refine (if_neg (Pos.ne_of_gt add_csize_pos)).trans ?_ rw [utf8PrevAux_of_valid] <;> simp @@ -310,9 +310,9 @@ theorem firstDiffPos_loop_eq (l₁ l₂ r₁ r₂ stop p) show get ⟨l₂ ++ b :: r₂⟩ ⟨p⟩ = b by simp [hl₂, get_of_valid]] simp; split <;> simp subst b - rw [show next ⟨l₁ ++ a :: r₁⟩ ⟨p⟩ = ⟨utf8Len l₁ + csize a⟩ by simp [hl₁, next_of_valid]] + rw [show next ⟨l₁ ++ a :: r₁⟩ ⟨p⟩ = ⟨utf8Len l₁ + a.utf8Size⟩ by simp [hl₁, next_of_valid]] simpa [← hl₁, ← Nat.add_assoc, Nat.add_right_comm] using - firstDiffPos_loop_eq (l₁ ++ [a]) (l₂ ++ [a]) r₁ r₂ stop (p + csize a) + firstDiffPos_loop_eq (l₁ ++ [a]) (l₂ ++ [a]) r₁ r₂ stop (p + a.utf8Size) (by simp [hl₁]) (by simp [hl₂]) (by simp [hstop, ← Nat.add_assoc, Nat.add_right_comm]) · next h => rw [dif_neg] <;> simp [hstop, ← hl₁, ← hl₂, -Nat.not_lt, Nat.lt_min] @@ -758,7 +758,8 @@ theorem toIterator : ∀ {s}, ValidFor l m r s → s.toIterator.ValidFor l.rever theorem get : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.get ⟨utf8Len m₁⟩ = c | _, ⟨⟩ => by simpa using get_of_valid (l ++ m₁) (c :: m₂ ++ r) -theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + csize c⟩ +theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → + s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + c.utf8Size⟩ | _, ⟨⟩ => by simp [Substring.next] rw [if_neg (mt Pos.ext_iff.1 ?a)] @@ -772,7 +773,8 @@ theorem next : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.next ⟨utf8Len theorem next_stop : ∀ {s}, ValidFor l m r s → s.next ⟨utf8Len m⟩ = ⟨utf8Len m⟩ | _, ⟨⟩ => by simp [Substring.next, Pos.add_eq] -theorem prev : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → s.prev ⟨utf8Len m₁ + csize c⟩ = ⟨utf8Len m₁⟩ +theorem prev : ∀ {s}, ValidFor l (m₁ ++ c :: m₂) r s → + s.prev ⟨utf8Len m₁ + c.utf8Size⟩ = ⟨utf8Len m₁⟩ | _, ⟨⟩ => by simp [Substring.prev] rw [if_neg (mt Pos.ext_iff.1 <| Ne.symm ?a)] @@ -916,7 +918,7 @@ theorem get : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ → s.get simp [h.toString] at e; subst e; simp [h.get] theorem next : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ → - s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + csize c⟩ + s.next ⟨utf8Len m₁⟩ = ⟨utf8Len m₁ + c.utf8Size⟩ | _, h, e => by let ⟨l, m, r, h⟩ := h.validFor simp [h.toString] at e; subst e; simp [h.next] @@ -925,7 +927,7 @@ theorem next_stop : ∀ {s}, Valid s → s.next ⟨s.bsize⟩ = ⟨s.bsize⟩ | _, h => let ⟨l, m, r, h⟩ := h.validFor; by simp [h.bsize, h.next_stop] theorem prev : ∀ {s}, Valid s → s.toString.1 = m₁ ++ c :: m₂ → - s.prev ⟨utf8Len m₁ + csize c⟩ = ⟨utf8Len m₁⟩ + s.prev ⟨utf8Len m₁ + c.utf8Size⟩ = ⟨utf8Len m₁⟩ | _, h, e => by let ⟨l, m, r, h⟩ := h.validFor simp [h.toString] at e; subst e; simp [h.prev] From f96a34401de084c73c787ecb45b85d4fb47bb981 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 02:26:30 +0100 Subject: [PATCH 4/6] chore(RBSet): consolidate API from mathlib (#834) --- Batteries/Data/RBMap/Basic.lean | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/Batteries/Data/RBMap/Basic.lean b/Batteries/Data/RBMap/Basic.lean index ae60899f26..a9ba215ad9 100644 --- a/Batteries/Data/RBMap/Basic.lean +++ b/Batteries/Data/RBMap/Basic.lean @@ -678,6 +678,16 @@ instance [Repr α] : Repr (RBSet α cmp) where /-- `O(log n)`. Insert element `v` into the tree. -/ @[inline] def insert (t : RBSet α cmp) (v : α) : RBSet α cmp := ⟨t.1.insert cmp v, t.2.insert⟩ +/-- +Insert all elements from a collection into a `RBSet α cmp`. +-/ +def insertMany [ForIn Id ρ α] (s : RBSet α cmp) (as : ρ) : + RBSet α cmp := Id.run do + let mut s := s + for a in as do + s := s.insert a + return s + /-- `O(log n)`. Remove an element from the tree using a cut function. The `cut` function is used to locate an element in the tree: From 42b5dddbd6b2658fcfede9dad26cc47737edec2d Mon Sep 17 00:00:00 2001 From: L Date: Tue, 11 Jun 2024 23:15:19 -0700 Subject: [PATCH 5/6] fix(linter): "(invalid MessageData.lazy, missing context)" (#838) --- Batteries/Tactic/Lint/Frontend.lean | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/Batteries/Tactic/Lint/Frontend.lean b/Batteries/Tactic/Lint/Frontend.lean index 4eff8b1450..072e23743f 100644 --- a/Batteries/Tactic/Lint/Frontend.lean +++ b/Batteries/Tactic/Lint/Frontend.lean @@ -125,9 +125,11 @@ def printWarning (declName : Name) (warning : MessageData) (useErrorFormat : Boo (filePath : System.FilePath := default) : CoreM MessageData := do if useErrorFormat then if let some range ← findDeclarationRanges? declName then - return m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: { + let msg ← addMessageContextPartial + m!"{filePath}:{range.range.pos.line}:{range.range.pos.column + 1}: error: { ← mkConstWithLevelParams declName} {warning}" - pure m!"#check {← mkConstWithLevelParams declName} /- {warning} -/" + return msg + addMessageContextPartial m!"#check {← mkConstWithLevelParams declName} /- {warning} -/" /-- Formats a map of linter warnings using `print_warning`, sorted by line number. -/ def printWarnings (results : HashMap Name MessageData) (filePath : System.FilePath := default) From c5ca3f90b2bd4024d75aeda8dea065de9e6853b4 Mon Sep 17 00:00:00 2001 From: leanprover-community-mathlib4-bot Date: Wed, 12 Jun 2024 09:05:17 +0000 Subject: [PATCH 6/6] chore: bump to nightly-2024-06-12 --- lean-toolchain | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lean-toolchain b/lean-toolchain index c868e61f55..2e64b81f61 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:nightly-2024-06-11 +leanprover/lean4:nightly-2024-06-12