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

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

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]

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⟩

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,15 +72,23 @@ def UInt16.toUInt32 (a : UInt16) : UInt32 := ⟨⟨a.toNat, Nat.lt_trans a.toBit
 
 instance UInt32.instOfNat : OfNat UInt32 n := ⟨UInt32.ofNat n⟩
 
+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]
+
+@[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.ofNat' n h1 < UInt32.ofNat m := by
-  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat',
+     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.ofNat' n h1  := by
-  simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat',
-    Nat.mod_eq_of_lt h2, imp_self]
+     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

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")]

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

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

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

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