feat: omega doesn't get stuck on bare Int.negSucc (#6276)

This PR ensures `omega` doesn't get stuck on bare `Int.negSucc` terms in goals. This came up in ImperialCollegeLondon/FLT#260.
leanprover · Dec 1, 2024 · 29e84fa · 29e84fa
1 parent 6bf8ff3
commit 29e84fa
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 0 deletions.
diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -228,6 +228,7 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
     | .app (.app (.app (.app (.const ``Prod.mk [u, v]) _) _) x) y =>
       rewrite e (mkApp4 (.const ``Prod.snd_mk [u, v]) α x β y)
     | _ => mkAtomLinearCombo e
+  | (``Int.negSucc, #[n]) => rewrite e (mkApp (.const ``Int.negSucc_eq []) n)
   | _ => mkAtomLinearCombo e
 where
   /--

diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean
@@ -466,6 +466,12 @@ example (z : Int) : z.toNat = 0 ↔ z ≤ 0 := by
 example (z : Int) (a : Fin z.toNat) (h : 0 ≤ z) : ↑↑a ≤ z := by
   omega
 
+/-! ### Int.negSucc
+Make sure we aren't stopped by stray `Int.negSucc` terms.
+-/
+
+example (x : Int) (h : Int.negSucc 0 < x ∧ x < 1) : x = 0 := by omega
+
 /-! ### BitVec -/
 open BitVec