max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: natCast in grind cutsat (#8776)

Browse source 
This PR ensures that user provided `natCast` application are properly
internalized in the grind cutsat module.
This commit is contained in:
Leonardo de Moura 2025-06-13 13:56:00 -04:00 • committed by GitHub
parent 4b7ea26d91
commit ff6eb56f5c
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
4 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
View file

@ -290,7 +290,7 @@ def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
/-- Different kinds of terms internalized by this module. -/
private inductive SupportedTermKind where
| add | mul | num | div | mod | sub | pow | natAbs | toNat
| add | mul | num | div | mod | sub | pow | natAbs | toNat | natCast
deriving BEq
private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
@ -307,6 +307,7 @@ private def getKindAndType? (e : Expr) : Option (SupportedTermKind × Expr) :=
some (.num, α)
| Int.natAbs _ => some (.natAbs, Nat.mkType)
| Int.toNat _ => some (.toNat, Nat.mkType)
| NatCast.natCast α _ _ => some (.natCast, α)
| _ => none
private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) : Bool := Id.run do
@ -315,7 +316,7 @@ private def isForbiddenParent (parent? : Option Expr) (k : SupportedTermKind) :
-- TODO: document `NatCast.natCast` case.
-- Remark: we added it to prevent natCast_sub from being expanded twice.
if declName == ``NatCast.natCast then return true
if k matches .div | .mod | .sub | .pow | .natAbs | .toNat then return false
if k matches .div | .mod | .sub | .pow | .natAbs | .toNat | .natCast then return false
if declName == ``HAdd.hAdd || declName == ``LE.le || declName == ``Dvd.dvd then return true
match k with
| .add => return false

3
tests/lean/grind/omega_regressions.lean
View file

@ -1,3 +0,0 @@
-- These are test cases extracted from Mathlib, where `omega` works but `grind` does not (yet!)
example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by grind

4
tests/lean/run/grind_cutsat_nat_le.lean
View file

@ -27,7 +27,9 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
grind
/--
trace: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
trace: [grind.cutsat.assert] -1*↑a ≤ 0
[grind.cutsat.assert] -1*↑b ≤ 0
[grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
[grind.cutsat.assert] -1*↑c ≤ 0
[grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
[grind.cutsat.assert] -1*↑0 = 0

2
tests/lean/run/grind_natCast_issue.lean Normal file
View file

@ -0,0 +1,2 @@
example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by
grind