From 29e84fa7eaacddaa42df27494cccb6ab1e89f3fd Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Mon, 2 Dec 2024 10:57:15 +1100
Subject: [PATCH] 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 https://github.com/ImperialCollegeLondon/FLT/pull/260.
---
 src/Lean/Elab/Tactic/Omega/Frontend.lean | 1 +
 tests/lean/run/omega.lean                | 6 ++++++
 2 files changed, 7 insertions(+)

diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index 0d992d100f..9c407fda61 100644
--- 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
index 5dbd185978..36061c90d8 100644
--- 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