Floating-Point Representations

This module defines FloatRep, a sign/exponent/mantissa representation of floating-point numbers parameterized by a FloatCfg, together with its rational interpretation coeQ, negation, validity predicates, and an ordering floatrepLe proved equivalent to the order on the underlying rationals.

structure FloatRep (α : FloatCfg) : Type

A sign/exponent/mantissa representation of a (normal) floating-point number in the format α.

• s : Bool

  The sign bit (true for negative).

• e : ℤ

  The exponent.

• m : ℕ

  The mantissa (an offset into [1, 2)).

@[implicit_reducible]

instance instReprFloatRep {C : FloatCfg} : Repr (FloatRep C)

Equations

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

def FloatRep.decEq {C : FloatCfg} (f1 f2 : FloatRep C) : Decidable (f1 = f2)

Decidable equality on FloatRep.

Equations

• f1.decEq f2 = ⋯.mpr instDecidableAnd

def FloatRep.validM {C : FloatCfg} (f : FloatRep C) : Prop

A representation has a valid mantissa when it is below the precision.

Equations

• f.validM = (f.m < C.prec)

def coeQ {C : FloatCfg} : FloatRep C → ℚ

The rational value represented by a FloatRep.

Equations

• coeQ { s := s, e := e, m := m } = (if s = true then -1 else 1) * (↑m / ↑C.prec + 1) * 2 ^ e

theorem coe_q_false_pos {C : FloatCfg} {e : ℤ} {m : ℕ} : 0 < coeQ { s := false, e := e, m := m }

def FloatRep.neg {C : FloatCfg} : FloatRep C → FloatRep C

Negate a representation by flipping its sign bit.

Equations

• { s := s, e := e, m := m }.neg = { s := !s, e := e, m := m }

theorem Flean.neg_neg {C : FloatCfg} : FloatRep.neg ∘ FloatRep.neg = id

theorem neg_invertible {C : FloatCfg} : Function.Bijective FloatRep.neg

theorem neg_valid_m {C : FloatCfg} {f : FloatRep C} : f.neg.validM ↔ f.validM

theorem coe_q_of_neg {C : FloatCfg} (f : FloatRep C) : coeQ f.neg = -coeQ f

theorem neg_false {C : FloatCfg} (e : ℤ) (m : ℕ) : { s := true, e := e, m := m } = { s := false, e := e, m := m }.neg

theorem neg_true {C : FloatCfg} (e : ℤ) (m : ℕ) : { s := false, e := e, m := m } = { s := true, e := e, m := m }.neg

theorem coe_q_true_neg {C : FloatCfg} {e : ℤ} {m : ℕ} : coeQ { s := true, e := e, m := m } < 0

theorem coe_q_nezero {C : FloatCfg} {f : FloatRep C} : coeQ f ≠ 0

theorem floatrep_of_false₁ {C : FloatCfg} (P : FloatRep C → Prop) (h1 : ∀ (f : FloatRep C), P f.neg → P f) (h2 : ∀ (e : ℤ) (m : ℕ), P { s := false, e := e, m := m }) (f : FloatRep C) : P f

theorem floatrep_of_false₂ {C : FloatCfg} (P : FloatRep C → FloatRep C → Prop) (h1 : ∀ (f1 f2 : FloatRep C), P f1.neg f2 → P f1 f2) (h2 : ∀ (f1 f2 : FloatRep C), P f1 f2.neg → P f1 f2) (h3 : ∀ (e e' : ℤ) (m m' : ℕ), P { s := false, e := e, m := m } { s := false, e := e', m := m' }) (f1 f2 : FloatRep C) : P f1 f2

theorem coe_q_of_Cprec {C : FloatCfg} (b : Bool) (e : ℤ) : coeQ { s := b, e := e, m := C.prec } = (if b = true then -1 else 1) * 2 ^ (e + 1)

def FloatRep.validE {C : FloatCfg} (f : FloatRep C) : Prop

A representation has a valid exponent when it lies in [emin, emax].

Equations

• f.validE = (C.emin ≤ f.e ∧ f.e ≤ C.emax)

theorem neg_valid_e {C : FloatCfg} {f : FloatRep C} : f.neg.validE ↔ f.validE

theorem floatrep_e_le_of_coe_q {C : FloatCfg} (f1 f2 : FloatRep C) (vm2 : f2.validM) (h : |coeQ f1| ≤ |coeQ f2|) : f1.e ≤ f2.e

theorem max_mantissa_q (C : FloatCfg) : 1 ≤ 2 - 1 / ↑C.prec ∧ 2 - 1 / ↑C.prec < 2

theorem normal_range {C : FloatCfg} (f : FloatRep C) (ve : f.validE) (vm : f.validM) : C.emin ≤ Int.log 2 |coeQ f| ∧ Int.log 2 |coeQ f| ≤ C.emax

theorem normal_range' {C : FloatCfg} (m : ℕ) (e : ℤ) (vm : m < C.prec) (ve2 : e ≤ C.emax) : |(↑m / ↑C.prec + 1) * 2 ^ e| ≤ (2 - 1 / ↑C.prec) * 2 ^ C.emax

def maxFloatQ (C : FloatCfg) : ℚ

The largest finite rational representable in the format C.

Equations

• maxFloatQ C = (2 - 1 / ↑C.prec) * 2 ^ C.emax

def maxFloatRep (C : FloatCfg) : FloatRep C

The representation of the largest finite float of the format C.

Equations

• maxFloatRep C = { s := false, e := C.emax, m := C.prec - 1 }

theorem coe_q_max_float_rep {C : FloatCfg} : coeQ (maxFloatRep C) = maxFloatQ C

def floatrepLePos {C : FloatCfg} (f1 f2 : FloatRep C) : Prop

Ordering on positive representations: larger exponent, or equal exponent and larger-or-equal mantissa.

Equations

• floatrepLePos f1 f2 = (f1.e < f2.e ∨ f1.e = f2.e ∧ f1.m ≤ f2.m)

def floatrepLePos' {C : FloatCfg} (f1 f2 : FloatRep C) : Prop

An equivalent formulation of floatrepLePos as a conjunction.

Equations

• floatrepLePos' f1 f2 = (f1.e ≤ f2.e ∧ (f1.e = f2.e → f1.m ≤ f2.m))

theorem floatrep_pos_equiv {C : FloatCfg} (f1 f2 : FloatRep C) : floatrepLePos f1 f2 ↔ floatrepLePos' f1 f2

theorem floatrep_le_pos_neg₁ {C : FloatCfg} (f1 f2 : FloatRep C) : floatrepLePos f1.neg f2 ↔ floatrepLePos f1 f2

theorem floatrep_le_pos_neg₂ {C : FloatCfg} (f1 f2 : FloatRep C) : floatrepLePos f1 f2.neg ↔ floatrepLePos f1 f2

theorem floatrep_le_pos_coe_q {C : FloatCfg} (f1 f2 : FloatRep C) (vm1 : f1.m ≤ C.prec) : floatrepLePos f1 f2 → |coeQ f1| ≤ |coeQ f2|

theorem coe_q_le_floatrep_pos {C : FloatCfg} (f1 f2 : FloatRep C) (vm2 : f2.validM) : |coeQ f1| ≤ |coeQ f2| → floatrepLePos f1 f2

theorem floatrep_le_pos_iff_coe_q {C : FloatCfg} (f1 f2 : FloatRep C) (vm1 : f1.m ≤ C.prec) (vm2 : f2.validM) : floatrepLePos f1 f2 ↔ |coeQ f1| ≤ |coeQ f2|

def floatrepLe {C : FloatCfg} (f1 f2 : FloatRep C) : Prop

The full ordering on representations, accounting for signs.

Equations

• floatrepLe f1 f2 = match (f1.s, f2.s) with | (false, false) => floatrepLePos f1 f2 | (false, true) => False | (true, false) => True | (true, true) => floatrepLePos f2.neg f1.neg

theorem floatrep_le_iff_coe_q_le {C : FloatCfg} (f1 f2 : FloatRep C) (vm1 : f1.validM) (vm2 : f2.validM) : floatrepLe f1 f2 ↔ coeQ f1 ≤ coeQ f2