From 1284d43ad71675b84e0399d3fa262aa0a0ef722e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 16 Mar 2025 13:24:51 -0700
Subject: [PATCH] fix: `simp +arith` (#7511)

This PR fixes two bugs in `simp +arith` that were preventing specific
subterms from being normalized.
---
 src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean | 36 ++++++++++---------
 src/Lean/Meta/Tactic/Simp/Main.lean           |  2 +-
 tests/lean/run/simp_arith_issues.lean         | 18 ++++++++++
 3 files changed, 39 insertions(+), 17 deletions(-)
 create mode 100644 tests/lean/run/simp_arith_issues.lean

diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
index d72b66427b..72bcd23eb2 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
@@ -69,7 +69,10 @@ def simpEq? (e : Expr) : MetaM (Option (Expr × Expr)) := do
           let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
           return some (r, ← mkExpectedTypeHint h (← mkEq e r))
 
-def simpLe? (e : Expr) : MetaM (Option (Expr × Expr)) := do
+
+def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr)) := do
+  -- If `e` is not already a `≤`, then we should not check whether it has changed.
+  let checkIfModified := e.isAppOf ``LE.le && checkIfModified
   let some (a, b, atoms) ← leCnstr? e | return none
   withAbstractAtoms atoms ``Int fun atoms => do
     let e := mkIntLE (← a.denoteExpr (atoms[·]!)) (← b.denoteExpr (atoms[·]!))
@@ -82,7 +85,7 @@ def simpLe? (e : Expr) : MetaM (Option (Expr × Expr)) := do
       let r := mkConst ``True
       let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq e r))
-    else if p.toExpr == a && b == .num 0 then
+    else if checkIfModified && p.toExpr == a && b == .num 0 then
       return none
     else
       let k := p.gcdCoeffs'
@@ -106,25 +109,26 @@ def simpRel? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let mut thmName := Name.anonymous
     match_expr arg with
     | LE.le α _ lhs rhs =>
-      if α.isConstOf ``Int then
-        eNew?   := some (mkIntLE (mkIntAdd rhs (mkIntLit 1)) lhs)
-        thmName := ``Int.not_le_eq
+      let_expr Int ← α | pure ()
+      eNew?   := some (mkIntLE (mkIntAdd rhs (mkIntLit 1)) lhs)
+      thmName := ``Int.not_le_eq
     | GE.ge α _ lhs rhs =>
-      if α.isConstOf ``Int then
-        eNew?   := some (mkIntLE (mkIntAdd lhs (mkIntLit 1)) rhs)
-        thmName := ``Int.not_ge_eq
+      let_expr Int ← α | pure ()
+      eNew?   := some (mkIntLE (mkIntAdd lhs (mkIntLit 1)) rhs)
+      thmName := ``Int.not_ge_eq
     | LT.lt α _ lhs rhs =>
-      if α.isConstOf ``Int then
-        eNew?   := some (mkIntLE rhs lhs)
-        thmName := ``Int.not_lt_eq
+      let_expr Int ← α | pure ()
+      eNew?   := some (mkIntLE rhs lhs)
+      thmName := ``Int.not_lt_eq
     | GT.gt α _ lhs rhs =>
-      if α.isConstOf ``Int then
-        eNew?   := some (mkIntLE lhs rhs)
-        thmName := ``Int.not_gt_eq
+      let_expr Int ← α | pure ()
+      eNew?   := some (mkIntLE lhs rhs)
+      thmName := ``Int.not_gt_eq
     | _ => pure ()
     if let some eNew := eNew? then
       let h₁ := mkApp2 (mkConst thmName) (arg.getArg! 2) (arg.getArg! 3)
-      if let some (eNew', h₂) ← simpLe? eNew then
+      -- Already modified
+      if let some (eNew', h₂) ← simpLe? eNew (checkIfModified := false) then
         let h  := mkApp6 (mkConst ``Eq.trans [levelOne]) (mkSort levelZero) e eNew eNew' h₁ h₂
         return some (eNew', h)
       else
@@ -132,7 +136,7 @@ def simpRel? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     else
       return none
   else
-    simpLe? e
+    simpLe? e (checkIfModified := true)
 
 def simpDvd? (e : Expr) : MetaM (Option (Expr × Expr)) := do
   let some (d, e, atoms) ← dvdCnstr? e | return none
diff --git a/src/Lean/Meta/Tactic/Simp/Main.lean b/src/Lean/Meta/Tactic/Simp/Main.lean
index 0b7370abf6..6752638804 100644
--- a/src/Lean/Meta/Tactic/Simp/Main.lean
+++ b/src/Lean/Meta/Tactic/Simp/Main.lean
@@ -520,7 +520,7 @@ def processCongrHypothesis (h : Expr) (hType : Expr) : SimpM Bool := do
       return r.proof?.isSome || (xs.size > 0 && lhs != r.expr)
 
 /-- Try to rewrite `e` children using the given congruence theorem -/
-def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do
+def trySimpCongrTheorem? (c : SimpCongrTheorem) (e : Expr) : SimpM (Option Result) := withNewMCtxDepth do withParent e do
   recordCongrTheorem c.theoremName
   trace[Debug.Meta.Tactic.simp.congr] "{c.theoremName}, {e}"
   let thm ← mkConstWithFreshMVarLevels c.theoremName
diff --git a/tests/lean/run/simp_arith_issues.lean b/tests/lean/run/simp_arith_issues.lean
new file mode 100644
index 0000000000..991673b1a3
--- /dev/null
+++ b/tests/lean/run/simp_arith_issues.lean
@@ -0,0 +1,18 @@
+set_option grind.warning false
+
+example (a b : Int) (f : Int → Int) (h : a = (if a < 0 then b - 1 else 1 - b)) : False := by
+  simp +arith only at h
+  guard_hyp h : a = if a + 1 ≤ 0 then b + -1 else -1 * b + 1
+  sorry
+
+example {a b : Int} : (if a < b then a else b - 1) ≤ b := by
+  grind
+
+example {a b : Int} : (if a < b then a else b - 1) < b := by
+  grind
+
+example {a b : Nat} : (if a < b then a else b - 1) ≤ b := by
+  grind
+
+example {a b : Nat} : b > 0 → (if a < b then a else b - 1) < b := by
+  grind