From bba399eefef79236c976a68f26a9b0fc101e730e Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 17 Nov 2025 17:58:28 +1100 Subject: [PATCH] chore: finish dealing with `#grind_lint` (#11207) This ensures that no `grind` annotated theorem, simply by being instantiated, causes a chain of >20 further instantiations, with a small list of documented exceptions. --- src/Init/Data/Option/Lemmas.lean | 5 +++- src/Init/Data/Vector/Extract.lean | 10 +++++-- src/Init/Data/Vector/Range.lean | 6 ++++- src/Lean/Elab/Tactic/Grind/Lint.lean | 8 ++++++ src/Std/Data/DHashMap/RawLemmas.lean | 8 +++++- src/Std/Data/HashMap/RawLemmas.lean | 8 +++++- src/Std/Data/HashSet/RawLemmas.lean | 8 +++++- tests/lean/run/grind_lint.lean | 40 +++++++++++----------------- 8 files changed, 62 insertions(+), 31 deletions(-) diff --git a/src/Init/Data/Option/Lemmas.lean b/src/Init/Data/Option/Lemmas.lean index de615d6484..cdc2351597 100644 --- a/src/Init/Data/Option/Lemmas.lean +++ b/src/Init/Data/Option/Lemmas.lean @@ -212,10 +212,13 @@ theorem bind_comm {f : α → β → Option γ} (a : Option α) (b : Option β) (a.bind fun x => b.bind (f x)) = b.bind fun y => a.bind fun x => f x y := by cases a <;> cases b <;> rfl -@[grind =] theorem bind_assoc (x : Option α) (f : α → Option β) (g : β → Option γ) : (x.bind f).bind g = x.bind fun y => (f y).bind g := by cases x <;> rfl +grind_pattern bind_assoc => (x.bind f).bind g where + f =/= some + g =/= some + theorem bind_congr {α β} {o : Option α} {f g : α → Option β} : (h : ∀ a, o = some a → f a = g a) → o.bind f = o.bind g := by cases o <;> simp diff --git a/src/Init/Data/Vector/Extract.lean b/src/Init/Data/Vector/Extract.lean index fbbb6cb69f..39b2ae7723 100644 --- a/src/Init/Data/Vector/Extract.lean +++ b/src/Init/Data/Vector/Extract.lean @@ -176,7 +176,6 @@ theorem set_eq_push_extract_append_extract {xs : Vector α n} {i : Nat} (h : i < rcases xs with ⟨as, rfl⟩ simp [Array.set_eq_push_extract_append_extract] -@[grind =] theorem extract_reverse {xs : Vector α n} {i j : Nat} : xs.reverse.extract i j = (xs.extract (n - j) (n - i)).reverse.cast (by omega) := by ext i h @@ -184,10 +183,17 @@ theorem extract_reverse {xs : Vector α n} {i j : Nat} : congr 1 omega -@[grind =] +grind_pattern extract_reverse => xs.reverse.extract i j where + i =/= n - _ + j =/= n - _ + theorem reverse_extract {xs : Vector α n} {i j : Nat} : (xs.extract i j).reverse = (xs.reverse.extract (n - j) (n - i)).cast (by omega) := by rcases xs with ⟨xs, rfl⟩ simp [Array.reverse_extract] +grind_pattern reverse_extract => (xs.extract i j).reverse where + i =/= n - _ + j =/= n - _ + end Vector diff --git a/src/Init/Data/Vector/Range.lean b/src/Init/Data/Vector/Range.lean index cc49dd9d32..95c83f1f22 100644 --- a/src/Init/Data/Vector/Range.lean +++ b/src/Init/Data/Vector/Range.lean @@ -74,12 +74,16 @@ theorem map_add_range' {a} (s n step) : map (a + ·) (range' s n step) = range' theorem range'_succ_left : range' (s + 1) n step = (range' s n step).map (· + 1) := by ext <;> simp <;> omega -@[grind _=_] theorem range'_append {s m n step : Nat} : range' s m step ++ range' (s + step * m) n step = range' s (m + n) step := by rw [← toArray_inj] simp [Array.range'_append] +grind_pattern range'_append => range' s m step ++ range' (s + step * m) n step + +grind_pattern range'_append => range' s (m + n) step where + s =/= _ + _ * _ -- This cuts off an infinite chain of instantiations. + @[simp] theorem range'_append_1 {s m n : Nat} : range' s m ++ range' (s + m) n = range' s (m + n) := by simpa using range'_append (step := 1) diff --git a/src/Lean/Elab/Tactic/Grind/Lint.lean b/src/Lean/Elab/Tactic/Grind/Lint.lean index 92968b169e..5858bad56f 100644 --- a/src/Lean/Elab/Tactic/Grind/Lint.lean +++ b/src/Lean/Elab/Tactic/Grind/Lint.lean @@ -189,3 +189,11 @@ def elabGrindLintCheck : CommandElab := fun stx => liftTermElabM <| withTheReade Tactic.TryThis.addSuggestion stx { suggestion := .string suggestion } end Lean.Elab.Tactic.Grind + +-- We allow these as grind lemmas even though they triggers >20 further instantiations. +-- See tests/lean/run/grind_lint.lean for more details. +#grind_lint skip BitVec.msb_replicate +#grind_lint skip BitVec.msb_signExtend +#grind_lint skip List.replicate_sublist_iff +#grind_lint skip List.Sublist.append +#grind_lint skip List.Sublist.middle diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index f0388a5a76..43e4d2fc06 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -2425,7 +2425,6 @@ theorem insertMany_list_singleton (h : m.WF) simp_to_raw rw [Raw₀.Const.insertMany_cons] -@[grind _=_] theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} : insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by induction l₁ generalizing m with @@ -2433,6 +2432,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} : | cons hd tl ih => rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert] +grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where + l₁ =/= [] + l₂ =/= [] +grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where + l₁ =/= [] + l₂ =/= [] + @[elab_as_elim] theorem insertMany_ind {motive : Raw α (fun _ => β) → Prop} (m : Raw α fun _ => β) (l : ρ) (init : motive m) (insert : ∀ m a b, motive m → motive (m.insert a b)) : diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 13b021048f..9f30b6a852 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1148,7 +1148,6 @@ theorem insertMany_cons (h : m.WF) {l : List (α × β)} insertMany m (⟨k, v⟩ :: l) = insertMany (m.insert k v) l := ext (DHashMap.Raw.Const.insertMany_cons h.out) -@[grind _=_] theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} : insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by induction l₁ generalizing m with @@ -1156,6 +1155,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List (α × β)} : | cons hd tl ih => rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert] +grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where + l₁ =/= [] + l₂ =/= [] +grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where + l₁ =/= [] + l₂ =/= [] + @[elab_as_elim] theorem insertMany_ind {motive : Raw α β → Prop} (m : Raw α β) {l : ρ} (init : motive m) (insert : ∀ m a b, motive m → motive (m.insert a b)) : diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 7024c3bdbc..72ebdb546e 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -655,7 +655,6 @@ theorem insertMany_cons (h : m.WF) {l : List α} {k : α} : insertMany m (k :: l) = insertMany (m.insert k) l := ext (HashMap.Raw.insertManyIfNewUnit_cons h.1) -@[grind _=_] theorem insertMany_append (h : m.WF) {l₁ l₂ : List α} : insertMany m (l₁ ++ l₂) = insertMany (insertMany m l₁) l₂ := by induction l₁ generalizing m with @@ -663,6 +662,13 @@ theorem insertMany_append (h : m.WF) {l₁ l₂ : List α} : | cons hd tl ih => rw [List.cons_append, insertMany_cons h, insertMany_cons h, ih h.insert] +grind_pattern insertMany_append => insertMany m (l₁ ++ l₂) where + l₁ =/= [] + l₂ =/= [] +grind_pattern insertMany_append => insertMany (insertMany m l₁) l₂ where + l₁ =/= [] + l₂ =/= [] + @[elab_as_elim] theorem insertMany_ind {motive : Raw α → Prop} (m : Raw α) (l : ρ) (init : motive m) (insert : ∀ m a, motive m → motive (m.insert a)) : diff --git a/tests/lean/run/grind_lint.lean b/tests/lean/run/grind_lint.lean index 92ce2bd449..9d5eb51110 100644 --- a/tests/lean/run/grind_lint.lean +++ b/tests/lean/run/grind_lint.lean @@ -1,51 +1,43 @@ --- Already working: +import Std +import Lean.Elab.Tactic.Grind.Lint +/-! `BitVec` exceptions -/ + +-- `BitVec.msb_replicate` is reasonable at 25. #guard_msgs in -#grind_lint check (min := 20) in Array +#grind_lint inspect (min := 30) BitVec.msb_replicate --- In progress: +-- `BitVec.msb_signExtend` is reasonable at 22. +#guard_msgs in +#grind_lint inspect (min := 25) BitVec.msb_signExtend + +/-! `List` exceptions -/ -- TODO: Not sure what to do here, see https://lean-fro.zulipchat.com/#narrow/channel/503415-grind/topic/.60.23grind_lint.60.20command/near/556730710 -#grind_lint inspect List.getLast?_concat +-- #grind_lint inspect List.getLast?_concat #grind_lint skip List.getLast?_concat -- TODO: We should consider changing the grind annotation for `List.getElem?_eq_none` -- so it only fires if we've already proved the hypothesis holds. (i.e. the new gadget) -- Other than that, everything looks sane here: -#grind_lint inspect List.getLast?_pmap +-- #grind_lint inspect List.getLast?_pmap #grind_lint skip List.getLast?_pmap --- TODO: We should try to remove these attributes; if that's okay we can remove these mutes. -attribute [-grind] List.Sublist.getLast_mem List.Sublist.head_mem --- #grind_lint inspect List.getLast_filter --- #grind_lint inspect List.head_filter -#grind_lint mute List.getLast_filter -#grind_lint mute List.head_filter - -- TODO: `List.Sublist.eq_of_length` should probably only fire when we've already proved the hypotheses. -- `List.replicate_sublist_iff` is reasonable at 30. #guard_msgs in #grind_lint inspect (min := 30) List.replicate_sublist_iff -#grind_lint skip List.replicate_sublist_iff -- `List.Sublist.append` is reasonable at 25. #guard_msgs in #grind_lint inspect (min := 25) List.Sublist.append -#grind_lint skip List.Sublist.append -- `List.Sublist.middle` is reasonable at 25. #guard_msgs in #grind_lint inspect (min := 25) List.Sublist.middle -#grind_lint skip List.Sublist.middle -#grind_lint check (min := 20) in List +/-! Final check of everything: -/ --- TODO: - --- #grind_lint check (min := 20) in Vector --- #grind_lint check (min := 20) in Option --- #grind_lint check (min := 20) in Nat Int Rat Dyadic --- #grind_lint check (min := 20) in Prod Sum --- #grind_lint check (min := 20) in module Std --- #grind_lint check (min := 20) +#guard_msgs in +#grind_lint check (min := 20)