From c358b0c7341de7cdd732b8f09ab552f7405facfb Mon Sep 17 00:00:00 2001 From: Kim Morrison <477956+kim-em@users.noreply.github.com> Date: Mon, 5 Jan 2026 18:55:02 +1000 Subject: [PATCH] feat: add guards for grind patterns for `getElem?_eq_none` theorems (#11761) This PR adds some `grind_pattern` `guard` conditions to potentially expensive theorems. --- src/Init/Data/Array/Lemmas.lean | 3 ++- src/Init/Data/BitVec/Lemmas.lean | 3 +++ src/Init/Data/Vector/Lemmas.lean | 3 ++- src/Init/GetElem.lean | 4 +++- src/Lean/Elab/Tactic/Grind/LintExceptions.lean | 1 + tests/lean/run/grind_lint_1.lean | 5 +---- tests/lean/run/grind_lint_list.lean | 8 +++----- 7 files changed, 15 insertions(+), 12 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index e9d1f8dbde..a92b323cda 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -115,7 +115,8 @@ theorem none_eq_getElem?_iff {xs : Array α} {i : Nat} : none = xs[i]? ↔ xs.si theorem getElem?_eq_none {xs : Array α} (h : xs.size ≤ i) : xs[i]? = none := by simp [h] -grind_pattern Array.getElem?_eq_none => xs.size, xs[i]? +grind_pattern Array.getElem?_eq_none => xs.size, xs[i]? where + guard xs.size ≤ i @[simp] theorem getElem?_eq_getElem {xs : Array α} {i : Nat} (h : i < xs.size) : xs[i]? = some xs[i] := getElem?_pos .. diff --git a/src/Init/Data/BitVec/Lemmas.lean b/src/Init/Data/BitVec/Lemmas.lean index 0a1b6c8d12..d54e589117 100644 --- a/src/Init/Data/BitVec/Lemmas.lean +++ b/src/Init/Data/BitVec/Lemmas.lean @@ -67,6 +67,9 @@ theorem none_eq_getElem?_iff {l : BitVec w} : none = l[n]? ↔ w ≤ n := by @[simp] theorem getElem?_eq_none {l : BitVec w} (h : w ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h +grind_pattern BitVec.getElem?_eq_none => l[n]? where + guard w ≤ n + theorem getElem?_eq (l : BitVec w) (i : Nat) : l[i]? = if h : i < w then some l[i] else none := by split <;> simp_all diff --git a/src/Init/Data/Vector/Lemmas.lean b/src/Init/Data/Vector/Lemmas.lean index f370dd4df8..bddfea8631 100644 --- a/src/Init/Data/Vector/Lemmas.lean +++ b/src/Init/Data/Vector/Lemmas.lean @@ -796,7 +796,8 @@ theorem getElem?_eq_none {xs : Vector α n} (h : n ≤ i) : xs[i]? = none := by -- This is a more aggressive pattern than for `List/Array.getElem?_eq_none`, because -- `length/size` won't appear. -grind_pattern Vector.getElem?_eq_none => xs[i]? +grind_pattern Vector.getElem?_eq_none => xs[i]? where + guard n ≤ i @[simp] theorem getElem?_eq_getElem {xs : Vector α n} {i : Nat} (h : i < n) : xs[i]? = some xs[i] := getElem?_pos .. diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 5aea65e37f..45851fb998 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -366,9 +366,11 @@ instance : GetElem? (List α) Nat α fun as i => i < as.length where theorem none_eq_getElem?_iff {l : List α} {i : Nat} : none = l[i]? ↔ length l ≤ i := by simp [eq_comm (a := none)] -@[grind =] theorem getElem?_eq_none (h : length l ≤ i) : l[i]? = none := getElem?_eq_none_iff.mpr h +grind_pattern getElem?_eq_none => l.length, l[i]? where + guard l.length ≤ i + instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where getElem?_def as i h := by split <;> simp_all diff --git a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean index 39f8dea396..41995f9cec 100644 --- a/src/Lean/Elab/Tactic/Grind/LintExceptions.lean +++ b/src/Lean/Elab/Tactic/Grind/LintExceptions.lean @@ -15,6 +15,7 @@ import Lean.Elab.Tactic.Grind.Lint #grind_lint skip List.replicate_sublist_iff #grind_lint skip List.Sublist.append #grind_lint skip List.Sublist.middle +#grind_lint skip List.getLast?_pmap #grind_lint skip Array.count_singleton #grind_lint skip Array.foldl_empty #grind_lint skip Array.foldr_empty diff --git a/tests/lean/run/grind_lint_1.lean b/tests/lean/run/grind_lint_1.lean index d8d9c6ad4b..40556be183 100644 --- a/tests/lean/run/grind_lint_1.lean +++ b/tests/lean/run/grind_lint_1.lean @@ -96,9 +96,7 @@ info: Try this to display the actual theorem instances: -- Note: The suffix skip should apply during check, but inspect bypasses it -- Array.range_succ and Array.range'_succ should NOT appear in the output /-- -info: instantiating `Array.back?_empty` triggers 19 additional `grind` theorem instantiations ---- -info: instantiating `Array.back?_mapIdx` triggers 18 additional `grind` theorem instantiations +info: instantiating `Array.back?_empty` triggers 17 additional `grind` theorem instantiations --- info: instantiating `Array.count_empty` triggers 19 additional `grind` theorem instantiations --- @@ -109,7 +107,6 @@ info: instantiating `Array.findIdx_singleton` triggers 16 additional `grind` the info: Try this: [apply] #grind_lint check (min := 15) in Array #grind_lint inspect Array.back?_empty - #grind_lint inspect Array.back?_mapIdx #grind_lint inspect Array.count_empty #grind_lint inspect Array.findIdx_empty #grind_lint inspect Array.findIdx_singleton diff --git a/tests/lean/run/grind_lint_list.lean b/tests/lean/run/grind_lint_list.lean index 64cf3428ca..e7ab913b27 100644 --- a/tests/lean/run/grind_lint_list.lean +++ b/tests/lean/run/grind_lint_list.lean @@ -7,11 +7,9 @@ import Lean.Elab.Tactic.Grind.LintExceptions -- #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 skip List.getLast?_pmap +-- `List.getLast?_pmap` is reasonable at 31. +#guard_msgs in +#grind_lint inspect (min := 31) List.getLast?_pmap -- `List.replicate_sublist_iff` is reasonable at 30. #guard_msgs in