TorchLean API

Docs HomeInstallationGuideExamplesGraphsTools

FloatLib.Floats.Formats.FixedPoint.Exact.Proof

Rational semantics and correctness of exact fixed point #

A coefficient m with d fractional radix digits denotes m / β^d; the numerical system and erased proof views relate the runtime operations to rational arithmetic. Common-scale addition is exact; multiplication changes the scale to the sum of the operand fractional-digit counts.

Import Exact.Runtime for the representation and executable functions. The configured family uses the refinement theorems here to provide the same operations through ExecFloat.

source
def FloatLib.Floats.Formats.FixedPoint.numericalSystem (radix : Numerics.Radix) (fractionalDigits : ℕ) :
Numerics.NumericalSystem

The exact rational numerical system at one fixed radix and scale.

Instances For
    source
    @[reducible, inline]
    abbrev FloatLib.Floats.Formats.FixedPoint.At (radix : Numerics.Radix) (fractionalDigits : ℕ) (value : Numerics.NumericalValue ℚ) :
    Type

    A fixed-point code with an erased proof of its complete denotation.

    Instances For
      source
      @[reducible, inline]
      abbrev FloatLib.Floats.Formats.FixedPoint.AtFinite (radix : Numerics.Radix) (fractionalDigits : ℕ) (value : ℚ) :
      Type

      A fixed-point code with an erased proof of its exact rational value.

      Instances For

        Arithmetic refinement #

        source
        @[simp]
        theorem FloatLib.Floats.Formats.FixedPoint.Code.toRat_add {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : Code radix fractionalDigits) :
        (left.add right).toRat = left.toRat + right.toRat

        Decoding exact fixed-point addition gives rational addition.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.FixedPoint.Code.toRat_neg {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : Code radix fractionalDigits) :
        value.neg.toRat = -value.toRat

        Decoding exact fixed-point negation gives rational negation.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.FixedPoint.Code.toRat_sub {radix : Numerics.Radix} {fractionalDigits : ℕ} (left right : Code radix fractionalDigits) :
        (left.sub right).toRat = left.toRat - right.toRat

        Decoding exact fixed-point subtraction gives rational subtraction.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.FixedPoint.Code.toRat_mul {radix : Numerics.Radix} {p q : ℕ} (left : Code radix p) (right : Code radix q) :
        (left.mul right).toRat = left.toRat * right.toRat

        Decoding scale-composing fixed-point multiplication gives rational multiplication.

        source
        @[simp]
        theorem FloatLib.Floats.Formats.FixedPoint.numericalSystem_represents_iff {radix : Numerics.Radix} {fractionalDigits : ℕ} (value : Code radix fractionalDigits) (scalar : ℚ) :
        (numericalSystem radix fractionalDigits).Represents value scalar ↔ value.toRat = scalar

        Representation in the fixed-point numerical system is equality of decoded rationals.

        source
        theorem FloatLib.Floats.Formats.FixedPoint.add_refines {radix : Numerics.Radix} {fractionalDigits : ℕ} :
        Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits) (numericalSystem radix fractionalDigits) (numericalSystem radix fractionalDigits) Code.add fun (left right : ℚ) => left + right

        Fixed-point addition is a finite refinement of rational addition.

        source
        theorem FloatLib.Floats.Formats.FixedPoint.neg_refines {radix : Numerics.Radix} {fractionalDigits : ℕ} :
        Numerics.Operation.Finite1 (numericalSystem radix fractionalDigits) (numericalSystem radix fractionalDigits) Code.neg fun (value : ℚ) => -value

        Fixed-point negation exactly refines rational negation.

        source
        theorem FloatLib.Floats.Formats.FixedPoint.sub_refines {radix : Numerics.Radix} {fractionalDigits : ℕ} :
        Numerics.Operation.Finite2 (numericalSystem radix fractionalDigits) (numericalSystem radix fractionalDigits) (numericalSystem radix fractionalDigits) Code.sub fun (left right : ℚ) => left - right

        Fixed-point subtraction exactly refines rational subtraction.

        source
        theorem FloatLib.Floats.Formats.FixedPoint.mul_refines {radix : Numerics.Radix} {p q : ℕ} :
        Numerics.Operation.Finite2 (numericalSystem radix p) (numericalSystem radix q) (numericalSystem radix (p + q)) Code.mul fun (left right : ℚ) => left * right

        Multiplication composes the two fixed scales and refines rational multiplication exactly.