From 47548aa171f02cf0b61fc1eb6bcaee82bb50d060 Mon Sep 17 00:00:00 2001 From: Markus Himmel Date: Fri, 14 Feb 2025 07:58:15 +0100 Subject: [PATCH] chore: rename `UIntX.ofNatCore`, `UIntX.ofNat'` -> `UIntX.ofNatLT` (#7071) This PR unifies the existing functions `UIntX.ofNatCore` and `UIntX.ofNat'` under a new name, `UIntX.ofNatLT`. --- src/Init/Data/Char/Basic.lean | 6 +- src/Init/Data/Repr.lean | 2 +- src/Init/Data/UInt/Basic.lean | 19 +++++- src/Init/Data/UInt/BasicAux.lean | 28 +++++---- src/Init/Data/UInt/Lemmas.lean | 5 +- src/Init/Prelude.lean | 60 ++++--------------- .../Tactic/Simp/BuiltinSimprocs/UInt.lean | 7 --- tests/lean/simprocEval3.lean | 5 -- tests/lean/simprocEval3.lean.expected.out | 3 - 9 files changed, 53 insertions(+), 82 deletions(-) diff --git a/src/Init/Data/Char/Basic.lean b/src/Init/Data/Char/Basic.lean index 93f997f9ef..7cddc85570 100644 --- a/src/Init/Data/Char/Basic.lean +++ b/src/Init/Data/Char/Basic.lean @@ -40,12 +40,12 @@ theorem isValidUInt32 (n : Nat) (h : isValidCharNat n) : n < UInt32.size := by apply Nat.lt_trans h₂ decide -theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNat' n (isValidUInt32 n h)) := +theorem isValidChar_of_isValidCharNat (n : Nat) (h : isValidCharNat n) : isValidChar (UInt32.ofNatLT n (isValidUInt32 n h)) := match h with | Or.inl h => - Or.inl (UInt32.ofNat'_lt_of_lt _ (by decide) h) + Or.inl (UInt32.ofNatLT_lt_of_lt _ (by decide) h) | Or.inr ⟨h₁, h₂⟩ => - Or.inr ⟨UInt32.lt_ofNat'_of_lt _ (by decide) h₁, UInt32.ofNat'_lt_of_lt _ (by decide) h₂⟩ + Or.inr ⟨UInt32.lt_ofNatLT_of_lt _ (by decide) h₁, UInt32.ofNatLT_lt_of_lt _ (by decide) h₂⟩ theorem isValidChar_zero : isValidChar 0 := Or.inl (by decide) diff --git a/src/Init/Data/Repr.lean b/src/Init/Data/Repr.lean index 09920c9072..53f8aa098b 100644 --- a/src/Init/Data/Repr.lean +++ b/src/Init/Data/Repr.lean @@ -163,7 +163,7 @@ private def reprArray : Array String := Id.run do private def reprFast (n : Nat) : String := if h : n < 128 then Nat.reprArray.get n h else - if h : n < USize.size then (USize.ofNatCore n h).repr + if h : n < USize.size then (USize.ofNatLT n h).repr else (toDigits 10 n).asString @[implemented_by reprFast] diff --git a/src/Init/Data/UInt/Basic.lean b/src/Init/Data/UInt/Basic.lean index c9e9f7e993..984dcc6cf4 100644 --- a/src/Init/Data/UInt/Basic.lean +++ b/src/Init/Data/UInt/Basic.lean @@ -14,6 +14,9 @@ open Nat @[deprecated UInt8.ofBitVec (since := "2025-02-12"), inherit_doc UInt8.ofBitVec] def UInt8.mk (bitVec : BitVec 8) : UInt8 := UInt8.ofBitVec bitVec +@[inline, deprecated UInt8.ofNatLT (since := "2025-02-13"), inherit_doc UInt8.ofNatLT] +def UInt8.ofNatCore (n : Nat) (h : n < UInt8.size) : UInt8 := + UInt8.ofNatLT n h @[extern "lean_uint8_add"] def UInt8.add (a b : UInt8) : UInt8 := ⟨a.toBitVec + b.toBitVec⟩ @@ -83,6 +86,9 @@ instance : Min UInt8 := minOfLe @[deprecated UInt16.ofBitVec (since := "2025-02-12"), inherit_doc UInt16.ofBitVec] def UInt16.mk (bitVec : BitVec 16) : UInt16 := UInt16.ofBitVec bitVec +@[inline, deprecated UInt16.ofNatLT (since := "2025-02-13"), inherit_doc UInt16.ofNatLT] +def UInt16.ofNatCore (n : Nat) (h : n < UInt16.size) : UInt16 := + UInt16.ofNatLT n h @[extern "lean_uint16_add"] def UInt16.add (a b : UInt16) : UInt16 := ⟨a.toBitVec + b.toBitVec⟩ @@ -154,6 +160,9 @@ instance : Min UInt16 := minOfLe @[deprecated UInt32.ofBitVec (since := "2025-02-12"), inherit_doc UInt32.ofBitVec] def UInt32.mk (bitVec : BitVec 32) : UInt32 := UInt32.ofBitVec bitVec +@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT] +def UInt32.ofNatCore (n : Nat) (h : n < UInt32.size) : UInt32 := + UInt32.ofNatLT n h @[extern "lean_uint32_add"] def UInt32.add (a b : UInt32) : UInt32 := ⟨a.toBitVec + b.toBitVec⟩ @@ -210,6 +219,9 @@ def Bool.toUInt32 (b : Bool) : UInt32 := if b then 1 else 0 @[deprecated UInt64.ofBitVec (since := "2025-02-12"), inherit_doc UInt64.ofBitVec] def UInt64.mk (bitVec : BitVec 64) : UInt64 := UInt64.ofBitVec bitVec +@[inline, deprecated UInt64.ofNatLT (since := "2025-02-13"), inherit_doc UInt64.ofNatLT] +def UInt64.ofNatCore (n : Nat) (h : n < UInt64.size) : UInt64 := + UInt64.ofNatLT n h @[extern "lean_uint64_add"] def UInt64.add (a b : UInt64) : UInt64 := ⟨a.toBitVec + b.toBitVec⟩ @@ -279,6 +291,9 @@ instance : Min UInt64 := minOfLe @[deprecated USize.ofBitVec (since := "2025-02-12"), inherit_doc USize.ofBitVec] def USize.mk (bitVec : BitVec System.Platform.numBits) : USize := USize.ofBitVec bitVec +@[inline, deprecated USize.ofNatLT (since := "2025-02-13"), inherit_doc USize.ofNatLT] +def USize.ofNatCore (n : Nat) (h : n < USize.size) : USize := + USize.ofNatLT n h theorem usize_size_le : USize.size ≤ 18446744073709551616 := by cases usize_size_eq <;> next h => rw [h]; decide @@ -311,7 +326,7 @@ This function is overridden with a native implementation. -/ @[extern "lean_usize_of_nat"] def USize.ofNat32 (n : @& Nat) (h : n < 4294967296) : USize := - USize.ofNatCore n (Nat.lt_of_lt_of_le h le_usize_size) + USize.ofNatLT n (Nat.lt_of_lt_of_le h le_usize_size) @[extern "lean_uint8_to_usize"] def UInt8.toUSize (a : UInt8) : USize := USize.ofNat32 a.toBitVec.toNat (Nat.lt_trans a.toBitVec.isLt (by decide)) @@ -336,7 +351,7 @@ This function is overridden with a native implementation. -/ @[extern "lean_usize_to_uint64"] def USize.toUInt64 (a : USize) : UInt64 := - UInt64.ofNatCore a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le) + UInt64.ofNatLT a.toBitVec.toNat (Nat.lt_of_lt_of_le a.toBitVec.isLt usize_size_le) instance : Mul USize := ⟨USize.mul⟩ instance : Mod USize := ⟨USize.mod⟩ diff --git a/src/Init/Data/UInt/BasicAux.lean b/src/Init/Data/UInt/BasicAux.lean index eedde3b8f7..f40738b033 100644 --- a/src/Init/Data/UInt/BasicAux.lean +++ b/src/Init/Data/UInt/BasicAux.lean @@ -50,16 +50,16 @@ def UInt32.toFin (x : UInt32) : Fin UInt32.size := x.toBitVec.toFin def UInt32.val (x : UInt32) : Fin UInt32.size := x.toFin @[extern "lean_uint32_of_nat"] def UInt32.ofNat (n : @& Nat) : UInt32 := ⟨BitVec.ofNat 32 n⟩ -@[extern "lean_uint32_of_nat"] -def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLT n h⟩ +@[inline, deprecated UInt32.ofNatLT (since := "2025-02-13"), inherit_doc UInt32.ofNatLT] +def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := UInt32.ofNatLT n h /-- Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`. -/ def UInt32.ofNatTruncate (n : Nat) : UInt32 := if h : n < UInt32.size then - UInt32.ofNat' n h + UInt32.ofNatLT n h else - UInt32.ofNat' (UInt32.size - 1) (by decide) + UInt32.ofNatLT (UInt32.size - 1) (by decide) abbrev Nat.toUInt32 := UInt32.ofNat @[extern "lean_uint32_to_uint8"] def UInt32.toUInt8 (a : UInt32) : UInt8 := a.toNat.toUInt8 @@ -72,16 +72,24 @@ def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBit instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩ -theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : - n < m → UInt32.ofNat' n h1 < UInt32.ofNat m := by - simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat', +theorem UInt32.ofNatLT_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : + n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := by + simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h2, imp_self] -theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : - m < n → UInt32.ofNat m < UInt32.ofNat' n h1 := by - simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat', +@[deprecated UInt32.ofNatLT_lt_of_lt (since := "2025-02-13")] +theorem UInt32.ofNat'_lt_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : + n < m → UInt32.ofNatLT n h1 < UInt32.ofNat m := UInt32.ofNatLT_lt_of_lt h1 h2 + +theorem UInt32.lt_ofNatLT_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : + m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := by + simp only [(· < ·), BitVec.toNat, ofNatLT, BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h2, imp_self] +@[deprecated UInt32.lt_ofNatLT_of_lt (since := "2025-02-13")] +theorem UInt32.lt_ofNat'_of_lt {n m : Nat} (h1 : n < UInt32.size) (h2 : m < UInt32.size) : + m < n → UInt32.ofNat m < UInt32.ofNatLT n h1 := UInt32.lt_ofNatLT_of_lt h1 h2 + /-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/ def UInt64.toFin (x : UInt64) : Fin UInt64.size := x.toBitVec.toFin @[deprecated UInt64.toFin (since := "2025-02-12"), inherit_doc UInt64.toFin] diff --git a/src/Init/Data/UInt/Lemmas.lean b/src/Init/Data/UInt/Lemmas.lean index 9761d18583..41a46408f8 100644 --- a/src/Init/Data/UInt/Lemmas.lean +++ b/src/Init/Data/UInt/Lemmas.lean @@ -29,7 +29,10 @@ macro "declare_uint_theorems" typeName:ident bits:term:arg : command => do @[simp] theorem toNat_ofNat {n : Nat} : (ofNat n).toNat = n % 2 ^ $bits := BitVec.toNat_ofNat .. - @[simp] theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatCore n h).toNat = n := BitVec.toNat_ofNatLT .. + @[simp] theorem toNat_ofNatLT {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT .. + + @[deprecated toNat_ofNatLT (since := "2025-02-13")] + theorem toNat_ofNatCore {n : Nat} {h : n < size} : (ofNatLT n h).toNat = n := BitVec.toNat_ofNatLT .. @[simp] theorem toFin_val_eq_toNat (x : $typeName) : x.toFin.val = x.toNat := rfl @[deprecated toFin_val_eq_toNat (since := "2025-02-12")] diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index 653e740e5a..2ddb0efa4b 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1939,14 +1939,6 @@ structure UInt8 where attribute [extern "lean_uint8_of_nat_mk"] UInt8.ofBitVec attribute [extern "lean_uint8_to_nat"] UInt8.toBitVec -/-- -Pack a `Nat` less than `2^8` into a `UInt8`. -This function is overridden with a native implementation. --/ -@[extern "lean_uint8_of_nat"] -def UInt8.ofNatCore (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where - toBitVec := BitVec.ofNatLT n h - /-- Pack a `Nat` less than `2^8` into a `UInt8`. This function is overridden with a native implementation. @@ -1971,7 +1963,7 @@ def UInt8.decEq (a b : UInt8) : Decidable (Eq a b) := instance : DecidableEq UInt8 := UInt8.decEq instance : Inhabited UInt8 where - default := UInt8.ofNatCore 0 (of_decide_eq_true rfl) + default := UInt8.ofNatLT 0 (of_decide_eq_true rfl) /-- The size of type `UInt16`, that is, `2^16 = 65536`. -/ abbrev UInt16.size : Nat := 65536 @@ -1993,14 +1985,6 @@ structure UInt16 where attribute [extern "lean_uint16_of_nat_mk"] UInt16.ofBitVec attribute [extern "lean_uint16_to_nat"] UInt16.toBitVec -/-- -Pack a `Nat` less than `2^16` into a `UInt16`. -This function is overridden with a native implementation. --/ -@[extern "lean_uint16_of_nat"] -def UInt16.ofNatCore (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where - toBitVec := BitVec.ofNatLT n h - /-- Pack a `Nat` less than `2^16` into a `UInt16`. This function is overridden with a native implementation. @@ -2025,7 +2009,7 @@ def UInt16.decEq (a b : UInt16) : Decidable (Eq a b) := instance : DecidableEq UInt16 := UInt16.decEq instance : Inhabited UInt16 where - default := UInt16.ofNatCore 0 (of_decide_eq_true rfl) + default := UInt16.ofNatLT 0 (of_decide_eq_true rfl) /-- The size of type `UInt32`, that is, `2^32 = 4294967296`. -/ abbrev UInt32.size : Nat := 4294967296 @@ -2047,14 +2031,6 @@ structure UInt32 where attribute [extern "lean_uint32_of_nat_mk"] UInt32.ofBitVec attribute [extern "lean_uint32_to_nat"] UInt32.toBitVec -/-- -Pack a `Nat` less than `2^32` into a `UInt32`. -This function is overridden with a native implementation. --/ -@[extern "lean_uint32_of_nat"] -def UInt32.ofNatCore (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where - toBitVec := BitVec.ofNatLT n h - /-- Pack a `Nat` less than `2^32` into a `UInt32`. This function is overridden with a native implementation. @@ -2084,7 +2060,7 @@ def UInt32.decEq (a b : UInt32) : Decidable (Eq a b) := instance : DecidableEq UInt32 := UInt32.decEq instance : Inhabited UInt32 where - default := UInt32.ofNatCore 0 (of_decide_eq_true rfl) + default := UInt32.ofNatLT 0 (of_decide_eq_true rfl) instance : LT UInt32 where lt a b := LT.lt a.toBitVec b.toBitVec @@ -2132,14 +2108,6 @@ structure UInt64 where attribute [extern "lean_uint64_of_nat_mk"] UInt64.ofBitVec attribute [extern "lean_uint64_to_nat"] UInt64.toBitVec -/-- -Pack a `Nat` less than `2^64` into a `UInt64`. -This function is overridden with a native implementation. --/ -@[extern "lean_uint64_of_nat"] -def UInt64.ofNatCore (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where - toBitVec := BitVec.ofNatLT n h - /-- Pack a `Nat` less than `2^64` into a `UInt64`. This function is overridden with a native implementation. @@ -2164,7 +2132,7 @@ def UInt64.decEq (a b : UInt64) : Decidable (Eq a b) := instance : DecidableEq UInt64 := UInt64.decEq instance : Inhabited UInt64 where - default := UInt64.ofNatCore 0 (of_decide_eq_true rfl) + default := UInt64.ofNatLT 0 (of_decide_eq_true rfl) /-- The size of type `USize`, that is, `2^System.Platform.numBits`. -/ abbrev USize.size : Nat := (hPow 2 System.Platform.numBits) @@ -2202,14 +2170,6 @@ structure USize where attribute [extern "lean_usize_of_nat_mk"] USize.ofBitVec attribute [extern "lean_usize_to_nat"] USize.toBitVec -/-- -Pack a `Nat` less than `USize.size` into a `USize`. -This function is overridden with a native implementation. --/ -@[extern "lean_usize_of_nat"] -def USize.ofNatCore (n : @& Nat) (h : LT.lt n USize.size) : USize where - toBitVec := BitVec.ofNatLT n h - /-- Pack a `Nat` less than `USize.size` into a `USize`. This function is overridden with a native implementation. @@ -2234,7 +2194,7 @@ def USize.decEq (a b : USize) : Decidable (Eq a b) := instance : DecidableEq USize := USize.decEq instance : Inhabited USize where - default := USize.ofNatCore 0 usize_size_pos + default := USize.ofNatLT 0 usize_size_pos /-- A `Nat` denotes a valid unicode codepoint if it is less than `0x110000`, and @@ -2302,9 +2262,9 @@ instance : DecidableEq Char := /-- Returns the number of bytes required to encode this `Char` in UTF-8. -/ def Char.utf8Size (c : Char) : Nat := let v := c.val - ite (LE.le v (UInt32.ofNatCore 0x7F (of_decide_eq_true rfl))) 1 - (ite (LE.le v (UInt32.ofNatCore 0x7FF (of_decide_eq_true rfl))) 2 - (ite (LE.le v (UInt32.ofNatCore 0xFFFF (of_decide_eq_true rfl))) 3 4)) + ite (LE.le v (UInt32.ofNatLT 0x7F (of_decide_eq_true rfl))) 1 + (ite (LE.le v (UInt32.ofNatLT 0x7FF (of_decide_eq_true rfl))) 2 + (ite (LE.le v (UInt32.ofNatLT 0xFFFF (of_decide_eq_true rfl))) 3 4)) /-- `Option α` is the type of values which are either `some a` for some `a : α`, @@ -3569,9 +3529,9 @@ with /-- A hash function for names, which is stored inside the name itself as a computed field. -/ @[computed_field] hash : Name → UInt64 - | .anonymous => .ofNatCore 1723 (of_decide_eq_true rfl) + | .anonymous => .ofNatLT 1723 (of_decide_eq_true rfl) | .str p s => mixHash p.hash s.hash - | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (of_decide_eq_true rfl))) + | .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatLT v h) (fun _ => UInt64.ofNatLT 17 (of_decide_eq_true rfl))) instance : Inhabited Name where default := Name.anonymous diff --git a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean index d4131e497c..f797cd6f8d 100644 --- a/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean +++ b/src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/UInt.lean @@ -11,7 +11,6 @@ open Lean Meta Simp macro "declare_uint_simprocs" typeName:ident : command => let ofNat := typeName.getId ++ `ofNat -let ofNatCore := mkIdent (typeName.getId ++ `ofNatCore) let ofNatLT := mkIdent (typeName.getId ++ `ofNatLT) let toNat := mkIdent (typeName.getId ++ `toNat) let fromExpr := mkIdent `fromExpr @@ -55,12 +54,6 @@ builtin_simproc [simp, seval] reduceNe (( _ : $typeName) ≠ _) := reduceBinPr builtin_dsimproc [simp, seval] reduceBEq (( _ : $typeName) == _) := reduceBoolPred ``BEq.beq 4 (. == .) builtin_dsimproc [simp, seval] reduceBNe (( _ : $typeName) != _) := reduceBoolPred ``bne 4 (. != .) -builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNatCore):ident ($ofNatCore _ _) := fun e => do - unless e.isAppOfArity $(quote ofNatCore.getId) 2 do return .continue - let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue - let value := $(mkIdent ofNat) value - return .done <| toExpr value - builtin_dsimproc [simp, seval] $(mkIdent `reduceOfNatLT):ident ($ofNatLT _ _) := fun e => do unless e.isAppOfArity $(quote ofNatLT.getId) 2 do return .continue let some value ← Nat.fromExpr? e.appFn!.appArg! | return .continue diff --git a/tests/lean/simprocEval3.lean b/tests/lean/simprocEval3.lean index 37db04f803..13998ef236 100644 --- a/tests/lean/simprocEval3.lean +++ b/tests/lean/simprocEval3.lean @@ -5,11 +5,6 @@ example (h : x = 8) : x = (8 : UInt32).toNat := by trace_state assumption -example (h : x = 8) : x = UInt32.ofNatCore 8 (by decide) := by - simp - trace_state - assumption - example (h : x = 8) : x = UInt32.ofNatLT 8 (by decide) := by simp trace_state diff --git a/tests/lean/simprocEval3.lean.expected.out b/tests/lean/simprocEval3.lean.expected.out index d10fc3ca82..3dd108b02a 100644 --- a/tests/lean/simprocEval3.lean.expected.out +++ b/tests/lean/simprocEval3.lean.expected.out @@ -4,9 +4,6 @@ h : x = 8 x : UInt32 h : x = 8 ⊢ x = 8 -x : UInt32 -h : x = 8 -⊢ x = 8 x : Nat ⊢ foo x = 10 x : Nat