From 084c0975688c1ab589f05013cef69393c082dd01 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Dec 2025 21:43:01 -0800 Subject: [PATCH 1/3] chore: use `not_value` at `Nat.pow_pos` and remove `TODO` from `grind_lint_bitvec.lean` --- src/Init/Data/Nat/Lemmas.lean | 1 + tests/lean/run/grind_lint_bitvec.lean | 6 ++---- 2 files changed, 3 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index bf38670c6ee2..9c988fb20770 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -1095,6 +1095,7 @@ grind_pattern div_pow_of_pos => a ^ n where guard n > 0 grind_pattern Nat.pow_pos => a ^ n where + not_value a -- Avoid excessive `BitVec` theorem instantiation (See `grind_lint_bitvec.lean`) guard a > 0 protected theorem pow_add' (a m n : Nat) : a ^ (m + n) = a ^ n * a ^ m := by diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean index 1b3f2beebc70..3c542a5c6f61 100644 --- a/tests/lean/run/grind_lint_bitvec.lean +++ b/tests/lean/run/grind_lint_bitvec.lean @@ -7,13 +7,11 @@ import Lean.Elab.Tactic.Grind.LintExceptions #guard_msgs in #grind_lint inspect (min := 30) BitVec.msb_replicate --- TODO: Reduce limit after we add support for `no_value` constraint -- `BitVec.msb_signExtend` is reasonable at 22. #guard_msgs in -#grind_lint inspect (min := 26) BitVec.msb_signExtend +#grind_lint inspect (min := 22) BitVec.msb_signExtend /-! Check BitVec namespace: -/ --- TODO: Reduce limit after we add support for `no_value` constraint. It was `20` #guard_msgs in -#grind_lint check (min := 23) in BitVec +#grind_lint check (min := 20) in BitVec From 0674481232586710c69a9eee78c38853c5db08d0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Dec 2025 22:10:16 -0800 Subject: [PATCH 2/3] chore: did not help symbolic examples --- src/Init/Data/Nat/Lemmas.lean | 2 +- tests/lean/run/grind_lint_bitvec.lean | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/Nat/Lemmas.lean b/src/Init/Data/Nat/Lemmas.lean index 9c988fb20770..76ca3d778226 100644 --- a/src/Init/Data/Nat/Lemmas.lean +++ b/src/Init/Data/Nat/Lemmas.lean @@ -1095,7 +1095,7 @@ grind_pattern div_pow_of_pos => a ^ n where guard n > 0 grind_pattern Nat.pow_pos => a ^ n where - not_value a -- Avoid excessive `BitVec` theorem instantiation (See `grind_lint_bitvec.lean`) + not_value n guard a > 0 protected theorem pow_add' (a m n : Nat) : a ^ (m + n) = a ^ n * a ^ m := by diff --git a/tests/lean/run/grind_lint_bitvec.lean b/tests/lean/run/grind_lint_bitvec.lean index 3c542a5c6f61..2b383ea83b28 100644 --- a/tests/lean/run/grind_lint_bitvec.lean +++ b/tests/lean/run/grind_lint_bitvec.lean @@ -7,11 +7,11 @@ import Lean.Elab.Tactic.Grind.LintExceptions #guard_msgs in #grind_lint inspect (min := 30) BitVec.msb_replicate --- `BitVec.msb_signExtend` is reasonable at 22. +-- `BitVec.msb_signExtend` is reasonable at 26. #guard_msgs in -#grind_lint inspect (min := 22) BitVec.msb_signExtend +#grind_lint inspect (min := 26) BitVec.msb_signExtend /-! Check BitVec namespace: -/ #guard_msgs in -#grind_lint check (min := 20) in BitVec +#grind_lint check (min := 23) in BitVec From 166f0187e569ee2b8c83526d3061b6a31cd60277 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Dec 2025 22:13:22 -0800 Subject: [PATCH 3/3] chore: test --- tests/lean/run/grind_match_cond_issue.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/tests/lean/run/grind_match_cond_issue.lean b/tests/lean/run/grind_match_cond_issue.lean index 869a9cd489fa..186c8ef3a4c4 100644 --- a/tests/lean/run/grind_match_cond_issue.lean +++ b/tests/lean/run/grind_match_cond_issue.lean @@ -15,3 +15,7 @@ example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False) example {n m a : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * n → False) (h : a ^ 2 = 4 ^ m * n) : False := by grind + +example {m a n : Nat} (ih : ∀ {a : Nat}, a ^ 2 = 4 ^ m * 4 * n → False) + (h : a ^ 2 = 4 ^ (m + 1) * n) : False := by + grind