Floating point arithmetic

The floating point number ⟨n,s⟩ represents n * 2^(s - 2^63), where n : Int64, s : UInt64.

Floating basics

structure Floating.Valid (n : Int64) (s : UInt64) : Prop

Validity of a Floating as a single type

• zero_same : n = 0 → s = 0

  0 has a single, standardized representation

• nan_same : n = Int64.minValue → s = UInt64.max

  nan has a single, standardized representation

• norm : n ≠ 0 → n ≠ Int64.minValue → s ≠ 0 → 2 ^ 62 ≤ n.uabs

  If we're not 0, nan, or denormalized, the high bit of n is set

@[unbox]

structure Floating : Type

Floating point number

• n : Int64

  Unscaled value

• s : UInt64

  Binary exponent + 2^63

• v : Valid self.n self.s

  We're valid and normalized

@[instance_reducible]

instance instDecidableEqFloating : DecidableEq Floating

Equations

• instDecidableEqFloating = instDecidableEqFloating.decEq

def instDecidableEqFloating.decEq (x✝ x✝¹ : Floating) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

theorem Floating.zero_same (x : Floating) : x.n = 0 → x.s = 0

theorem Floating.nan_same (x : Floating) : x.n = Int64.minValue → x.s = UInt64.max

theorem Floating.norm (x : Floating) : x.n ≠ 0 → x.n ≠ Int64.minValue → x.s ≠ 0 → 2 ^ 62 ≤ x.n.uabs

def Floating.valid (n : Int64) (s : UInt64) : Bool

Computational version of Floating.Valid

Equations

• Floating.valid n s = bif n == 0 then s == 0 else bif n == Int64.minValue then s == UInt64.max else s == 0 || decide (1 <<< 62 ≤ n.uabs)

theorem Floating.valid_iff {n : Int64} {s : UInt64} : Valid n s ↔ valid n s = true

Floating.valid decides Floating.Valid

@[instance_reducible]

instance Floating.instDecidableValid (n : Int64) (s : UInt64) : Decidable (Valid n s)

Valid is decidable

Equations

• Floating.instDecidableValid n s = if v : Floating.valid n s = true then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Floating.instBEq : BEq Floating

Equations

• Floating.instBEq = { beq := fun (x y : Floating) => x.n == y.n && x.s == y.s }

theorem Floating.beq_def {x y : Floating} : (x == y) = (x.n == y.n && x.s == y.s)

instance Floating.instLawfulBEq : LawfulBEq Floating

theorem Floating.ext_iff {x y : Floating} : x = y ↔ x.n = y.n ∧ x.s = y.s

@[instance_reducible]

instance Floating.instNan : Nan Floating

Standard floating point nan

Equations

• Floating.instNan = { nan := { n := Int64.minValue, s := UInt64.max, v := Floating.instNan._proof_1 } }

noncomputable def Floating.val (x : Floating) : ℝ

The ℝ that a Floating represents, if it's not nan

Equations

• x.val = ↑↑x.n * 2 ^ (x.s.toInt - 2 ^ 63)

def Floating.valq (x : Floating) : ℚ

The ℚ that a Floating represents, if it's not nan

Equations

• x.valq = ↑↑x.n * 2 ^ (x.s.toInt - 2 ^ 63)

@[instance_reducible]

instance Floating.instApproxReal : Approx Floating ℝ

Floating approximates ℝ

Equations

• Floating.instApproxReal = { approx := fun (x : Floating) (a : ℝ) => x = nan ∨ x.val = a }

@[instance_reducible]

instance Floating.instZero : Zero Floating

0 : Floating

Equations

• Floating.instZero = { zero := { n := 0, s := 0, v := Floating.instZero._proof_1 } }

@[instance_reducible]

instance Floating.instOne : One Floating

1 : Floating

Equations

• Floating.instOne = { one := { n := 2 ^ 62, s := 2 ^ 63 - 62, v := Floating.instOne._proof_2 } }

@[simp]

theorem Floating.n_zero : n 0 = 0

@[simp]

theorem Floating.s_zero : s 0 = 0

@[simp]

theorem Floating.n_one : n 1 = 2 ^ 62

@[simp]

theorem Floating.s_one : s 1 = 2 ^ 63 - 62

@[simp]

theorem Floating.n_nan : nan.n = Int64.minValue

@[simp]

theorem Floating.s_nan : nan.s = UInt64.max

instance Floating.instApproxNanReal : ApproxNan Floating ℝ

nan could be anything

@[simp]

theorem Floating.val_zero : val 0 = 0

0 = 0

@[simp]

theorem Floating.zero_ne_nan : 0 ≠ nan

0 ≠ nan

@[simp]

theorem Floating.nan_ne_zero : nan ≠ 0

nan ≠ 0

@[simp]

theorem Floating.one_ne_nan : 1 ≠ nan

1 ≠ nan

@[simp]

theorem Floating.nan_ne_one : nan ≠ 1

nan ≠ 1

@[simp]

theorem Floating.approx_zero_iff {a : ℝ} : approx 0 a ↔ a = 0

0 is just zero

instance Floating.instApproxZeroReal : ApproxZero Floating ℝ

instance Floating.instApproxZeroIffReal : ApproxZeroIff Floating ℝ

@[simp]

theorem Floating.val_one : val 1 = 1

1 = 1

instance Floating.instApproxOneReal : ApproxOne Floating ℝ

theorem Floating.val_nan : nan.val = -2 ^ 63 * 2 ^ (2 ^ 63 - 1)

@[simp]

theorem Floating.approx_eq_singleton {a : ℝ} {x : Floating} (n : x ≠ nan) : approx x a ↔ x.val = a

If we're not nan, approx is a singleton

@[simp]

theorem Floating.approx_val {x : Floating} : approx x x.val

theorem Floating.n_ne_min {x : Floating} (n : x ≠ nan) : x.n ≠ Int64.minValue

If we're not nan, x.n ≠ .min

theorem Floating.n_ne_zero {x : Floating} (n : x ≠ 0) : x.n ≠ 0

If we're not zero, x.n ≠ 0

theorem Floating.n_ne_zero' {x : Floating} (n : x.s ≠ 0) : x.n ≠ 0

If x.s ≠ 0, x.n ≠ 0

theorem Floating.n_eq_zero_iff {x : Floating} : x.n = 0 ↔ x = 0

x.n = 0 exactly at 0

theorem Floating.norm' {x : Floating} (x0 : x ≠ 0) (s0 : x.s.toNat ≠ 0) : 2 ^ 62 ≤ x.n.uabs.toNat

More user friendly version of x.norm

theorem Floating.val_eq_zero {x : Floating} : x.val = 0 ↔ x = 0

Only 0 has zero val

theorem Floating.val_ne_zero {x : Floating} : x.val ≠ 0 ↔ x ≠ 0

Only 0 has zero val

@[simp]

theorem Floating.coe_valq {x : Floating} : ↑x.valq = x.val

valq = val

Simplification lemmas used elsewhere

This should really be cleaned up

@[simp]

theorem Floating.u62 : UInt64.toNat 62 = 62

@[simp]

theorem Floating.u64 : UInt64.toNat 64 = 64

@[simp]

theorem Floating.u65 : UInt64.toNat 65 = 65

@[simp]

theorem Floating.u126 : UInt64.toNat 126 = 126

@[simp]

theorem Floating.u127 : UInt64.toNat 127 = 127

@[simp]

theorem Floating.up62 : (2 ^ 62).toNat = 2 ^ 62

@[simp]

theorem Floating.up63 : (2 ^ 63).toNat = 2 ^ 63

@[simp]

theorem Floating.ua2 : Int.natAbs 2 = 2

theorem Floating.rounds_iff {a : ℝ} {x : Floating} {up : Bool} : Rounds x a up ↔ x ≠ nan → if up = true then a ≤ x.val else x.val ≤ a

theorem Floating.rounds_of_ne_nan {a : ℝ} {x : Floating} {up : Bool} (h : x ≠ nan → if up = true then a ≤ x.val else x.val ≤ a) : Rounds x a up

Remove a nan possibility from a rounding statement

theorem Floating.val_of_nonneg {x : Floating} (x0 : 0 ≤ x.val) : x.val = ↑x.n.toUInt64.toNat * 2 ^ (↑x.s.toNat - 2 ^ 63)

val if we're nonnegative

The smallest normalized value

@[irreducible]

def Floating.min_norm : Floating

The smallest normalized floating point value

@[simp]

theorem Floating.min_norm_ne_nan : min_norm ≠ nan

@[simp]

theorem Floating.val_min_norm : min_norm.val = 2 ^ (62 - 2 ^ 63)

Conversion to Float

@[irreducible]

def Floating.toFloat (x : Floating) : Float

Approximate Floating by a Float

Equations

• x.toFloat = bif x == nan then Float.nan else x.n.toFloat.scaleB (x.s.toInt - 2 ^ 63)

Print Floating in 7 significant digits, rounding down arbitrarily

@[irreducible]

def Floating.decimal (x : Floating) (prec : ℕ) (up : Bool) : Decimal

Convert to Decimal with a given precision and rounding. Ignores nan and takes abs.

Equations

• x.decimal prec up = Decimal.ofBinary (↑x.n) (x.s.toInt - 2 ^ 63) prec up

theorem Floating.decimal_le (x : Floating) (prec : ℕ) : (x.decimal prec false).val ≤ x.val

decimal rounds down if desired

theorem Floating.le_decimal (x : Floating) (prec : ℕ) : x.val ≤ (x.decimal prec true).val

decimal rounds up if desired

@[instance_reducible]

instance Floating.instRepr : Repr Floating

We print Fixed s as an approximate floating point number

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance Floating.instReprRaw : Repr (Raw Floating)

Print raw representation of a Floating

Equations

• Floating.instReprRaw = { reprPrec := fun (x : Raw Floating) (x_1 : ℕ) => Std.format "⟨⟨" ++ Std.format x.val.n.toUInt64 ++ Std.format "⟩, ⟨" ++ Std.format x.val.s ++ Std.format "⟩, _⟩" }