Documentation

LeanPool.Flean.Rounding

Rounding Rationals to Floating-Point Representations #

This module defines normalization of a FloatRep, the roundDown/roundf rounding maps from rationals to representations under an IntRounder, and the correctness and error-bound results (such as roundf_close) controlling the distance between a rational and its rounded floating-point value.

def FloatRep.normalize {C : FloatCfg} (f : FloatRep C) :

Normalize a representation whose mantissa has reached the precision by incrementing the exponent and zeroing the mantissa.

Equations

f.normalize = if f.m = C.prec then { s := f.s, e := f.e + 1, m := 0 } else f

Instances For

theorem normalize_valid {C : FloatCfg} (f : FloatRep C) (h : f.m ≤ C.prec) :

f.normalize.validM

theorem coe_normalize {C : FloatCfg} (f : FloatRep C) (h : f.m ≤ C.prec) :

coeQ f.normalize = coeQ f

theorem normalize_neg {C : FloatCfg} (f : FloatRep C) :

f.neg.normalize = f.normalize.neg

def roundf {C : FloatCfg} (r : IntRounder) (q : ℚ) :

Round a rational to a normal representation using the rounder r.

Equations

roundf r q = { s := decide (q < 0), e := Int.log 2 |q|, m := r (decide (q < 0)) ((|q| * (2 ^ Int.log 2 |q|)⁻¹ - 1) * ↑C.prec) }.normalize

Instances For

theorem roundf_neg {C : FloatCfg} (r : IntRounder) {q : ℚ} (h : q ≠ 0) :

roundf r.neg (-q) = (roundf r q).neg

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

P r f

theorem roundf_coe {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (f : FloatRep C) (h : f.validM) :

roundf r (coeQ f) = f

def roundDown {C : FloatCfg} :

ℚ → FloatRep C

Round a rational down (toward zero in mantissa) to a representation.

Equations

roundDown = roundf round0

Instances For

theorem round0_neg :

IntRounder.neg round0 = round0

theorem round_down_neg {C : FloatCfg} (q : ℚ) (h : q ≠ 0) :

roundDown (-q) = (roundDown q).neg

theorem round_down_coe {C : FloatCfg} (f : FloatRep C) (h : f.validM) :

roundDown (coeQ f) = f

theorem coe_q_inj_valid {C : FloatCfg} {f1 f2 : FloatRep C} (h : f1.validM) (h' : f2.validM) :

coeQ f1 = coeQ f2 → f1 = f2

theorem roundf_almost_valid {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) (h : q ≠ 0) :

r (decide (q < 0)) ((|q| * (2 ^ Int.log 2 |q|)⁻¹ - 1) * ↑C.prec) ≤ C.prec

theorem roundf_valid {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) (h : q ≠ 0) :

(roundf r q).validM

theorem round_down_valid {C : FloatCfg} (q : ℚ) (h : q ≠ 0) :

(roundDown q).validM

theorem roundf_of_pos {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) (h : 0 < q) :

0 < coeQ (roundf r q)

theorem round_down_of_pos {C : FloatCfg} (q : ℚ) (h : 0 < q) :

0 < coeQ (roundDown q)

theorem roundf_of_pos' {C : FloatCfg} (r : IntRounder) (q : ℚ) (h : 0 < q) :

(roundf r q).s = false

theorem round_down_of_pos' {C : FloatCfg} (q : ℚ) (h : 0 < q) :

(roundDown q).s = false

theorem roundf_of_neg {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q : ℚ) (h : q < 0) :

coeQ (roundf r q) < 0

theorem round_down_of_neg {C : FloatCfg} (q : ℚ) (h : q < 0) :

coeQ (roundDown q) < 0

theorem roundf_of_neg' {C : FloatCfg} (r : IntRounder) (q : ℚ) (h : q < 0) :

(roundf r q).s = true

theorem round_down_of_neg' {C : FloatCfg} (q : ℚ) (h : q < 0) :

(roundDown q).s = true

theorem le_roundf_of_le {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] (q1 q2 : ℚ) (q1_nezero : q1 ≠ 0) (q2_nezero : q2 ≠ 0) :

q1 ≤ q2 → coeQ (roundf r q1) ≤ coeQ (roundf r q2)

theorem le_round_down_of_le {C : FloatCfg} (q1 q2 : ℚ) (q1_nezero : q1 ≠ 0) (q2_nezero : q2 ≠ 0) :

q1 ≤ q2 → coeQ (roundDown q1) ≤ coeQ (roundDown q2)

theorem round_down_false_of_le_coe_aux {C : FloatCfg} (q : ℚ) (e : ℤ) (m : ℕ) (vm : m < C.prec) (q_pos : 0 < q) (h : q ≤ coeQ { s := false, e := e, m := m }) :

coeQ (roundDown q) ≤ coeQ { s := false, e := e, m := m }

theorem e_le_iff_log {C : FloatCfg} (f1 f2 : FloatRep C) (vm1 : f1.validM) (vm2 : f2.validM) :

f1.e ≤ f2.e ↔ Int.log 2 |coeQ f1| ≤ Int.log 2 |coeQ f2|

def roundFunction (R : Rounding) (s : Bool) (q : ℚ) :

The IntRounder selected by the rounding mode in scope.

Equations

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

Instances For

instance instValidRounderRoundFunction (R : Rounding) :

ValidRounder (roundFunction R)

def roundRep {C : FloatCfg} [R : Rounding] (q : ℚ) :

Round a rational to a representation using the rounding mode in scope.

Equations

roundRep q = roundf (roundFunction R) q

Instances For

theorem round_rep_coe {C : FloatCfg} [R : Rounding] (f : FloatRep C) (h : f.validM) :

roundRep (coeQ f) = f

theorem round_valid_m {C : FloatCfg} [R : Rounding] (q : ℚ) (q_nezero : q ≠ 0) :

(roundRep q).validM

theorem roundf_min_abs_e {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (h : q ≠ 0) :

Int.log 2 |q| ≤ (roundf r |q|).e

theorem round_min_e {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (h : q ≠ 0) :

Int.log 2 |q| ≤ (roundf r q).e

theorem round_min_e' {C : FloatCfg} [R : Rounding] (q : ℚ) (h : q ≠ 0) :

Int.log 2 |q| ≤ (roundRep q).e

theorem convert_rep_strict_mono {C : FloatCfg} (q : ℚ) :

StrictMono fun (x : ℚ) => (1 + x / ↑C.prec) * 2 ^ Int.log 2 |q|

theorem q_le_floatrep_ceil {C : FloatCfg} {q : ℚ} (h : q ≠ 0) :

|q| ≤ (1 + ↑⌈(|q| * (2 ^ Int.log 2 |q|)⁻¹ - 1) * ↑C.prec⌉.natAbs / ↑C.prec) * 2 ^ Int.log 2 |q|

theorem floatrep_floor_le_q {C : FloatCfg} {q : ℚ} (q_nezero : q ≠ 0) :

(↑⌊(|q| * (2 ^ Int.log 2 |q|)⁻¹ - 1) * ↑C.prec⌋.natAbs / ↑C.prec + 1) * 2 ^ Int.log 2 |q| ≤ |q|

theorem roundf_down_le {C : FloatCfg} {q : ℚ} (q_nezero : q ≠ 0) :

coeQ (roundf rounddown q) ≤ q

theorem le_roundf_up {C : FloatCfg} {q : ℚ} (q_nezero : q ≠ 0) :

q ≤ coeQ (roundf roundup q)

theorem roundf_up_minus_down {C : FloatCfg} {q : ℚ} (q_nezero : q ≠ 0) :

coeQ (roundf roundup q) - coeQ (roundf rounddown q) ≤ 2 ^ Int.log 2 |q| / ↑C.prec

theorem round_max_e {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (q_nezero : q ≠ 0) (e : ℤ) (h : |q| ≤ (2 - 1 / ↑C.prec) * 2 ^ e) :

(roundf r q).e ≤ e

theorem roundf_in_range {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (q_nezero : q ≠ 0) (h : |q| ≤ maxFloatQ C) :

(roundf r q).e ≤ C.emax

theorem round_rep_in_range {C : FloatCfg} [R : Rounding] {q : ℚ} (q_nezero : q ≠ 0) (h : |q| ≤ maxFloatQ C) :

(roundRep q).e ≤ C.emax

theorem roundf_eq_up_down {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (q_nezero : q ≠ 0) :

roundf r q = roundf rounddown q ∨ roundf r q = roundf roundup q

theorem roundf_close {C : FloatCfg} (r : IntRounder) [rh : ValidRounder r] {q : ℚ} (q_nezero : q ≠ 0) :

|q - coeQ (roundf r q)| ≤ 2 ^ Int.log 2 |q| / ↑C.prec

theorem roundf_near_close {C : FloatCfg} {q : ℚ} (q_nezero : q ≠ 0) :

|q - coeQ (roundf roundnearest q)| ≤ 2 ^ (Int.log 2 |q| - 1) / ↑C.prec