From 5ff31fa7df216cf1e90feebec998dd223ca9ca9e Mon Sep 17 00:00:00 2001 From: Siddharth Bhat Date: Tue, 30 Jul 2024 16:58:23 -0500 Subject: [PATCH] feat: Nat simprocs for simplifying bit expressions This came up in the context of simplifying proof states for https://github.com/leanprover/LNSym. --- src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean | 10 ++++++++++ tests/lean/run/simprocNat.lean | 8 ++++++++ 2 files changed, 18 insertions(+) diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 2a1a4163fbe0..f71e70228345 100644 --- 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 index a442c9a9ceef..9e6606d1596a 100644 --- 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