feat: omega supports Nat.succ (#474)

leanprover-community · Dec 21, 2023 · 7a51fa8 · 7a51fa8
1 parent 5bf9172
commit 7a51fa8
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/Std/Tactic/Omega/Frontend.lean b/Std/Tactic/Omega/Frontend.lean
@@ -179,6 +179,7 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
         mkAtomLinearCombo e
     | _ => mkAtomLinearCombo e
   | (``Nat.cast, #[_, _, n]) => match n.getAppFnArgs with
+    | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
     | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
     | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
     | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)

diff --git a/test/omega/test.lean b/test/omega/test.lean
@@ -26,6 +26,8 @@ example {x : Int} : x / 0 = 0 := by omega
 
 example {x : Int} : x / 2 + x / (-2) = 0 := by omega
 
+example {x y z : Nat} (_ : a ≤ c) (_ : b ≤ c) : a < Nat.succ c := by omega
+
 example (_ : 7 < 3) : False := by omega
 example (_ : 0 < 0) : False := by omega