Floating point standardization: build a Floating out of n : Int64, s : UInt64`

@[irreducible, specialize #[]]

def Floating.lower (g s : UInt64) : UInt64 × UInt64

Decrease s by g if possible, saturating at s = 0. We return (t, s - t) where t is the normalized exponent.

Equations

• Floating.lower g s = (bif decide (s < g) then 0 else s - g, s - bif decide (s < g) then 0 else s - g)

@[simp]

theorem Floating.low_d_le (g s : UInt64) : (lower g s).2.toNat ≤ g.toNat

lower returns small shifts

theorem Floating.low_le_s (g s : UInt64) : (lower g s).1 ≤ s

lower reduces the exponent

theorem Floating.low_le_s' {g s : UInt64} : (lower g s).1.toNat ≤ s.toNat

lower reduces the exponent

theorem Floating.low_s_2_eq {g s : UInt64} : (lower g s).2.toNat = s.toNat - (lower g s).1.toNat

lower.2 in terms of lower.1, expressed in terms of ℕ

@[simp]

theorem Floating.log2_g_le_62 {n : Int64} (nm : n ≠ Int64.minValue) : n.uabs.log2 ≤ 62

@[simp]

theorem Floating.log2_g_le_62' {n : Int64} (nm : n ≠ Int64.minValue) : n.uabs.toNat.log2 ≤ 62

@[simp]

theorem Floating.low_d_le_62 {n : Int64} (nm : n ≠ Int64.minValue) (s : UInt64) : (lower (62 - n.uabs.log2) s).2.toNat ≤ 62

lower returns shifts under 62

@[simp]

theorem Floating.low_lt {n : Int64} (nm : n ≠ Int64.minValue) (s : UInt64) : n.uabs.toNat * 2 ^ (lower (62 - n.uabs.log2) s).2.toNat < 2 ^ 63

low doesn't overflow

@[simp]

theorem Floating.low_lt' {n : Int64} (nm : n ≠ Int64.minValue) (s : UInt64) : |↑n * 2 ^ (lower (62 - n.uabs.log2) s).2.toNat| < 2 ^ 63

low doesn't overflow

theorem Floating.coe_low_s {n : Int64} {s : UInt64} (nm : n ≠ Int64.minValue) : ↑(n <<< (lower (62 - n.uabs.log2) s).2) = ↑n * 2 ^ (lower (62 - n.uabs.log2) s).2.toNat

lower respects ℤ conversion

theorem Floating.of_ns_ne_nan {n : Int64} {s : UInt64} (nm : n ≠ Int64.minValue) : n <<< (lower (62 - n.uabs.log2) s).2 ≠ Int64.minValue

of_ns doesn't create nan

theorem Floating.of_ns_norm {n : Int64} {s : UInt64} (n0 : n ≠ 0) (nm : n ≠ Int64.minValue) : n <<< (lower (62 - n.uabs.fast_log2) s).2 ≠ 0 → n <<< (lower (62 - n.uabs.fast_log2) s).2 ≠ Int64.minValue → (lower (62 - n.uabs.fast_log2) s).1 ≠ 0 → 2 ^ 62 ≤ (n <<< (lower (62 - n.uabs.fast_log2) s).2).uabs

of_ns satisfies norm

theorem Floating.valid_of_ns {n : Int64} {s : UInt64} (nm : n ≠ Int64.minValue) (n0 : n ≠ 0) : have t := lower (62 - n.uabs.fast_log2) s; Valid (n <<< t.2) t.1

of_ns is valid

@[irreducible]

def Floating.of_ns (n : Int64) (s : UInt64) : Floating

Construct a Floating given possibly non-standardized n, s

Equations

• Floating.of_ns n s = if nm : n = Int64.minValue then nan else if n0 : n = 0 then 0 else let t := Floating.lower (62 - n.uabs.fast_log2) s; { n := n <<< t.2, s := t.1, v := ⋯ }

@[simp]

theorem Floating.of_ns_nan (s : UInt64) : of_ns Int64.minValue s = nan

of_ns propagates nan

@[simp]

theorem Floating.of_ns_zero (s : UInt64) : of_ns 0 s = 0

of_ns propagates 0

theorem Floating.val_of_ns {n : Int64} {s : UInt64} (nm : n ≠ Int64.minValue) : (of_ns n s).val = ↑↑n * 2 ^ (s.toInt - 2 ^ 63)

of_ns preserves val

@[simp]

theorem Floating.of_ns_eq_nan_iff {n : Int64} {s : UInt64} : of_ns n s = nan ↔ n = Int64.minValue

of_ns doesn't create nan

@[simp]

theorem Floating.of_ns_ne_nan_iff {n : Int64} {s : UInt64} : of_ns n s ≠ nan ↔ n ≠ Int64.minValue

of_ns doesn't create nan

Coersion from fixed point to floating point

@[irreducible]

def Fixed.toFloating {s : Int64} (x : Fixed s) : Floating

Fixed s to Floating by hiding s

Equations

• ↑x = Floating.of_ns x.n (s.toUInt64 + 2 ^ 63)

@[instance_reducible]

instance Floating.instCoeHeadFixed {s : Int64} : CoeHead (Fixed s) Floating

Coersion from Fixed s to Floating

Equations

• Floating.instCoeHeadFixed = { coe := fun (x : Fixed s) => ↑x }

theorem Floating.approx_coe {s : Int64} {x : Fixed s} {a : ℝ} (ax : approx x a) : approx (↑x) a

To prove a ∈ approx (x : Floating), we prove a ∈ approx x

@[simp]

theorem Fixed.toFloating_nan {s : Int64} : ↑nan = nan