feat: add basic simprocs for Nat

src/Lean/Meta/Tactic/Simp.lean

@@ -10,6 +10,7 @@ import Lean.Meta.Tactic.Simp.Main
 import Lean.Meta.Tactic.Simp.Rewrite
 import Lean.Meta.Tactic.Simp.SimpAll
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs
 
 namespace Lean
 

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

@@ -0,0 +1,6 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat

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

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Offset
+import Lean.Meta.Tactic.Simp.Simproc
+
+namespace Nat
+open Lean Meta Simp
+
+def fromExpr? (e : Expr) : SimpM (Option Nat) := do
+  let some n ← evalNat e |>.run | return none
+  return some n
+
+@[inline] def reduceBin (declName : Name) (arity : Nat) (op : Nat → Nat → Nat) (e : Expr) : SimpM (Option Step) := do
+  unless e.isAppOfArity declName arity do return none
+  let some n ← fromExpr? e.appFn!.appArg! | return none
+  let some m ← fromExpr? e.appArg! | return none
+  return some (.done { expr := mkNatLit (op n m) })
+
+@[inline] def reduceBinPred (declName : Name) (arity : Nat) (op : Nat → Nat → Bool) (e : Expr) : SimpM (Option Step) := do
+  unless e.isAppOfArity declName arity do return none
+  let some n ← fromExpr? e.appFn!.appArg! | return none
+  let some m ← fromExpr? e.appArg! | return none
+  let d ← mkDecide e
+  if op n m then
+    return some (.done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] })
+  else
+    return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] })
+
+builtin_simproc reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc reduceDiv ((_ / _ : Nat)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc reduceMod ((_ % _ : Nat)) := reduceBin ``HMod.hMod 6 (· % ·)
+builtin_simproc reducePow ((_ ^ _ : Nat)) := reduceBin ``HPow.hPow 6 (· ^ ·)
+builtin_simproc reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
+
+builtin_simproc reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc reduceLE  (( _ : Nat) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc reduceGT  (( _ : Nat) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc reduceGE  (( _ : Nat) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end Nat

tests/lean/matchOfNatIssue.lean.expected.out

@@ -1,3 +1,3 @@
 x : Int
 h : x = 2
-⊢ Int.ofNat (2 / 1) = x
+⊢ Int.ofNat 2 = x

tests/lean/simprocEval1.lean

@@ -0,0 +1,63 @@
+def foo (_ : Nat) := 10
+
+example : foo x = 8 + 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 5 * 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 12 - 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 20 / 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = 110 % 100 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = (3+2)*2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x * foo x = 10 ^ 2 := by
+  simp
+  trace_state
+  rw [foo]
+
+example : foo x = Nat.gcd 10 20 := by
+  simp
+  trace_state
+  rw [foo]
+
+def boo (_ : Nat) := True
+
+example : boo x ↔ 2 < 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ 3 > 2 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ 2 ≤ 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ 3 ≥ 2 := by
+  simp
+  trace_state
+  trivial

tests/lean/simprocEval1.lean.expected.out

@@ -0,0 +1,24 @@
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x * foo x = 100
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x