feat: add simprocs for Fin

src/Init/Data/Fin/Basic.lean

@@ -100,7 +100,7 @@ instance : ShiftLeft (Fin n) where
 instance : ShiftRight (Fin n) where
   shiftRight := Fin.shiftRight
 
-instance : OfNat (Fin (no_index (n+1))) i where
+instance ofNatInst : OfNat (Fin (no_index (n+1))) i where
   ofNat := Fin.ofNat i
 
 instance : Inhabited (Fin (no_index (n+1))) where

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

@@ -4,3 +4,4 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Fin

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

@@ -0,0 +1,65 @@
+/-
+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.ToExpr
+import Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
+
+namespace Fin
+open Lean Meta Simp
+
+structure Value where
+  ofNatFn   : Expr
+  size      : Nat
+  value     : Nat
+
+def fromExpr? (e : Expr) : SimpM (Option Value) := do
+  unless e.isAppOfArity ``OfNat.ofNat 3 do return none
+  let type ← whnf e.appFn!.appFn!.appArg!
+  unless type.isAppOfArity ``Fin 1 do return none
+  let some size ← evalNat type.appArg! |>.run | return none
+  unless size > 0 do return none
+  let some value ← evalNat e.appFn!.appArg! |>.run | return none
+  let value := value % size
+  return some { size, value, ofNatFn := e.appFn!.appFn! }
+
+def Value.toExpr (v : Value) : Expr :=
+  let vExpr := mkRawNatLit v.value
+  mkApp2 v.ofNatFn vExpr (mkApp2 (mkConst ``Fin.ofNatInst) (Lean.toExpr (v.size - 1)) vExpr)
+
+@[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 v₁ ← fromExpr? e.appFn!.appArg! | return none
+  let some v₂ ← fromExpr? e.appArg! | return none
+  unless v₁.size == v₂.size do return none
+  let v := { v₁ with value := op v₁.value v₂.value % v₁.size }
+  return some (.done { expr := v.toExpr })
+
+@[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 v₁ ← fromExpr? e.appFn!.appArg! | return none
+  let some v₂ ← fromExpr? e.appArg! | return none
+  let d ← mkDecide e
+  if op v₁.value v₂.value 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))] })
+
+/-
+The following code assumes users did not override the `Fin n` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
+builtin_simproc reduceAdd ((_ + _ : Fin _)) := reduceBin ``HAdd.hAdd 6 (· + ·)
+builtin_simproc reduceMul ((_ * _ : Fin _)) := reduceBin ``HMul.hMul 6 (· * ·)
+builtin_simproc reduceSub ((_ - _ : Fin _)) := reduceBin ``HSub.hSub 6 (· - ·)
+builtin_simproc reduceDiv ((_ / _ : Fin _)) := reduceBin ``HDiv.hDiv 6 (· / ·)
+builtin_simproc reduceMod ((_ % _ : Fin _)) := reduceBin ``HMod.hMod 6 (· % ·)
+
+builtin_simproc reduceLT  (( _ : Fin _) < _)  := reduceBinPred ``LT.lt 4 (. < .)
+builtin_simproc reduceLE  (( _ : Fin _) ≤ _)  := reduceBinPred ``LE.le 4 (. ≤ .)
+builtin_simproc reduceGT  (( _ : Fin _) > _)  := reduceBinPred ``GT.gt 4 (. > .)
+builtin_simproc reduceGE  (( _ : Fin _) ≥ _)  := reduceBinPred ``GE.ge 4 (. ≥ .)
+
+end Fin

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

@@ -13,6 +13,11 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   let some n ← evalNat e |>.run | return none
   return some n
 
+@[inline] def reduceUnary (declName : Name) (arity : Nat) (op : Nat → Nat) (e : Expr) : SimpM (Option Step) := do
+  unless e.isAppOfArity declName arity do return none
+  let some n ← fromExpr? e.appArg! | return none
+  return some (.done { expr := mkNatLit (op 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
@@ -29,6 +34,13 @@ def fromExpr? (e : Expr) : SimpM (Option Nat) := do
   else
     return some (.done { expr := mkConst ``False, proof? := mkAppN (mkConst ``eq_false_of_decide) #[e, d.appArg!, (← mkEqRefl (mkConst ``false))] })
 
+builtin_simproc reduceSucc (Nat.succ _) := reduceUnary ``Nat.succ 1 (· + 1)
+
+/-
+The following code assumes users did not override the `Nat` instances for the arithmetic operators.
+If they do, they must disable the following `simprocs`.
+-/
+
 builtin_simproc reduceAdd ((_ + _ : Nat)) := reduceBin ``HAdd.hAdd 6 (· + ·)
 builtin_simproc reduceMul ((_ * _ : Nat)) := reduceBin ``HMul.hMul 6 (· * ·)
 builtin_simproc reduceSub ((_ - _ : Nat)) := reduceBin ``HSub.hSub 6 (· - ·)

tests/lean/simprocEval2.lean

@@ -0,0 +1,53 @@
+def foo (_ : Nat) : Fin 32 := 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 - 3 = 17 % 10 := by
+  simp
+  trace_state
+  simp [foo]
+
+example : foo x = (3+2)*2 := by
+  simp
+  trace_state
+  rw [foo]
+
+def boo (_ : Nat) := True
+
+example : boo x ↔ (2 : Fin 8) < 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (3 : Fin 8) > 2 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (2 : Fin 8) ≤ 3 := by
+  simp
+  trace_state
+  trivial
+
+example : boo x ↔ (3 : Fin 8) ≥ 2 := by
+  simp
+  trace_state
+  trivial

tests/lean/simprocEval2.lean.expected.out

@@ -0,0 +1,20 @@
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ foo x - 3 = 7
+x : Nat
+⊢ foo x = 10
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x
+x : Nat
+⊢ boo x