Mathematical semantics of P3109 rational arithmetic

Finite arithmetic is exact rational arithmetic, and rational embedding into the reals preserves the complete expression. The algebraic results describe arithmetic before rounding. The decoding theorems connect the public executable operations to one report projection of that exact result.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.add_comm (left right : Numerics.NumericalValue ℚ) : add left right = add right left

Exact closed addition is commutative, including exceptional operands.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.mul_comm (left right : Numerics.NumericalValue ℚ) : mul left right = mul right left

Exact closed multiplication is commutative, including zero times infinity.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.add_assoc (left middle right : Numerics.NumericalValue ℚ) : add (add left middle) right = add left (add middle right)

Exact closed addition is associative, and opposite infinities stay indeterminate.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sub_self (value : ℚ) : sub (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.finite value) = Numerics.NumericalValue.finite 0

Subtracting a finite datum from itself gives the unique exact zero.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_zero (value : Numerics.NumericalValue ℚ) : div value (Numerics.NumericalValue.finite 0) = nan

Zero denominators are NaN, even for infinite numerators.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_infinity (value : ℚ) (negative : Bool) : div (Numerics.NumericalValue.finite value) (Numerics.NumericalValue.infinity negative) = Numerics.NumericalValue.finite 0

Every finite numerator divided by either infinity gives the unique zero.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_mul_cancel (left right : ℚ) (hright : right ≠ 0) : mul (div (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) (Numerics.NumericalValue.finite right) = Numerics.NumericalValue.finite left

Finite nonzero division cancels before any destination rounding.

@[simp]

theorem FloatLib.Floats.Formats.P3109.Arithmetic.fma_finite (left right addend : ℚ) : fma (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) (Numerics.NumericalValue.finite addend) = Numerics.NumericalValue.finite (left * right + addend)

Finite fused multiply-add retains the whole rational expression.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.faa_eq_add_add (left middle right : Numerics.NumericalValue ℚ) : faa left middle right = add left (add middle right)

Fused add-add is independent of the grouping of the exact additions.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.add_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (add (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left + ↑right)

Rational addition embeds as addition in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.sub_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (sub (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left - ↑right)

Rational subtraction embeds as subtraction in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.mul_finite_real (left right : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (mul (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left * ↑right)

Rational multiplication embeds as multiplication in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.div_finite_real (left right : ℚ) (hright : right ≠ 0) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (div (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right)) = Numerics.NumericalValue.finite (↑left / ↑right)

Nonzero rational division embeds as division in the reals.

theorem FloatLib.Floats.Formats.P3109.Arithmetic.fma_finite_real (left right addend : ℚ) : Numerics.NumericalValue.map (fun (value : ℚ) => ↑value) (fma (Numerics.NumericalValue.finite left) (Numerics.NumericalValue.finite right) (Numerics.NumericalValue.finite addend)) = Numerics.NumericalValue.finite (↑left * ↑right + ↑addend)

FMA computes the real expression with no rounded intermediate product.

theorem FloatLib.Floats.ExecFloat.P3109.decode_unary {source : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (value : P3109 source) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (unary operation value target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (operation value.toClosedRat))

The executable unary operation decodes to one projection of its exact closed result.

theorem FloatLib.Floats.ExecFloat.P3109.decode_binary {leftFormat rightFormat : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (binary operation left right target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (operation left.toClosedRat right.toClosedRat))

The executable binary operation decodes to one projection of its exact closed result.

theorem FloatLib.Floats.ExecFloat.P3109.decode_ternary {leftFormat rightFormat thirdFormat : Formats.P3109.Format} (operation : Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ → Numerics.NumericalValue ℚ) (left : P3109 leftFormat) (right : P3109 rightFormat) (third : P3109 thirdFormat) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) : Formats.P3109.Format.SameDatum (ternary operation left right third target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (operation left.toClosedRat right.toClosedRat third.toClosedRat))

The executable fused operation decodes to one projection of the whole exact expression.

theorem FloatLib.Floats.ExecFloat.P3109.decode_fma_finite {format : Formats.P3109.Format} (left right addend : P3109 format) (target : Formats.P3109.Format) (mode : Formats.P3109.RoundingMode) (saturation : Formats.P3109.SaturationMode) (x y z : ℚ) (hleft : left.toClosedRat = Numerics.NumericalValue.finite x) (hright : right.toClosedRat = Numerics.NumericalValue.finite y) (haddend : addend.toClosedRat = Numerics.NumericalValue.finite z) : Formats.P3109.Format.SameDatum (left.fma right addend target mode saturation).decode (target.projectRatValue { rounding := mode, saturation := saturation } (Numerics.NumericalValue.finite (x * y + z)))

Finite FMA is one projection of the exact rational product plus addend.