refactor: add helper function evalPropStep (leanprover#3252)

hhu-adam · Feb 4, 2024 · cf092e7 · cf092e7
1 parent 43bbedc
commit cf092e7
Show file tree

Hide file tree

Showing 5 changed files with 27 additions and 20 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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