diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean index 2a1a4163fb..f71e702283 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 a442c9a9ce..9e6606d159 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