feat: add Float.toBits and Float.fromBits

This PR adds raw transmutation of floating-point numbers to and from `UInt64`. Floats and UInts share the same endianness across all supported platforms. The IEEE 754 standard precisely specifies the bit layout of floats. Note that `Float.toBits` is distinct from `Float.toUInt64`, which attempts to preserve the numeric value rather than the bitwise value.

src/Init/Data/Array/Attach.lean

@@ -10,6 +10,16 @@ import Init.Data.List.Attach
 
 namespace Array
 
+/-- `O(n)`. Partial map. If `f : Π a, P a → β` is a partial function defined on
+  `a : α` satisfying `P`, then `pmap f l h` is essentially the same as `map f l`
+  but is defined only when all members of `l` satisfy `P`, using the proof
+  to apply `f`.
+
+We replace this at runtime with a more efficient version via
+-/
+def pmap {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) : Array β :=
+  (l.toList.pmap f (fun a m => H a (mem_def.mpr m))).toArray
+
 /--
 Unsafe implementation of `attachWith`, taking advantage of the fact that the representation of
 `Array {x // P x}` is the same as the input `Array α`.
@@ -35,6 +45,10 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.toArray.attach = (l.attachWith (· ∈ l.toArray) (by simp)).toArray := by
   simp [attach]
 
+@[simp] theorem _root_.List.pmap_toArray {l : List α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l.toArray, P a} :
+    l.toArray.pmap f H = (l.pmap f (by simpa using H)).toArray := by
+  simp [pmap]
+
 @[simp] theorem toList_attachWith {l : Array α} {P : α → Prop} {H : ∀ x ∈ l, P x} :
    (l.attachWith P H).toList = l.toList.attachWith P (by simpa [mem_toList] using H) := by
   simp [attachWith]
@@ -43,6 +57,22 @@ Unsafe implementation of `attachWith`, taking advantage of the fact that the rep
     l.attach.toList = l.toList.attachWith (· ∈ l) (by simp [mem_toList]) := by
   simp [attach]
 
+@[simp] theorem toList_pmap {l : Array α} {P : α → Prop} {f : ∀ a, P a → β} {H : ∀ a ∈ l, P a} :
+    (l.pmap f H).toList = l.toList.pmap f (fun a m => H a (mem_def.mpr m)) := by
+  simp [pmap]
+
+/-- Implementation of `pmap` using the zero-copy version of `attach`. -/
+@[inline] private def pmapImpl {P : α → Prop} (f : ∀ a, P a → β) (l : Array α) (H : ∀ a ∈ l, P a) :
+    Array β := (l.attachWith _ H).map fun ⟨x, h'⟩ => f x h'
+
+@[csimp] private theorem pmap_eq_pmapImpl : @pmap = @pmapImpl := by
+  funext α β p f L h'
+  cases L
+  simp only [pmap, pmapImpl, List.attachWith_toArray, List.map_toArray, mk.injEq, List.map_attachWith]
+  apply List.pmap_congr_left
+  intro a m h₁ h₂
+  congr
+
 @[simp] theorem _root_.List.attachWith_mem_toArray {l : List α} :
     l.attachWith (fun x => x ∈ l.toArray) (fun x h => by simpa using h) =
       l.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩ := by

src/Init/Data/Float.lean

@@ -47,6 +47,25 @@ def Float.lt : Float → Float → Prop := fun a b =>
 def Float.le : Float → Float → Prop := fun a b =>
   floatSpec.le a.val b.val
 
+/--
+Raw transmutation from `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+-/
+@[extern "lean_float_from_bits"] opaque Float.fromBits : UInt64 → Float
+
+/--
+Raw transmutation to `UInt64`.
+
+Floats and UInts have the same endianness on all supported platforms.
+IEEE 754 very precisely specifies the bit layout of floats.
+
+Note that this function is distinct from `Float.toUInt64`, which attempts
+to preserve the numeric value, and not the bitwise value.
+-/
+@[extern "lean_float_to_bits"] opaque Float.toBits : Float → UInt64
+
 instance : Add Float := ⟨Float.add⟩
 instance : Sub Float := ⟨Float.sub⟩
 instance : Mul Float := ⟨Float.mul⟩

src/Init/Data/List/Basic.lean

@@ -551,7 +551,7 @@ theorem reverseAux_eq_append (as bs : List α) : reverseAux as bs = reverseAux a
 /-! ### flatten -/
 
 /--
-`O(|flatten L|)`. `join L` concatenates all the lists in `L` into one list.
+`O(|flatten L|)`. `flatten L` concatenates all the lists in `L` into one list.
 * `flatten [[a], [], [b, c], [d, e, f]] = [a, b, c, d, e, f]`
 -/
 def flatten : List (List α) → List α

src/Lean/Compiler/ConstFolding.lean

@@ -133,8 +133,8 @@ def foldNatBinBoolPred (fn : Nat → Nat → Bool) (a₁ a₂ : Expr) : Option E
     return mkConst ``Bool.false
 
 def foldNatBeq := fun _ : Bool => foldNatBinBoolPred (fun a b => a == b)
-def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
-def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
+def foldNatBlt := fun _ : Bool => foldNatBinBoolPred (fun a b => a < b)
+def foldNatBle := fun _ : Bool => foldNatBinBoolPred (fun a b => a ≤ b)
 
 def natFoldFns : List (Name × BinFoldFn) :=
   [(``Nat.add, foldNatAdd),

src/Lean/PrettyPrinter/Delaborator/Builtins.lean

@@ -1092,19 +1092,29 @@ def coeDelaborator : Delab := whenPPOption getPPCoercions do
   let e ← getExpr
   let .const declName _ := e.getAppFn | failure
   let some info ← Meta.getCoeFnInfo? declName | failure
+  let n := e.getAppNumArgs
+  guard <| n ≥ info.numArgs
   if (← getPPOption getPPExplicit) && info.coercee != 0 then
     -- Approximation: the only implicit arguments come before the coercee
     failure
-  let n := e.getAppNumArgs
-  withOverApp info.numArgs do
-    match info.type with
-    | .coe => `(↑$(← withNaryArg info.coercee delab))
-    | .coeFun =>
-      if n = info.numArgs then
-        `(⇑$(← withNaryArg info.coercee delab))
-      else
-        withNaryArg info.coercee delab
-    | .coeSort => `(↥$(← withNaryArg info.coercee delab))
+  if n == info.numArgs then
+    delabHead info 0 false
+  else
+    let nargs := n - info.numArgs
+    delabAppCore nargs (delabHead info nargs) (unexpand := false)
+where
+  delabHead (info : CoeFnInfo) (nargs : Nat) (insertExplicit : Bool) : Delab := do
+    guard <| !insertExplicit
+    if info.type == .coeFun && nargs > 0 then
+      -- In the CoeFun case, annotate with the coercee itself.
+      -- We can still see the whole coercion expression by hovering over the whitespace between the arguments.
+      withNaryArg info.coercee <| withAnnotateTermInfo delab
+    else
+      withAnnotateTermInfo do
+        match info.type with
+        | .coe     => `(↑$(← withNaryArg info.coercee delab))
+        | .coeFun  => `(⇑$(← withNaryArg info.coercee delab))
+        | .coeSort => `(↥$(← withNaryArg info.coercee delab))
 
 @[builtin_delab app.dite]
 def delabDIte : Delab := whenNotPPOption getPPExplicit <| whenPPOption getPPNotation <| withOverApp 5 do

src/Std/Tactic/BVDecide/Normalize/Canonicalize.lean

@@ -99,17 +99,5 @@ attribute [bv_normalize] BitVec.mul_eq
 attribute [bv_normalize] BitVec.udiv_eq
 attribute [bv_normalize] BitVec.umod_eq
 
-@[bv_normalize]
-theorem Bool.and_eq_and (x y : Bool) : x.and y = (x && y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.or_eq_or (x y : Bool) : x.or y = (x || y) := by
-  rfl
-
-@[bv_normalize]
-theorem Bool.no_eq_not (x : Bool) : x.not = !x := by
-  rfl
-
 end Normalize
 end Std.Tactic.BVDecide

src/include/lean/lean.h

@@ -1259,6 +1259,8 @@ static inline lean_obj_res lean_nat_mod(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_eq(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 == a2;
     } else {
         return lean_nat_big_eq(a1, a2);
@@ -1275,6 +1277,8 @@ static inline bool lean_nat_ne(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 <= a2;
     } else {
         return lean_nat_big_le(a1, a2);
@@ -1287,6 +1291,8 @@ static inline uint8_t lean_nat_dec_le(b_lean_obj_arg a1, b_lean_obj_arg a2) {
 
 static inline bool lean_nat_lt(b_lean_obj_arg a1, b_lean_obj_arg a2) {
     if (LEAN_LIKELY(lean_is_scalar(a1) && lean_is_scalar(a2))) {
+        // This comparison is UB according to the standard but allowed as per the
+        // GCC documentation and the address sanitizer does not complain about it.
         return a1 < a2;
     } else {
         return lean_nat_big_lt(a1, a2);
@@ -2685,6 +2691,8 @@ static inline size_t lean_float_to_usize(double a) {
     else
         return (size_t) lean_float_to_uint32(a); // NOLINT
 }
+LEAN_EXPORT double lean_float_from_bits(uint64_t u);
+LEAN_EXPORT uint64_t lean_float_to_bits(double d);
 static inline double lean_float_add(double a, double b) { return a + b; }
 static inline double lean_float_sub(double a, double b) { return a - b; }
 static inline double lean_float_mul(double a, double b) { return a * b; }

src/runtime/object.cpp

@@ -1620,6 +1620,21 @@ extern "C" LEAN_EXPORT obj_res lean_float_frexp(double a) {
     return r;
 }
 
+extern "C" LEAN_EXPORT double lean_float_from_bits(uint64_t u)
+{
+    static_assert(sizeof(double) == sizeof(u), "`double` unexpected size.");
+    double ret;
+    std::memcpy(&ret, &u, sizeof(double));
+    return ret;
+}
+
+extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
+{
+    uint64_t ret;
+    std::memcpy(&ret, &d, sizeof(double));
+    return ret;
+}
+
 // =======================================
 // Strings
 

tests/lean/run/6086.lean

@@ -0,0 +1,3 @@
+/-- info: [true, true, false, true, false, false, true, true, false, true, false, false] -/
+#guard_msgs in
+#eval [Nat.ble 36 37, Nat.ble 37 37, Nat.ble 38 37, Nat.blt 36 37, Nat.blt 37 37, Nat.blt 38 37, 36 ≤ 37, 37 ≤ 37, 38 ≤ 37 ,36 < 37, 37 < 37, 38 < 37]

tests/lean/run/floatBits.lean

@@ -0,0 +1,13 @@
+def d : Float := 1.245
+
+/--
+info: 4608285800708723180
+-/
+#guard_msgs in
+#eval d.toBits
+
+/--
+info: true
+-/
+#guard_msgs in
+#eval Float.fromBits d.toBits == d