Implementation of floating-point numbers (experimental).

def Int.shift2 (a b : ℕ) : ℤ → ℕ × ℕ

Equations

• Int.shift2 a b (Int.ofNat e) = (a <<< e, b)
• Int.shift2 a b (Int.negSucc e) = (a, b <<< e.succ)

inductive FP.RMode : Type

• NE : FP.RMode

instance FP.instInhabitedRMode : Inhabited FP.RMode

Equations

• FP.instInhabitedRMode = { default := FP.RMode.NE }

class FP.FloatCfg : Type

• prec : ℕ
• emax : ℕ
• precPos : 0 < FP.FloatCfg.prec
• precMax : FP.FloatCfg.prec ≤ FP.FloatCfg.emax

def FP.prec [C : FP.FloatCfg] : ℕ

Equations

• FP.prec = FP.FloatCfg.prec

def FP.emax [C : FP.FloatCfg] : ℕ

Equations

• FP.emax = FP.FloatCfg.emax

def FP.emin [C : FP.FloatCfg] : ℤ

Equations

• FP.emin = 1 - ↑FP.FloatCfg.emax

def FP.ValidFinite [C : FP.FloatCfg] (e : ℤ) (m : ℕ) : Prop

Equations

• FP.ValidFinite e m = (FP.emin ≤ e + ↑FP.prec - 1 ∧ e + ↑FP.prec - 1 ≤ ↑FP.emax ∧ e = (e + ↑m.size - ↑FP.prec) ⊔ FP.emin)

instance FP.decValidFinite [C : FP.FloatCfg] (e : ℤ) (m : ℕ) : Decidable (FP.ValidFinite e m)

Equations

• FP.decValidFinite e m = id inferInstance

inductive FP.Float [C : FP.FloatCfg] : Type

• inf [C : FP.FloatCfg] : Bool → FP.Float
• nan [C : FP.FloatCfg] : FP.Float
• finite [C : FP.FloatCfg] : Bool → (e : ℤ) → (m : ℕ) → FP.ValidFinite e m → FP.Float

def FP.Float.isFinite [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.finite a e m a_1).isFinite = true
• x✝.isFinite = false

def FP.toRat [C : FP.FloatCfg] (f : FP.Float) : f.isFinite = true → ℚ

Equations

• FP.toRat (FP.Float.finite s e m a) x_2 = match Int.shift2 m 1 e with | (n, d) => let r := mkRat (↑n) d; if s = true then -r else r

theorem FP.Float.Zero.valid [C : FP.FloatCfg] : FP.ValidFinite FP.emin 0

def FP.Float.zero [C : FP.FloatCfg] (s : Bool) : FP.Float

Equations

• FP.Float.zero s = FP.Float.finite s FP.emin 0 ⋯

instance FP.instInhabitedFloat [C : FP.FloatCfg] : Inhabited FP.Float

Equations

• FP.instInhabitedFloat = { default := FP.Float.zero true }

def FP.Float.sign' [C : FP.FloatCfg] : FP.Float → Semiquot Bool

Equations

• (FP.Float.inf s).sign' = pure s
• FP.Float.nan.sign' = ⊤
• (FP.Float.finite s e m a).sign' = pure s

def FP.Float.sign [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.inf s).sign = s
• FP.Float.nan.sign = false
• (FP.Float.finite s e m a).sign = s

def FP.Float.isZero [C : FP.FloatCfg] : FP.Float → Bool

Equations

• (FP.Float.finite a e 0 a_1).isZero = true
• x✝.isZero = false

def FP.Float.neg [C : FP.FloatCfg] : FP.Float → FP.Float

Equations

• (FP.Float.inf s).neg = FP.Float.inf !s
• FP.Float.nan.neg = FP.Float.nan
• (FP.Float.finite s e m a).neg = FP.Float.finite (!s) e m a

def FP.divNatLtTwoPow (n d : ℕ) : ℤ → Bool

Equations

• FP.divNatLtTwoPow n d (Int.ofNat e) = decide (n < d <<< e)
• FP.divNatLtTwoPow n d (Int.negSucc e) = decide (n <<< e.succ < d)

unsafe def FP.ofPosRatDn [C : FP.FloatCfg] (n d : ℕ+) : FP.Float × Bool

Equations

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

unsafe def FP.nextUpPos [C : FP.FloatCfg] (e : ℤ) (m : ℕ) (v : FP.ValidFinite e m) : FP.Float

Equations

• FP.nextUpPos e m v = if ss : m.succ.size = m.size then FP.Float.finite false e m.succ ⋯ else if h : e = ↑FP.emax then FP.Float.inf false else FP.Float.finite false e.succ m.succ.div2 ⋯

unsafe def FP.nextDnPos [C : FP.FloatCfg] (e : ℤ) (m : ℕ) (v : FP.ValidFinite e m) : FP.Float

Equations

• One or more equations did not get rendered due to their size.
• FP.nextDnPos e 0 v_2 = FP.nextUpPos FP.emin 0 ⋯

unsafe def FP.nextUp [C : FP.FloatCfg] : FP.Float → FP.Float

Equations

• FP.nextUp (FP.Float.finite false e m f) = FP.nextUpPos e m f
• FP.nextUp (FP.Float.finite true e m f) = (FP.nextDnPos e m f).neg
• FP.nextUp x✝ = x✝

unsafe def FP.nextDn [C : FP.FloatCfg] : FP.Float → FP.Float

Equations

• FP.nextDn (FP.Float.finite false e m f) = FP.nextDnPos e m f
• FP.nextDn (FP.Float.finite true e m f) = (FP.nextUpPos e m f).neg
• FP.nextDn x✝ = x✝

unsafe def FP.ofRatUp [C : FP.FloatCfg] : ℚ → FP.Float

Equations

• FP.ofRatUp { num := 0, den := den, den_nz := den_nz, reduced := reduced } = FP.Float.zero false
• FP.ofRatUp { num := Int.ofNat n.succ, den := d, den_nz := h, reduced := reduced } = match FP.ofPosRatDn n.succPNat ⟨d, ⋯⟩ with | (f, exact) => if exact = true then f else FP.nextUp f
• FP.ofRatUp { num := Int.negSucc n, den := d, den_nz := h, reduced := reduced } = (FP.ofPosRatDn n.succPNat ⟨d, ⋯⟩).1.neg

unsafe def FP.ofRatDn [C : FP.FloatCfg] (r : ℚ) : FP.Float

Equations

• FP.ofRatDn r = (FP.ofRatUp (-r)).neg

unsafe def FP.ofRat [C : FP.FloatCfg] : FP.RMode → ℚ → FP.Float

Equations

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

instance FP.Float.instNeg [C : FP.FloatCfg] : Neg FP.Float

Equations

• FP.Float.instNeg = { neg := FP.Float.neg }

unsafe def FP.Float.add [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float

Equations

• FP.Float.add mode FP.Float.nan x✝ = FP.Float.nan
• FP.Float.add mode x✝ FP.Float.nan = FP.Float.nan
• FP.Float.add mode (FP.Float.inf true) (FP.Float.inf false) = FP.Float.nan
• FP.Float.add mode (FP.Float.inf false) (FP.Float.inf true) = FP.Float.nan
• FP.Float.add mode (FP.Float.inf s₁) x✝ = FP.Float.inf s₁
• FP.Float.add mode x✝ (FP.Float.inf s₂) = FP.Float.inf s₂
• FP.Float.add mode (FP.Float.finite s₁ e₁ m₁ v₁) (FP.Float.finite s₂ e₂ m₂ v₂) = FP.ofRat mode (FP.toRat (FP.Float.finite s₁ e₁ m₁ v₁) ⋯ + FP.toRat (FP.Float.finite s₂ e₂ m₂ v₂) ⋯)

unsafe instance FP.Float.instAdd [C : FP.FloatCfg] : Add FP.Float

Equations

• FP.Float.instAdd = { add := FP.Float.add FP.RMode.NE }

unsafe def FP.Float.sub [C : FP.FloatCfg] (mode : FP.RMode) (f1 f2 : FP.Float) : FP.Float

Equations

• FP.Float.sub mode f1 f2 = FP.Float.add mode f1 (-f2)

unsafe instance FP.Float.instSub [C : FP.FloatCfg] : Sub FP.Float

Equations

• FP.Float.instSub = { sub := FP.Float.sub FP.RMode.NE }

unsafe def FP.Float.mul [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float

Equations

• FP.Float.mul mode FP.Float.nan x✝ = FP.Float.nan
• FP.Float.mul mode x✝ FP.Float.nan = FP.Float.nan
• FP.Float.mul mode (FP.Float.inf s₁) x✝ = if x✝.isZero = true then FP.Float.nan else FP.Float.inf (s₁ ^^ x✝.sign)
• FP.Float.mul mode x✝ (FP.Float.inf s₂) = if x✝.isZero = true then FP.Float.nan else FP.Float.inf (x✝.sign ^^ s₂)
• FP.Float.mul mode (FP.Float.finite s₁ e₁ m₁ v₁) (FP.Float.finite s₂ e₂ m₂ v₂) = FP.ofRat mode (FP.toRat (FP.Float.finite s₁ e₁ m₁ v₁) ⋯ * FP.toRat (FP.Float.finite s₂ e₂ m₂ v₂) ⋯)

unsafe def FP.Float.div [C : FP.FloatCfg] (mode : FP.RMode) : FP.Float → FP.Float → FP.Float

Equations

• One or more equations did not get rendered due to their size.
• FP.Float.div mode FP.Float.nan x✝ = FP.Float.nan
• FP.Float.div mode x✝ FP.Float.nan = FP.Float.nan
• FP.Float.div mode (FP.Float.inf a) (FP.Float.inf a_1) = FP.Float.nan
• FP.Float.div mode (FP.Float.inf s₁) x✝ = FP.Float.inf (s₁ ^^ x✝.sign)
• FP.Float.div mode x (FP.Float.inf s₂) = FP.Float.zero (x.sign ^^ s₂)