Conversion from ℕ, ℤ, ℚ, Float to Floating

Normalization given n ∈ [2^62, 2^63]

structure Floating.Convert : Type

A normalized n, s pair ready for conversion to Floating

• n : ℕ
• s : ℤ
• norm : self.n ∈ Set.Ico (2 ^ 62) (2 ^ 63)

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

Equations

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

theorem Floating.Convert.n_mod (x : Convert) : x.n % 2 ^ 64 = x.n

theorem Floating.Convert.valid_finish (x : Convert) : Valid x.n.toInt64 (UInt64.ofInt x.s)

Convert.finish is valid`

theorem Floating.Convert.valid_finish.e (x : Convert) : x.n % 2 ^ 64 = x.n

@[irreducible]

def Floating.Convert.finish (x : Convert) (up : Bool) : Floating

Build a Floating out of n * 2^(s - 2^63), rounding if required

Equations

• x.finish up = if x.s < 0 then bif up then Floating.min_norm else 0 else if 2 ^ 64 ≤ x.s then nan else { n := x.n.toInt64, s := UInt64.ofInt x.s, v := ⋯ }

theorem Floating.valid_convert_tweak : 2 ^ 62 ∈ Set.Ico (2 ^ 62) (2 ^ 63)

@[irreducible]

def Floating.convert_tweak (n : ℕ) (s : ℤ) (norm : n ∈ Set.Icc (2 ^ 62) (2 ^ 63)) : Convert

Build a Floating out of n * 2^(s - 2^63), rounding if required

Equations

• Floating.convert_tweak n s norm = if e : n = 2 ^ 63 then { n := 2 ^ 62, s := s + 1, norm := Floating.valid_convert_tweak } else { n := n, s := s, norm := ⋯ }

theorem Floating.Convert.approx_finish (x : Convert) (up : Bool) : Rounds (x.finish up) x.val up

Convert.finish is correct

theorem Floating.val_convert_tweak (n : ℕ) (s : ℤ) (norm : n ∈ Set.Icc (2 ^ 62) (2 ^ 63)) : (convert_tweak n s norm).val = ↑n * 2 ^ (s - 2 ^ 63)

convert_tweak is correct

theorem Floating.approx_convert {a : ℝ} {n : ℕ} {s : ℤ} {norm : n ∈ Set.Icc (2 ^ 62) (2 ^ 63)} {up : Bool} (an : if up = true then a ≤ ↑n * 2 ^ (s - 2 ^ 63) else ↑n * 2 ^ (s - 2 ^ 63) ≤ a) : Rounds ((convert_tweak n s norm).finish up) a up

Prove a (convert_tweak _ _ _).finish _ call is correct, in context.

Conversion from ℕ

theorem Floating.ofNat_norm {n : ℕ} {up : Bool} : have t := n.log2; have s := t - 62; ¬t ≤ 62 → n.shiftRightRound s up ∈ Set.Icc (2 ^ 62) (2 ^ 63)

@[irreducible]

def Floating.ofNat (n : ℕ) (up : Bool) : Floating

Conversion from ℕ to Floating, rounding up or down

Equations

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

instance Floating.instOfNatOfAtLeastTwo {n : ℕ} [n.AtLeastTwo] : OfNat Floating n

Conversion from ℕ literals to Floating, rounding down arbitrarily. Use Interval.ofNat if you want something trustworthy (it rounds both ways).

Equations

• Floating.instOfNatOfAtLeastTwo = { ofNat := Floating.ofNat n false }

theorem Floating.val_ofNat' {n : ℕ} (lt : n < 2 ^ 63 := by norm_num) {up : Bool} : (ofNat n up).val = ↑n

Small naturals convert exactly

theorem Floating.val_ofNat {n : ℕ} [n.AtLeastTwo] (lt : n < 2 ^ 63 := by norm_num) : val (OfNat.ofNat n) = ↑n

Small naturals convert exactly

theorem Floating.ofNat_ne_nan {n : ℕ} (lt : n < 2 ^ 63) (up : Bool) : ofNat n up ≠ nan

Small naturals do not overflow. Much larger values also do not overflow, but this is all we need at the moment.

theorem Floating.approx_ofNat (n : ℕ) (up : Bool) : Rounds (ofNat n up) (↑n) up

ofNat rounds the desired way

theorem Floating.ofNat_le {n : ℕ} (h : ofNat n false ≠ nan) : (ofNat n false).val ≤ ↑n

approx_ofNat, down version

theorem Floating.le_ofNat {n : ℕ} (h : ofNat n true ≠ nan) : ↑n ≤ (ofNat n true).val

approx_ofNat, up version

theorem Floating.ofNat_le_ofNat {n : ℕ} (h : ofNat n true ≠ nan) : (ofNat n false).val ≤ (ofNat n true).val

Combined version, for use in Interval construction

Conversion from ℤ

@[irreducible]

def Floating.ofInt (n : ℤ) (up : Bool) : Floating

Conversion from ℤ

Equations

• Floating.ofInt n up = bif decide (n < 0) then -Floating.ofNat (-n).toNat !up else Floating.ofNat n.toNat up

theorem Floating.approx_ofInt (n : ℤ) (up : Bool) : Rounds (ofInt n up) (↑n) up

ofInt rounds the desired way

theorem Floating.ofInt_le {n : ℤ} (h : ofInt n false ≠ nan) : (ofInt n false).val ≤ ↑n

approx_ofInt, down version

theorem Floating.le_ofInt {n : ℤ} (h : ofInt n true ≠ nan) : ↑n ≤ (ofInt n true).val

approx_ofInt, up version

theorem Floating.ofInt_le_ofInt {n : ℤ} (h : ofInt n true ≠ nan) : (ofInt n false).val ≤ (ofInt n true).val

Combined version, for use in Interval construction

Conversion from ℚ

theorem Floating.ofRat_norm {x : ℚ} {up : Bool} (x0 : ¬x = 0) : have r := x.log2; have n := x.num.natAbs; have p := if r ≤ 62 then (n <<< (62 - r).toNat, x.den) else (n, x.den <<< (r - 62).toNat); p.1.rdiv p.2 up ∈ Set.Icc (2 ^ 62) (2 ^ 63)

ofRat_abs gives the right input to convert_tweak

@[irreducible, inline]

def Floating.ofRat_abs (x : ℚ) (up : Bool) : Floating

Conversion from ℚ, taking absolute values and rounding up or down

Equations

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

@[irreducible]

def Floating.ofRat (x : ℚ) (up : Bool) : Floating

Conversion from ℚ, rounding up or down

Equations

• Floating.ofRat x up = bif decide (x < 0) then -Floating.ofRat_abs x (up != decide (x < 0)) else Floating.ofRat_abs x (up != decide (x < 0))

theorem Floating.approx_ofRat_abs (x : ℚ) (up : Bool) : Rounds (ofRat_abs x up) (↑|x|) up

ofRat_abs rounds the desired way

theorem Floating.approx_ofRat (x : ℚ) (up : Bool) : Rounds (ofRat x up) (↑x) up

ofRat rounds the desired way

theorem Floating.ofRat_le {x : ℚ} (h : ofRat x false ≠ nan) : (ofRat x false).val ≤ ↑x

approx_ofRat, down version

theorem Floating.le_ofRat {x : ℚ} (h : ofRat x true ≠ nan) : ↑x ≤ (ofRat x true).val

approx_ofRat, up version

theorem Floating.ofRat_le_ofRat {x : ℚ} (h : ofRat x true ≠ nan) : (ofRat x false).val ≤ (ofRat x true).val

Combined version, for use in Interval construction

Conversion from Float

@[irreducible]

def Floating.ofFloat (x : Float) (up : Bool) : Floating

Convert a Float to Floating. This could be fast, but we don't need it to be.

Equations

• Floating.ofFloat x up = match x.toRatParts with | none => nan | some (y, s) => have t := ↑s; if s ≠ ↑t then nan else (Floating.ofInt y up).scaleB t

theorem Floating.ofFloat_le_ofFloat {x : Float} (n0 : ofFloat x false ≠ nan) (n1 : ofFloat x true ≠ nan) : (ofFloat x false).val ≤ (ofFloat x true).val

ofFloat rounding is self-consistent