chore: fix test

src/Init/Data/Nat/Linear.lean

@@ -32,7 +32,7 @@ inductive Expr where
   | add  (a b : Expr)
   | mulL (k : Nat) (a : Expr)
   | mulR (a : Expr) (k : Nat)
-  deriving Inhabited
+  deriving Inhabited, BEq
 
 def Expr.denote (ctx : Context) : Expr → Nat
   | .add a b  => Nat.add (denote ctx a) (denote ctx b)

src/Lean/Meta/Tactic/Simp/Arith.lean

@@ -9,19 +9,9 @@ import Lean.Meta.Tactic.Simp.Arith.Int
 
 namespace Lean.Meta.Simp.Arith
 
-def parentIsTarget (parent? : Option Expr) : Bool :=
+def parentIsTarget (parent? : Option Expr) (isNatExpr : Bool) : Bool :=
   match parent? with
   | none => false
-  | some parent => isLinearTerm parent || isLinearCnstr parent || isDvdCnstr parent
-
-def simp? (e : Expr) (parent? : Option Expr) : MetaM (Option (Expr × Expr)) := do
-  -- TODO: invoke `Int` procedures and add support for arbitrary ordered comm rings
-  if isLinearCnstr e then
-    Nat.simpCnstr? e
-  else if isLinearTerm e && !parentIsTarget parent? then
-    trace[Meta.Tactic.simp] "arith expr: {e}"
-    Nat.simpExpr? e
-  else
-    return none
+  | some parent => isLinearTerm parent isNatExpr || isLinearCnstr parent || isDvdCnstr parent
 
 end Lean.Meta.Simp.Arith

src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean

@@ -71,13 +71,11 @@ def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
   let (e, ctx) ← toLinearExpr input
   let p  := e.toPoly
   let p' := p.norm
-  if p'.length < p.length then
-    -- We only return some if monomials were fused
-    let e' : LinearExpr := p'.toExpr
-    let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
-    let r ← e'.toArith ctx
-    return some (r, ← mkExpectedTypeHint p (← mkEq input r))
-  else
+  let e' : LinearExpr := p'.toExpr
+  if e' == e then
     return none
+  let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
+  let r ← e'.toArith ctx
+  return some (r, ← mkExpectedTypeHint p (← mkEq input r))
 
 end Lean.Meta.Simp.Arith.Nat

src/Lean/Meta/Tactic/Simp/Arith/Util.lean

@@ -34,14 +34,16 @@ def withAbstractAtoms (atoms : Array Expr) (type : Name) (k : Array Expr → Met
   go 0 #[] #[] #[]
 
 /-- Quick filter for linear terms. -/
-def isLinearTerm (e : Expr) : Bool :=
+def isLinearTerm (e : Expr) (isNatExpr : Bool) : Bool :=
   let f := e.getAppFn
   if !f.isConst then
     false
   else
     let n := f.constName!
-    n == ``HAdd.hAdd || n == ``HMul.hMul || n == ``HSub.hSub || n == ``Neg.neg || n == ``Nat.succ
-    || n == ``Add.add || n == ``Mul.mul || n == ``Sub.sub
+    n == ``HAdd.hAdd || n == ``HMul.hMul || n == ``Neg.neg || n == ``Nat.succ
+    || n == ``Add.add || n == ``Mul.mul
+    -- Recall that `Nat.sub` is truncated
+    || (!isNatExpr && (n == ``HSub.hSub || n == ``Sub.sub))
 
 /-- Quick filter for linear constraints. -/
 partial def isLinearCnstr (e : Expr) : Bool :=

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -280,35 +280,38 @@ where
   catch _ =>
     return .continue
 
+private def isNatExpr (e : Expr) : MetaM Bool := do
+  let type ← inferType e
+  let_expr Nat ← type | return false
+  return true
+
 def simpArith (e : Expr) : SimpM Step := do
   unless (← getConfig).arith do
     return .continue
   if Arith.isLinearCnstr e then
     if let some (e', h) ← Arith.Nat.simpCnstr? e then
       return .visit { expr := e', proof? := h }
-    else if let some (e', h) ← Arith.Int.simpRel? e then
+    if let some (e', h) ← Arith.Int.simpRel? e then
       return .visit { expr := e', proof? := h }
-    else if let some (e', h) ← Arith.Int.simpEq? e then
+    if let some (e', h) ← Arith.Int.simpEq? e then
       return .visit { expr := e', proof? := h }
-    else
-      return .continue
-  else if Arith.isLinearTerm e then
-    if Arith.parentIsTarget (← getContext).parent? then
+    return .continue
+  let isNat ← isNatExpr e
+  if Arith.isLinearTerm e isNat then
+    if Arith.parentIsTarget (← getContext).parent? isNat then
       -- We mark `cache := false` to ensure we do not miss simplifications.
       return .continue (some { expr := e, cache := false })
-    else if let some (e', h) ← Arith.Nat.simpExpr? e then
-      return .visit { expr := e', proof? := h }
-    else if let some (e', h) ← Arith.Int.simpExpr? e then
+    if isNat then
+      let some (e', h) ← Arith.Nat.simpExpr? e | pure ()
       return .visit { expr := e', proof? := h }
     else
-      return .continue
-  else if Arith.isDvdCnstr e then
-    if let some (e', h) ← Arith.Int.simpDvd? e then
+      let some (e', h) ← Arith.Int.simpExpr? e | pure ()
       return .visit { expr := e', proof? := h }
-    else
-      return .continue
-  else
     return .continue
+  if Arith.isDvdCnstr e then
+    let some (e', h) ← Arith.Int.simpDvd? e | pure ()
+    return .visit { expr := e', proof? := h }
+  return .continue
 
 /--
 Given a match-application `e` with `MatcherInfo` `info`, return `some result`

tests/lean/run/simpCnstr1.lean

@@ -1,41 +1,55 @@
-import Lean
 
-open Lean in open Lean.Meta in
-def test (declName : Name) : MetaM Unit := do
-  let info ← getConstInfo declName
-  forallTelescope info.type fun _ e => do
-    let some (e', p) ← Simp.Arith.simp? e none | throwError "failed to simplify{indentExpr e}"
-    check p
-    unless (← isDefEq (← inferType p) (← mkEq e e')) do
-      throwError "invalid proof"
-    IO.println s!"{← Meta.ppExpr e} ==> {← Meta.ppExpr e'}"
+example (a b : Nat) (h : a ≤ 2) : a + b + 1 + a < b + 4 + a := by
+  simp +arith
+  exact h
 
-axiom ex1 (a b : Nat) : a + b + 1 + a < b + 4 + a
-axiom ex2 (a b : Nat) : a + b + 1 + a = b + 4 + a + b
-axiom ex3 (a b : Nat) : 5 = b + 4 + a + b
-axiom ex4 (a b : Nat) : 4 = 1 + a
-axiom ex5 (a b : Nat) : 4 + ((a + a) + b) + (a + a) + (b + b) ≤ 3 + (4*a + b) + b + 8 + 1
-axiom ex6 (a b : Nat) : 4 = 8 + a
-axiom ex7 (a b : Nat) : a + a ≤ 8 + a + a + b
-axiom ex8 (a b c d : Nat) : b + a + c + d ≤ a + b + a + b
-axiom ex9 (a b : Nat) : a + b + 1 + a > b + 4 + a
-axiom ex10 (a b : Nat) : a + b + 1 + a ≥ b + 4 + a
-axiom ex11 (a b : Nat) : ¬ (a + b + 1 + a < b + 4 + a)
-axiom ex12 (a b : Nat) : ¬ (a + b + 1 + a > b + 4 + a)
-axiom ex13 (a b : Nat) : ¬ (a + b + 1 + a ≤ b + 4 + a)
-axiom ex14 (a b c d : Nat) : ¬ (a + d + b + 1 + a + d ≥ b + 4 + a + c)
+example (a b : Nat) (h : a = b + 3) : a + b + 1 + a = b + 4 + a + b := by
+  simp +arith
+  exact h
 
-#eval test ``ex1
-#eval test ``ex2
-#eval test ``ex3
-#eval test ``ex4
-#eval test ``ex5
-#eval test ``ex6
-#eval test ``ex7
-#eval test ``ex8
-#eval test ``ex9
-#eval test ``ex10
-#eval test ``ex11
-#eval test ``ex12
-#eval test ``ex13
-#eval test ``ex14
+example (a b : Nat) (h : 1 = a + 2*b) : 5 = b + 4 + a + b := by
+  simp +arith
+  exact h
+
+example (a : Nat) (h : 3 = a) : 4 = 1 + a := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : b ≤ 8) : 4 + ((a + a) + b) + (a + a) + (b + b) ≤ 3 + (4*a + b) + b + 8 + 1 := by
+  simp +arith
+  exact h
+
+example (a : Nat) (h : False) : 4 = 8 + a := by
+  simp +arith
+  exact h
+
+example (a b : Nat) : a + a ≤ 8 + a + a + b := by
+  simp +arith
+
+example (a b c d : Nat) (h : c + d ≤ a + b) : b + a + c + d ≤ a + b + a + b := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : 4 ≤ a) : a + b + 1 + a > b + 4 + a := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : 3 ≤ a) : a + b + 1 + a ≥ b + 4 + a := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : 3 ≤ a) : ¬ (a + b + 1 + a < b + 4 + a) := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : a ≤ 3) : ¬ (a + b + 1 + a > b + 4 + a) := by
+  simp +arith
+  exact h
+
+example (a b : Nat) (h : 4 ≤ a) : ¬ (a + b + 1 + a ≤ b + 4 + a) := by
+  simp +arith
+  exact h
+
+example (a b c d : Nat) (h : a + 2*d ≤ c + 2) : ¬ (a + d + b + 1 + a + d ≥ b + 4 + a + c) := by
+  simp +arith
+  exact h

tests/lean/run/simp_arith_issues.lean

@@ -16,3 +16,8 @@ example {a b : Nat} : (if a < b then a else b - 1) ≤ b := by
 
 example {a b : Nat} : b > 0 → (if a < b then a else b - 1) < b := by
   grind
+
+example (a b : Nat) (h : (a + 1) * 8 - 1 = b) : b = 8*a + 7 := by
+  simp +arith at h
+  guard_hyp h : 8*a + 7 = b
+  rw [h]