From 27cc0c80399f9f5ecebfdff65169d217a3045eea Mon Sep 17 00:00:00 2001 From: Mac Malone Date: Fri, 29 Nov 2024 03:24:40 -0500 Subject: [PATCH] feat: `USize.reduceToNat` (#6190) This PR adds the builtin simproc `USize.reduceToNat` which reduces the `USize.toNat` operation on literals less than `UInt32.size` (i.e., `4294967296`). --- .../Tactic/Simp/BuiltinSimprocs/UInt.lean | 20 ++++++++++++++++--- tests/lean/run/simprocUInt.lean | 7 +++++++ 2 files changed, 24 insertions(+), 3 deletions(-) create mode 100644 tests/lean/run/simprocUInt.lean diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean index 07e8b9df1b..db9dff719b 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -84,8 +84,22 @@ declare_uint_simprocs UInt8 declare_uint_simprocs UInt16 declare_uint_simprocs UInt32 declare_uint_simprocs UInt64 + /- -We disabled the simprocs for USize since the result of most operations depend on an opaque value: `System.Platform.numBits`. -We could reduce some cases using the fact that this opaque value is `32` or `64`, but it is unclear whether it would be useful in practice. +We do not use the normal simprocs for `USize` since the result of most operations depend on an opaque value: `System.Platform.numBits`. +However, we do reduce natural literals using the fact this opaque value is at least `32`. -/ --- declare_uint_simprocs USize +namespace USize + +def fromExpr (e : Expr) : SimpM (Option USize) := do + let some (n, _) ← getOfNatValue? e ``USize | return none + return USize.ofNat n + +builtin_simproc [simp, seval] reduceToNat (USize.toNat _) := fun e => do + let_expr USize.toNat e ← e | return .continue + let some (n, _) ← getOfNatValue? e ``USize | return .continue + unless n < UInt32.size do return .continue + let e := toExpr n + let p ← mkDecideProof (← mkLT e (mkNatLit UInt32.size)) + let p := mkApp2 (mkConst ``USize.toNat_ofNat_of_lt_32) e p + return .done { expr := e, proof? := p } diff --git a/tests/lean/run/simprocUInt.lean b/tests/lean/run/simprocUInt.lean new file mode 100644 index 0000000000..98ae68359f --- /dev/null +++ b/tests/lean/run/simprocUInt.lean @@ -0,0 +1,7 @@ +variable (x : USize) + +/- USize.toNat -/ + +#check_simp USize.toNat 4294967296 !~> +#check_simp USize.toNat 4294967295 ~> 4294967295 +#check_simp USize.toNat (x &&& 1) ~> x.toNat % 2