feat: Nat simprocs for simplifying bit expressions (#4874)

This came up in the context of simplifying proof states for https://github.com/leanprover/LNSym.
leanprover · Jul 31, 2024 · f869902 · f869902
1 parent d5a8c96
commit f869902
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 0 deletions.
diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
@@ -60,6 +60,16 @@ builtin_dsimproc [simp, seval] reducePow ((_ ^ _ : Nat)) := fun e => do
   unless (← checkExponent m) do return .continue
   return .done <| toExpr (n ^ m)
 
+builtin_dsimproc [simp, seval] reduceAnd ((_ &&& _ : Nat)) := reduceBin ``HOr.hOr 6 (· &&& ·)
+builtin_dsimproc [simp, seval] reduceXor ((_ ^^^ _ : Nat)) := reduceBin ``HXor.hXor 6 (· ^^^ ·)
+builtin_dsimproc [simp, seval] reduceOr ((_ ||| _ : Nat)) := reduceBin ``HOr.hOr 6 (· ||| ·)
+
+builtin_dsimproc [simp, seval] reduceShiftLeft ((_ <<< _ : Nat)) :=
+  reduceBin ``HShiftLeft.hShiftLeft 6 (· <<< ·)
+
+builtin_dsimproc [simp, seval] reduceShiftRight ((_ >>> _ : Nat)) :=
+  reduceBin ``HShiftRight.hShiftRight 6 (· >>> ·)
+
 builtin_dsimproc [simp, seval] reduceGcd (gcd _ _)       := reduceBin ``gcd 2 gcd
 
 builtin_simproc [simp, seval] reduceLT  (( _ : Nat) < _)  := reduceBinPred ``LT.lt 4 (. < .)

diff --git a/tests/lean/run/simprocNat.lean b/tests/lean/run/simprocNat.lean
@@ -1,5 +1,13 @@
 variable (a b : Nat)
 
+/- bitwise operation tests -/
+
+#check_simp (3 : Nat) &&& (1 : Nat) ~> 1
+#check_simp (3 : Nat) ^^^ (1 : Nat) ~> 2
+#check_simp (2 : Nat) ||| (1 : Nat) ~> 3
+#check_simp (3 : Nat) <<< (2 : Nat) ~> 12
+#check_simp (3 : Nat) >>> (1 : Nat) ~> 1
+
 /- subtract diff tests -/
 
 #check_simp (1000 : Nat) - 400 ~> 600