feat: improvements to the floating-point API (#14481)

This PR improves the API surrounding `Float` / `Float.Model` / `Float32`
/ `Float32.Model` / `UnpackedFloat` in the following ways:
- The declarations `Float.nan` / `Float.inf` / `Float32.nan` /
`Float32.inf` and their corresponding models `Float.Model.nan` /
`Float.Model.inf` / `Float32.Model.nan` / `Float32.Model.inf` are added
(upstreamed from batteries, if you will).
- The abbreviations `Int.toFloat` and `Int.toFloat32` are added,
analogous to the existing `Nat.toFloat` and `Nat.toFloat32`.
- `Float.Model.Format` now requires `2 ≤ exponentBits` instead of just
`0 < exponentBits`; which is a necessary condition for `pack` and
`unpack` to behave correctly
- The definitions `Float.ofNat` / `Float.ofInt` / `Float32.ofNat` /
`Float32.ofInt` are now exposed.
- The type `Float.Model.UnpackedFloat.Sign` now has `deriving
DecidableEq` instead of just `deriving BEq`.
- The definitions for `unpackMantissa` / `unpackExponent` / `unpackSign`
now use `BitVec.extractLsb'` instead of `BitVec.extractLsb`

Author: Rob23oba

src/Init/Data/Float/Float.lean

@@ -48,6 +48,26 @@ deriving instance DecidableEq for Float
 instance : Nonempty Float :=
   ⟨⟨default⟩⟩
 
+/--
+The special floating-point value `NaN`, short for “not a number”. This value comes up as the result
+of erroneous computation like `0 / 0`.
+
+Comparing any value with `NaN` using `==`, `<`, `≤` results in `false`, including `nan == nan`
+and `nan ≤ nan`. However, comparing with `NaN` using propositional equality will result in `true`
+if and only if the other value is also `NaN`, which means that `nan = nan` is true.
+
+Note: While there are many bit patterns that represent a “not a number” value, they are all equal
+in the logical model of `Float`, that is, all floating-point values `f : Float` with `f.isNaN`
+are propositionally equal to `nan`.
+-/
+def Float.nan : Float := .ofModel .nan
+
+/--
+The special floating-point value `+Inf`, short for positive infinity, used as a result for
+overflowing computations like `1 / 0`.
+-/
+def Float.inf : Float := .ofModel .inf
+
 /--
 Adds two 64-bit floating-point numbers according to IEEE 754. Typically used via the `+` operator.
 
@@ -229,10 +249,12 @@ This function has a logical model in terms of `Float.Model`.
   fun a => a.toModel.toUSize
 
 /--
-Checks whether a floating point number is `NaN` (“not a number”) value.
+Checks whether a floating point number is a `NaN` (“not a number”) value.
 
 `NaN` values result from operations that might otherwise be errors, such as dividing zero by zero.
 
+This function returns `true` if and only if the input is propositionally equal to `Float.nan`.
+
 This function has a logical model in terms of `Float.Model`. It is compiled to the C operator `isnan`.
 -/
 @[extern "lean_float_isnan"] def Float.isNaN : Float → Bool :=

src/Init/Data/Float/Float32.lean

@@ -48,6 +48,26 @@ deriving instance DecidableEq for Float32
 instance : Nonempty Float32 :=
   ⟨⟨default⟩⟩
 
+/--
+The special floating-point value `NaN`, short for “not a number”. This value comes up as the result
+of erroneous computation like `0 / 0`.
+
+Comparing any value with `NaN` using `==`, `<`, `≤` results in `false`, including `nan == nan`
+and `nan ≤ nan`. However, comparing with `NaN` using propositional equality will result in `true`
+if and only if the other value is also `NaN`, which means that `nan = nan` is true.
+
+Note: While there are many bit patterns that represent a “not a number” value, they are all equal
+in the logical model of `Float32`, that is, all floating-point values `f : Float32` with `f.isNaN`
+are propositionally equal to `nan`.
+-/
+def Float32.nan : Float32 := .ofModel .nan
+
+/--
+The special floating-point value `+Inf`, short for positive infinity, used as a result for
+overflowing computations like `1 / 0`.
+-/
+def Float32.inf : Float32 := .ofModel .inf
+
 /--
 Adds two 32-bit floating-point numbers according to IEEE 754. Typically used via the `+` operator.
 
@@ -226,10 +246,12 @@ This function has a logical model in terms of `Float32.Model`.
   fun a => a.toModel.toUSize
 
 /--
-Checks whether a floating point number is `NaN` ("not a number") value.
+Checks whether a floating point number is a `NaN` ("not a number") value.
 
 `NaN` values result from operations that might otherwise be errors, such as dividing zero by zero.
 
+This function returns `true` if and only if the input is propositionally equal to `Float32.nan`.
+
 This function has a logical model in terms of `Float32.Model`. It is compiled to the C operator `isnan`.
 -/
 @[extern "lean_float32_isnan"] def Float32.isNaN : Float32 → Bool :=

src/Init/Data/Float/Model/Float.lean

@@ -53,6 +53,18 @@ def pack (f : UnpackedFloat) : Float.Model where
   toBits := UInt64.ofBitVec (UnpackedFloat.pack Format.binary64 f)
   valid := by simp
 
+/--
+The special `NaN` value.
+-/
+def nan : Float.Model :=
+  pack .notANumber
+
+/--
+The special `Inf` value.
+-/
+def inf : Float.Model :=
+  pack (.infinity .positive)
+
 /--
 Compute the sum of two `Float.Model`.
 -/

src/Init/Data/Float/Model/Float32.lean

@@ -56,6 +56,18 @@ def pack (f : UnpackedFloat) : Float32.Model where
   toBits := UInt32.ofBitVec (UnpackedFloat.pack Format.binary32 f)
   valid := by simp
 
+/--
+The special `NaN` value.
+-/
+def nan : Float32.Model :=
+  pack .notANumber
+
+/--
+The special `Inf` value.
+-/
+def inf : Float32.Model :=
+  pack (.infinity .positive)
+
 /--
 Compute the sum of two `Float32.Model`.
 -/

src/Init/Data/Float/Model/Format/Basic.lean

@@ -33,7 +33,7 @@ structure Format where
   hm : 0 < mantissaBitsWithoutImplicit := by decide
   /-- The number of bits in the exponent. -/
   exponentBits : Nat
-  he : 0 < exponentBits := by decide
+  he : 2 ≤ exponentBits := by decide
 
 namespace Format
 

src/Init/Data/Float/Model/Unpacked/Pack/Basic.lean

@@ -66,21 +66,21 @@ will be missing the implicit bit.
 -/
 def unpackMantissa {spec : Format} (b : BitVec spec.numBits) :
     BitVec spec.mantissaBitsWithoutImplicit :=
-  b.extractLsb (spec.mantissaBitsWithoutImplicit - 1) 0 |>.cast (by have := spec.hm; omega)
+  b.extractLsb' 0 spec.mantissaBitsWithoutImplicit
 
 /--
 Unpacks the exponent portion of the packed float.
 -/
 def unpackExponent {spec : Format} (b : BitVec spec.numBits) :
     BitVec spec.exponentBits :=
-  b.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits - 1) spec.mantissaBitsWithoutImplicit |>.cast (by have := spec.he; omega)
+  b.extractLsb' spec.mantissaBitsWithoutImplicit spec.exponentBits
 
 /--
 Unpacks the sign bit of the packed float.
 -/
 def unpackSign {spec : Format} (b : BitVec spec.numBits) :
     BitVec 1 :=
-  b.extractLsb (spec.mantissaBitsWithoutImplicit + spec.exponentBits) (spec.mantissaBitsWithoutImplicit + spec.exponentBits) |>.cast (by omega)
+  b.extractLsb' (spec.mantissaBitsWithoutImplicit + spec.exponentBits) 1
 
 /--
 Unpacks the given float according to the given specification.

src/Init/Data/Float/Model/Unpacked/Pack/Lemmas.lean

@@ -49,6 +49,6 @@ theorem valid_pack {spec : Format} {f : UnpackedFloat} : spec.Valid (pack spec f
       omega
     omega
   | case6 s m e hm actualMantissaBits biasedExponent h₁ h₂ =>
-    simp [Nat.pos_iff_ne_zero.1 spec.he]
+    simp [Nat.ne_zero_of_lt spec.he]
 
 end Float.Model.UnpackedFloat

src/Init/Data/Float/Model/Unpacked/Sign.lean

@@ -27,7 +27,7 @@ inductive Sign where
   | negative : Sign
   /-- Positive (`+`) sign. -/
   | positive : Sign
-deriving Repr, BEq
+deriving Repr, DecidableEq
 
 namespace Sign
 

src/Init/Data/OfScientific.lean

@@ -64,23 +64,26 @@ instance : OfScientific Float where
 Converts a natural number into the closest-possible 64-bit floating-point number, or an infinite
 floating-point value if the range of `Float` is exceeded.
 -/
-@[export lean_float_of_nat]
-def Float.ofNat (n : Nat) : Float :=
+@[export lean_float_of_nat, expose]
+protected def Float.ofNat (n : Nat) : Float :=
   OfScientific.ofScientific n false 0
 
 /--
 Converts an integer into the closest-possible 64-bit floating-point number, or positive or negative
 infinite floating-point value if the range of `Float` is exceeded.
 -/
-def Float.ofInt : Int → Float
+@[expose] protected def Float.ofInt : Int → Float
   | Int.ofNat n => Float.ofNat n
   | Int.negSucc n => Float.neg (Float.ofNat (Nat.succ n))
 
-instance : OfNat Float n   := ⟨Float.ofNat n⟩
+instance : OfNat Float n := ⟨Float.ofNat n⟩
 
 @[inherit_doc Float.ofNat] abbrev Nat.toFloat (n : Nat) : Float :=
   Float.ofNat n
 
+@[inherit_doc Float.ofInt] abbrev Int.toFloat (n : Int) : Float :=
+  Float.ofInt n
+
 /--
 Precomputed values of `10 ^ e` for `0 ≤ e ≤ 10 `. In this range, the values can be represented
 exactly.
@@ -91,7 +94,7 @@ exactly.
    Float32.ofBits 0x49742400, Float32.ofBits 0x4B189680, Float32.ofBits 0x4CBEBC20,
    Float32.ofBits 0x4E6E6B28, Float32.ofBits 0x501502F9]
 
-@[expose] protected def Float32.ofScientific (m :Nat) (s : Bool) (e : Nat) : Float32 :=
+@[expose] protected def Float32.ofScientific (m : Nat) (s : Bool) (e : Nat) : Float32 :=
   -- See comments on `Float.ofScientific`.
   if h : m < 2 ^ 23 ∧ e ≤ 10 then
     let powerOfTen : Float32 :=
@@ -111,19 +114,22 @@ instance : OfScientific Float32 where
 Converts a natural number into the closest-possible 32-bit floating-point number, or an infinite
 floating-point value if the range of `Float32` is exceeded.
 -/
-@[export lean_float32_of_nat]
-def Float32.ofNat (n : Nat) : Float32 :=
+@[export lean_float32_of_nat, expose]
+protected def Float32.ofNat (n : Nat) : Float32 :=
   OfScientific.ofScientific n false 0
 
 /--
 Converts an integer into the closest-possible 32-bit floating-point number, or positive or negative
 infinite floating-point value if the range of `Float32` is exceeded.
 -/
-def Float32.ofInt : Int → Float32
+@[expose] protected def Float32.ofInt : Int → Float32
   | Int.ofNat n => Float32.ofNat n
   | Int.negSucc n => Float32.neg (Float32.ofNat (Nat.succ n))
 
-instance : OfNat Float32 n   := ⟨Float32.ofNat n⟩
+instance : OfNat Float32 n := ⟨Float32.ofNat n⟩
 
 @[inherit_doc Float32.ofNat] abbrev Nat.toFloat32 (n : Nat) : Float32 :=
   Float32.ofNat n
+
+@[inherit_doc Float32.ofInt] abbrev Int.toFloat32 (n : Int) : Float32 :=
+  Float32.ofInt n

tests/compile/float.lean

@@ -21,6 +21,8 @@ def tst1 : IO Unit := do
   IO.println (0 / 0 : Float).toUInt32
   IO.println (0 / 0 : Float).toUInt64
   IO.println (0 / 0 : Float).toUSize
+  IO.println Float.nan.isNaN
+  IO.println Float.inf.isInf
 
   IO.println (-1 : Float).toUInt8
   IO.println (256 : Float).toUInt8