From 5a32473f6695b44643ef81522e892c7d7b4be8d2 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 23 Feb 2024 13:30:05 +1100
Subject: [PATCH] feat: replace ToExpr Int (#3472)

The current `ToExpr Int` instance produces `@Int.ofNat (@OfNat.ofNat Nat
i ...)` for nonnegative `i` and `@Int.negSucc (@OfNat.ofNat Nat (-i+1)
...)` for negative `i`.

However it should be producing `@OfNat.ofNat Int i ...` for nonnegative
`i`, and `@Neg.neg ... (@OfNat.ofNat Int (-i) ...)` for negative `i`.
---
 src/Lean/Elab/Tactic/Omega/Frontend.lean | 22 +++-------------------
 src/Lean/ToExpr.lean                     | 13 ++++++++++---
 tests/lean/run/omega.lean                |  6 +++---
 3 files changed, 16 insertions(+), 25 deletions(-)

diff --git a/src/Lean/Elab/Tactic/Omega/Frontend.lean b/src/Lean/Elab/Tactic/Omega/Frontend.lean
index c9b04294b6..79fbc206a7 100644
--- a/src/Lean/Elab/Tactic/Omega/Frontend.lean
+++ b/src/Lean/Elab/Tactic/Omega/Frontend.lean
@@ -23,22 +23,6 @@ Allow elaboration of `OmegaConfig` arguments to tactics.
 -/
 declare_config_elab elabOmegaConfig Lean.Meta.Omega.OmegaConfig
 
-/--
-The current `ToExpr` instance for `Int` is bad,
-so we roll our own here.
--/
-def mkInt (i : Int) : Expr :=
-  if 0 ≤ i then
-    mkNat i.toNat
-  else
-    mkApp3 (.const ``Neg.neg [0]) (.const ``Int []) (mkNat (-i).toNat)
-      (.const ``Int.instNegInt [])
-where
-  mkNat (n : Nat) : Expr :=
-    let r := mkRawNatLit n
-    mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r
-        (.app (.const ``instOfNat []) r)
-
 /-- Match on the two defeq expressions for successor: `n+1`, `n.succ`. -/
 def succ? (e : Expr) : Option Expr :=
   match e.getAppFnArgs with
@@ -202,16 +186,16 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
   | (``HMod.hMod, #[_, _, _, _, n, k]) =>
     match groundNat? k with
     | some k' => do
-      let k' := mkInt k'
+      let k' := toExpr (k' : Int)
       rewrite (← mkAppM ``HMod.hMod #[n, k']) (mkApp2 (.const ``Int.emod_def []) n k')
     | none => mkAtomLinearCombo e
   | (``HDiv.hDiv, #[_, _, _, _, x, z]) =>
     match groundInt? z with
     | some 0 => rewrite e (mkApp (.const ``Int.ediv_zero []) x)
     | some i => do
-      let e' ← mkAppM ``HDiv.hDiv #[x, mkInt i]
+      let e' ← mkAppM ``HDiv.hDiv #[x, toExpr i]
       if i < 0 then
-        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (mkInt (-i)))
+        rewrite e' (mkApp2 (.const ``Int.ediv_neg []) x (toExpr (-i)))
       else
         mkAtomLinearCombo e'
     | _ => mkAtomLinearCombo e
diff --git a/src/Lean/ToExpr.lean b/src/Lean/ToExpr.lean
index 5bad40dd2b..aeffe52bf4 100644
--- a/src/Lean/ToExpr.lean
+++ b/src/Lean/ToExpr.lean
@@ -31,9 +31,16 @@ instance : ToExpr Nat where
 
 instance : ToExpr Int where
   toTypeExpr := .const ``Int []
-  toExpr i := match i with
-    | .ofNat n => mkApp (.const ``Int.ofNat []) (toExpr n)
-    | .negSucc n => mkApp (.const ``Int.negSucc []) (toExpr n)
+  toExpr i := if 0 ≤ i then
+    mkNat i.toNat
+  else
+    mkApp3 (.const ``Neg.neg [0]) (.const ``Int []) (.const ``Int.instNegInt [])
+      (mkNat (-i).toNat)
+where
+  mkNat (n : Nat) : Expr :=
+    let r := mkRawNatLit n
+    mkApp3 (.const ``OfNat.ofNat [0]) (.const ``Int []) r
+        (.app (.const ``instOfNat []) r)
 
 instance : ToExpr Bool where
   toExpr     := fun b => if b then mkConst ``Bool.true else mkConst ``Bool.false
diff --git a/tests/lean/run/omega.lean b/tests/lean/run/omega.lean
index a37a349f2b..f42745efd5 100644
--- a/tests/lean/run/omega.lean
+++ b/tests/lean/run/omega.lean
@@ -414,13 +414,13 @@ example (i : Fin 7) : (i : Nat) < 8 := by omega
 example (x y z i : Nat) (hz : z ≤ 1) : x % 2 ^ i + y % 2 ^ i + z < 2 * 2^ i := by omega
 
 -- Check that we correctly process base^(e+1) for constant base.
-example (x e : Nat) (hx : x < 2^(e+1)) : x < 2^e *2 := by omega
+example (x e : Nat) (hx : x < 2^(e+1)) : x < 2^e * 2 := by omega
 
 -- Check that we correctly handle `e.succ`
-example (x e : Nat) (hx : x < 2^(e.succ)) : x < 2^e *2 := by omega
+example (x e : Nat) (hx : x < 2^(e.succ)) : x < 2^e * 2 := by omega
 
 -- Check that this works for integer base.
-example (x : Int) (e : Nat) (hx : x < (2 : Int)^(e+1)) : x < 2^e *2 := by omega
+example (x : Int) (e : Nat) (hx : x < (2 : Int)^(e+1)) : x < 2^e * 2 := by omega
 
 /-! ### Ground terms -/