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

chore: rename BitVec.ofNatLt -> BitVec.ofNatLT (#7064)

Browse source 
This PR renames `BitVec.ofNatLt` to `BitVec.ofNatLT` and sets up
deprecations for the old name.
This commit is contained in:
Markus Himmel 2025-02-13 13:52:31 +01:00 • committed by GitHub
parent 4a900cc65c
commit b38da34db2
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
7 changed files with 51 additions and 36 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/Init/Data/BitVec/Basic.lean
View file

@ -25,6 +25,10 @@ set_option linter.missingDocs true
namespace BitVec
@[inline, deprecated BitVec.ofNatLT (since := "2025-02-13"), inherit_doc BitVec.ofNatLT]
protected def ofNatLt {n : Nat} (i : Nat) (p : i < 2 ^ n) : BitVec n :=
BitVec.ofNatLT i p
section Nat
instance natCastInst : NatCast (BitVec w) := ⟨BitVec.ofNat w⟩
@ -55,12 +59,12 @@ end subsingleton
section zero_allOnes
/-- Return a bitvector `0` of size `n`. This is the bitvector with all zero bits. -/
protected def zero (n : Nat) : BitVec n := .ofNatLt 0 (Nat.two_pow_pos n)
protected def zero (n : Nat) : BitVec n := .ofNatLT 0 (Nat.two_pow_pos n)
instance : Inhabited (BitVec n) where default := .zero n
/-- Bit vector of size `n` where all bits are `1`s -/
def allOnes (n : Nat) : BitVec n :=
.ofNatLt (2^n - 1) (Nat.le_of_eq (Nat.sub_add_cancel (Nat.two_pow_pos n)))
.ofNatLT (2^n - 1) (Nat.le_of_eq (Nat.sub_add_cancel (Nat.two_pow_pos n)))
end zero_allOnes
@ -138,7 +142,7 @@ protected def toInt (x : BitVec n) : Int :=
(x.toNat : Int) - (2^n : Nat)
/-- The `BitVec` with value `(2^n + (i mod 2^n)) mod 2^n`. -/
protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLt (i % (Int.ofNat (2^n))).toNat (by
protected def ofInt (n : Nat) (i : Int) : BitVec n := .ofNatLT (i % (Int.ofNat (2^n))).toNat (by
apply (Int.toNat_lt _).mpr
· apply Int.emod_lt_of_pos
exact Int.ofNat_pos.mpr (Nat.two_pow_pos _)
@ -167,12 +171,12 @@ recommended_spelling "one" for "1#n" in [BitVec.ofNat, «term__#__»]
| `($(_) $n $i:num) => `($i:num#$n)
| _ => throw ()
/-- Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLt i lt`. -/
/-- Notation for bit vector literals without truncation. `i#'lt` is a shorthand for `BitVec.ofNatLT i lt`. -/
scoped syntax:max term:max noWs "#'" noWs term:max : term
macro_rules | `($i#'$p) => `(BitVec.ofNatLt $i $p)
macro_rules | `($i#'$p) => `(BitVec.ofNatLT $i $p)
/-- Unexpander for bit vector literals without truncation. -/
@[app_unexpander BitVec.ofNatLt] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
@[app_unexpander BitVec.ofNatLT] def unexpandBitVecOfNatLt : Lean.PrettyPrinter.Unexpander
| `($(_) $i $p) => `($i#'$p)
| _ => throw ()
@ -356,7 +360,7 @@ end relations
section cast
/-- `cast eq x` embeds `x` into an equal `BitVec` type. -/
@[inline] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLt x.toNat (eq ▸ x.isLt)
@[inline] protected def cast (eq : n = m) (x : BitVec n) : BitVec m := .ofNatLT x.toNat (eq ▸ x.isLt)
@[simp] theorem cast_ofNat {n m : Nat} (h : n = m) (x : Nat) :
(BitVec.ofNat n x).cast h = BitVec.ofNat m x := by

27
src/Init/Data/BitVec/Lemmas.lean
View file

@ -274,16 +274,27 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
@[simp, bitvec_to_nat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
@[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@[simp] theorem toNat_ofNatLT (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@[simp] theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
@[deprecated toNat_ofNatLT (since := "2025-02-13")]
theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@[simp] theorem getLsbD_ofNatLT {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
getLsbD (x#'lt) i = x.testBit i := by
simp [getLsbD, BitVec.ofNatLt]
simp [getLsbD, BitVec.ofNatLT]
@[simp] theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
@[deprecated getLsbD_ofNatLT (since := "2025-02-13")]
theorem getLsbD_ofNatLt {n : Nat} (x : Nat) (lt : x < 2^n) (i : Nat) :
getLsbD (x#'lt) i = x.testBit i := getLsbD_ofNatLT x lt i
@[simp] theorem getMsbD_ofNatLT {n x i : Nat} (h : x < 2^n) :
getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := by
simp [getMsbD, getLsbD]
@[deprecated getMsbD_ofNatLT (since := "2025-02-13")]
theorem getMsbD_ofNatLt {n x i : Nat} (h : x < 2^n) :
getMsbD (x#'h) i = (decide (i < n) && x.testBit (n - 1 - i)) := getMsbD_ofNatLT h
@[simp, bitvec_to_nat] theorem toNat_ofNat (x w : Nat) : (BitVec.ofNat w x).toNat = x % 2^w := by
simp [BitVec.toNat, BitVec.ofNat, Fin.ofNat']
@ -1217,7 +1228,7 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
@[simp] theorem ofInt_negSucc_eq_not_ofNat {w n : Nat} :
BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLt, toNat_not,
simp only [BitVec.ofInt, Int.toNat, Int.ofNat_eq_coe, toNat_eq, toNat_ofNatLT, toNat_not,
toNat_ofNat]
cases h : Int.negSucc n % ((2 ^ w : Nat) : Int)
case ofNat =>
@ -1418,7 +1429,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
apply eq_of_toNat_eq
rw [shiftLeftZeroExtend, setWidth]
split
· simp only [toNat_ofNatLt, toNat_shiftLeft, toNat_setWidth']
· simp only [toNat_ofNatLT, toNat_shiftLeft, toNat_setWidth']
rw [Nat.mod_eq_of_lt]
rw [Nat.shiftLeft_eq, Nat.pow_add]
exact Nat.mul_lt_mul_of_pos_right x.isLt (Nat.two_pow_pos _)
@ -2901,7 +2912,7 @@ protected theorem ne_of_lt {x y : BitVec n} : x < y → x ≠ y := by
apply Nat.ne_of_lt
protected theorem umod_lt (x : BitVec n) {y : BitVec n} : 0 < y → x % y < y := by
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLt]
simp only [ofNat_eq_ofNat, lt_def, toNat_ofNat, Nat.zero_mod, umod, toNat_ofNatLT]
apply Nat.mod_lt
theorem not_lt_iff_le {x y : BitVec w} : (¬ x < y) ↔ y ≤ x := by
@ -3243,7 +3254,7 @@ theorem toNat_smod {x y : BitVec w} : (x.smod y).toNat =
by_cases h : x.msb <;> by_cases h' : y.msb
<;> by_cases h'' : (-x).umod y = 0#w <;> by_cases h''' : x.umod (-y) = 0#w
<;> simp only [h, h', h'', h''']
<;> simp only [umod, toNat_eq, toNat_ofNatLt, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp only [umod, toNat_eq, toNat_ofNatLT, toNat_ofNat, Nat.zero_mod] at h'' h'''
<;> simp [h'', h''']
@[simp]

6
src/Init/Data/UInt/BasicAux.lean
View file

@ -51,7 +51,7 @@ 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⟩
def UInt32.ofNat' (n : Nat) (h : n < UInt32.size) : UInt32 := ⟨BitVec.ofNatLT n h⟩
/--
Converts the given natural number to `UInt32`, but returns `2^32 - 1` for natural numbers `>= 2^32`.
-/
@ -74,12 +74,12 @@ 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',
simp only [(· < ·), BitVec.toNat, ofNat', 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',
simp only [(· < ·), BitVec.toNat, ofNat', BitVec.ofNatLT, ofNat, BitVec.ofNat, Fin.ofNat',
Nat.mod_eq_of_lt h2, imp_self]
/-- Converts a `UInt64` into the corresponding `Fin UInt64.size`. -/

2
src/Init/Data/UInt/Lemmas.lean
View file

@ -29,7 +29,7 @@ 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_ofNatCore {n : Nat} {h : n < size} : (ofNatCore 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")]

26
src/Init/Prelude.lean
View file

@ -1904,7 +1904,7 @@ instance : DecidableEq (BitVec n) := BitVec.decEq
/-- The `BitVec` with value `i`, given a proof that `i < 2^n`. -/
@[match_pattern]
protected def BitVec.ofNatLt {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
protected def BitVec.ofNatLT {n : Nat} (i : Nat) (p : LT.lt i (hPow 2 n)) : BitVec n where
toFin := ⟨i, p⟩
/-- Given a bitvector `x`, return the underlying `Nat`. This is O(1) because `BitVec` is a
@ -1945,7 +1945,7 @@ 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
toBitVec := BitVec.ofNatLT n h
/--
Pack a `Nat` less than `2^8` into a `UInt8`.
@ -1953,7 +1953,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint8_of_nat"]
def UInt8.ofNatLT (n : @& Nat) (h : LT.lt n UInt8.size) : UInt8 where
toBitVec := BitVec.ofNatLt n h
toBitVec := BitVec.ofNatLT n h
set_option bootstrap.genMatcherCode false in
/--
@ -1999,7 +1999,7 @@ 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
toBitVec := BitVec.ofNatLT n h
/--
Pack a `Nat` less than `2^16` into a `UInt16`.
@ -2007,7 +2007,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint16_of_nat"]
def UInt16.ofNatLT (n : @& Nat) (h : LT.lt n UInt16.size) : UInt16 where
toBitVec := BitVec.ofNatLt n h
toBitVec := BitVec.ofNatLT n h
set_option bootstrap.genMatcherCode false in
/--
@ -2053,7 +2053,7 @@ 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
toBitVec := BitVec.ofNatLT n h
/--
Pack a `Nat` less than `2^32` into a `UInt32`.
@ -2061,7 +2061,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def UInt32.ofNatLT (n : @& Nat) (h : LT.lt n UInt32.size) : UInt32 where
toBitVec := BitVec.ofNatLt n h
toBitVec := BitVec.ofNatLT n h
/--
Unpack a `UInt32` as a `Nat`.
@ -2138,7 +2138,7 @@ 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
toBitVec := BitVec.ofNatLT n h
/--
Pack a `Nat` less than `2^64` into a `UInt64`.
@ -2146,7 +2146,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint64_of_nat"]
def UInt64.ofNatLT (n : @& Nat) (h : LT.lt n UInt64.size) : UInt64 where
toBitVec := BitVec.ofNatLt n h
toBitVec := BitVec.ofNatLT n h
set_option bootstrap.genMatcherCode false in
/--
@ -2208,7 +2208,7 @@ 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
toBitVec := BitVec.ofNatLT n h
/--
Pack a `Nat` less than `USize.size` into a `USize`.
@ -2216,7 +2216,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_usize_of_nat"]
def USize.ofNatLT (n : @& Nat) (h : LT.lt n USize.size) : USize where
toBitVec := BitVec.ofNatLt n h
toBitVec := BitVec.ofNatLT n h
set_option bootstrap.genMatcherCode false in
/--
@ -2269,7 +2269,7 @@ This function is overridden with a native implementation.
-/
@[extern "lean_uint32_of_nat"]
def Char.ofNatAux (n : @& Nat) (h : n.isValidChar) : Char :=
{ val := ⟨BitVec.ofNatLt n (isValidChar_UInt32 h)⟩, valid := h }
{ val := ⟨BitVec.ofNatLT n (isValidChar_UInt32 h)⟩, valid := h }
/--
Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scalar value,
@ -2279,7 +2279,7 @@ Convert a `Nat` into a `Char`. If the `Nat` does not encode a valid unicode scal
def Char.ofNat (n : Nat) : Char :=
dite (n.isValidChar)
(fun h => Char.ofNatAux n h)
(fun _ => { val := ⟨BitVec.ofNatLt 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
(fun _ => { val := ⟨BitVec.ofNatLT 0 (of_decide_eq_true rfl)⟩, valid := Or.inl (of_decide_eq_true rfl) })
theorem Char.eq_of_val_eq : ∀ {c d : Char}, Eq c.val d.val → Eq c d
| ⟨_, _⟩, ⟨_, _⟩, rfl => rfl

4
src/Lean/Meta/LitValues.lean
View file

@ -74,7 +74,7 @@ def getFinValue? (e : Expr) : MetaM (Option ((n : Nat) × Fin n)) := OptionT.run
Return `some ⟨n, v⟩` if `e` is:
- an `OfNat.ofNat` application
- a `BitVec.ofNat` application
- a `BitVec.ofNatLt` application
- a `BitVec.ofNatLT` application
that encode a `BitVec n` with value `v`.
-/
def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := OptionT.run do
@ -83,7 +83,7 @@ def getBitVecValue? (e : Expr) : MetaM (Option ((n : Nat) × BitVec n)) := Optio
let n ← getNatValue? nExpr
let v ← getNatValue? vExpr
return ⟨n, BitVec.ofNat n v⟩
| BitVec.ofNatLt nExpr vExpr _ =>
| BitVec.ofNatLT nExpr vExpr _ =>
let n ← getNatValue? nExpr
let v ← getNatValue? vExpr
return ⟨n, BitVec.ofNat n v⟩

4
src/Std/Tactic/BVDecide/Normalize/BitVec.lean
View file

@ -57,8 +57,8 @@ theorem BitVec.sle_eq_ult (x y : BitVec w) :
attribute [bv_normalize] BitVec.ofNat_eq_ofNat
@[bv_normalize]
theorem BitVec.ofNatLt_reduce (n : Nat) (h) : BitVec.ofNatLt n h = BitVec.ofNat w n := by
simp [BitVec.ofNatLt, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h]
theorem BitVec.ofNatLT_reduce (n : Nat) (h) : BitVec.ofNatLT n h = BitVec.ofNat w n := by
simp [BitVec.ofNatLT, BitVec.ofNat, Fin.ofNat', Nat.mod_eq_of_lt h]
@[bv_normalize]
theorem BitVec.ofBool_eq_if (b : Bool) : BitVec.ofBool b = bif b then 1#1 else 0#1 := by