From cf092e79416c959a8238d89841963a8eb89c2a77 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leomoura@amazon.com>
Date: Sun, 4 Feb 2024 13:50:34 -0800
Subject: [PATCH] refactor: add helper function `evalPropStep` (#3252)

---
 .../Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean |  6 +----
 .../Meta/Tactic/Simp/BuiltinSimprocs/Int.lean |  6 +----
 .../Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean |  7 ++----
 .../Tactic/Simp/BuiltinSimprocs/UInt.lean     |  6 +----
 .../Tactic/Simp/BuiltinSimprocs/Util.lean     | 22 +++++++++++++++++++
 5 files changed, 27 insertions(+), 20 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean

diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
index 15368bed1f40..8ca70d11e9ff 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Fin.lean
@@ -40,11 +40,7 @@ def Value.toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op v₁.value v₂.value then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op v₁.value v₂.value)
 
 /-
 The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
index 496ed6d3707e..7138d98b1191 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Int.lean
@@ -47,11 +47,7 @@ def toExpr (v : Int) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some v₁ ← fromExpr? e.appFn!.appArg! | return .continue
   let some v₂ ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op v₁ v₂ then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op v₁ v₂)
 
 /-
 The following code assumes users did not override the `Int` instances for the arithmetic operators.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
index 5f3d0ba47233..bd017e38d1a1 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Meta.Offset
 import Lean.Meta.Tactic.Simp.Simproc
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Util
 
 namespace Nat
 open Lean Meta Simp
@@ -28,11 +29,7 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   unless e.isAppOfArity declName arity do return .continue
   let some n ← fromExpr? e.appFn!.appArg! | return .continue
   let some m ← fromExpr? e.appArg! | return .continue
-  let d ← mkDecide e
-  if op n m then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op n m)
 
 builtin_simproc [simp, seval] reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
 
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
index 56ce1841a773..dee1096a6836 100644
--- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean
@@ -41,11 +41,7 @@ def $toExpr (v : Value) : Expr :=
   unless e.isAppOfArity declName arity do return .continue
   let some n ← ($fromExpr e.appFn!.appArg!) | return .continue
   let some m ← ($fromExpr e.appArg!) | return .continue
-  let d ← mkDecide e
-  if op n.value m.value then
-    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``true))] }
-  else
-    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+  evalPropStep e (op n.value m.value)
 
 builtin_simproc [simp, seval] $(mkIdent `reduceAdd):ident ((_ + _ : $typeName)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc [simp, seval] $(mkIdent `reduceMul):ident ((_ * _ : $typeName)) := reduceBin ``HMul.hMul 6 (· * ·)
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean
new file mode 100644
index 000000000000..2d4a6184a979
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Util.lean
@@ -0,0 +1,22 @@
+/-
+Copyright (c) 2024 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.Simproc
+
+namespace Lean.Meta.Simp
+
+/--
+Let `result` be the result of evaluating proposition `p`, return a `.done` step where
+the resulting expression is `True`(`False`) if `result is `true`(`false`), and the
+proof is uses `Decidable p` and the auxiliary theorems `eq_true_of_decide`/`eq_false_of_decide`.
+-/
+def evalPropStep (p : Expr) (result : Bool) : SimpM Step := do
+  let d ← mkDecide p
+  if result then
+    return .done { expr := mkConst ``True, proof? := mkAppN (mkConst ``eq_true_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``true))] }
+  else
+    return .done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[p, d.appArg!, (← mkEqRefl (mkConst ``false))] }
+
+end Lean.Meta.Simp