Implementation of floating-point numbers (experimental).

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

Equations

• Int.shift2 a b x = match x with | Int.ofNat e => (a <<< e, 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

theorem FP.FloatCfg.precPos [self : FP.FloatCfg] : 0 < FP.FloatCfg.prec

theorem FP.FloatCfg.precMax [self : FP.FloatCfg] : 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 = max (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

• x.isFinite = match x with | FP.Float.finite a e m a_1 => true | x => false

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

Equations

• FP.toRat x✝ x = match x✝, x with | FP.Float.finite s e m a, x => 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

• x.sign' = match x with | FP.Float.inf s => pure s | FP.Float.nan => ⊤ | FP.Float.finite s e m a => pure s

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

Equations

• x.sign = match x with | FP.Float.inf s => s | FP.Float.nan => false | FP.Float.finite s e m a => s

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

Equations

• x.isZero = match x with | FP.Float.finite a e 0 a_1 => true | x => false

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

Equations

• x.neg = match x with | FP.Float.inf s => FP.Float.inf !s | FP.Float.nan => FP.Float.nan | FP.Float.finite s e m f => FP.Float.finite (!s) e m f

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

Equations

• FP.divNatLtTwoPow n d x = match x with | Int.ofNat e => decide (n < d <<< e) | 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 = let m' := m.succ; if ss : m'.size = m.size then FP.Float.finite false e m' ⋯ else if h : e = ↑FP.emax then FP.Float.inf false else FP.Float.finite false e.succ m'.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.

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

Equations

• FP.nextUp x = match x with | FP.Float.finite false e m f => FP.nextUpPos e m f | FP.Float.finite true e m f => (FP.nextDnPos e m f).neg | f => f

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

Equations

• FP.nextDn x = match x with | FP.Float.finite false e m f => FP.nextDnPos e m f | FP.Float.finite true e m f => (FP.nextUpPos e m f).neg | f => f

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

Equations

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

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

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

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 : FP.Float) (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

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

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.