max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

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

Browse source 
This came up in the context of simplifying proof states for
https://github.com/leanprover/LNSym.
This commit is contained in:
Siddharth 2024-07-31 12:26:05 -05:00 • committed by GitHub
parent d5a8c9647f
commit f869902a4b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 18 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/Nat.lean
View file

@ -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 (. < .)

8
tests/lean/run/simprocNat.lean
View file

@ -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