Constructors and projections for exact proof views

These definitions attach exact, total, or finite semantic evidence to an executable model and move between the three proof-indexed views without changing its runtime bits.

The views let later theorems ask for precisely the exceptional-value hypothesis they need instead of carrying a record of unrelated facts. Constructors and projections pass through the underlying model value; their semantic proofs are erased.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact.ofCode {fmt : FloatFormat} (x : Model fmt) : AtExact fmt x.exactValue

Attach the exact total interpretation computed from an executable value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact.ofDyadic {fmt : FloatFormat} (x : Model fmt) (value : Numerics.Dyadic) (hvalue : x.toDyadic? = some value) : AtExact fmt (ExactValue.finite value)

Attach a known exact finite dyadic interpretation.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact.denote {fmt : FloatFormat} {v : ExactValue} (x : AtExact fmt v) : exactValue ↑x = v

The bundled executable value has its indexed exact interpretation.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact.toValue {fmt : FloatFormat} {v : ExactValue} (x : AtExact fmt v) : AtValue fmt v.toNumericalValue

Forget exact encoding distinctions while retaining the same executable value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtExact.toAt {fmt : FloatFormat} {value : Numerics.Dyadic} (x : AtExact fmt (ExactValue.finite value)) : At fmt value.toReal

A finite exact refinement induces the corresponding real-valued refinement.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.OutcomeAt.ofOutcome {fmt : FloatFormat} (outcome : IEEEOutcome fmt) : OutcomeAt fmt outcome.value.exactValue outcome.status

Attach the exact value and status computed by an executable IEEE outcome.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.OutcomeAt.denote {fmt : FloatFormat} {v : ExactValue} {status : IEEEStatus} (outcome : OutcomeAt fmt v status) : (↑outcome).value.exactValue = v

The bundled outcome's value has its indexed exact interpretation.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.OutcomeAt.status_eq {fmt : FloatFormat} {v : ExactValue} {status : IEEEStatus} (outcome : OutcomeAt fmt v status) : (↑outcome).status = status

The bundled outcome has its indexed IEEE exception status.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.OutcomeAt.toAtExact {fmt : FloatFormat} {v : ExactValue} {status : IEEEStatus} (outcome : OutcomeAt fmt v status) : AtExact fmt v

Project the outcome's value to its exact proof-indexed view.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.ofCode {fmt : FloatFormat} (x : Model fmt) : AtValue fmt x.toNumericalValue

Attach the exact total interpretation of an executable value.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.ofFinite {fmt : FloatFormat} (x : Model fmt) (hfinite : x.isFinite = true) : AtValue fmt (Numerics.NumericalValue.finite x.toReal)

Attach the finite interpretation of an executable value known to be finite.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.ofInf {fmt : FloatFormat} (x : Model fmt) (hinf : x.isInf = true) : AtValue fmt (Numerics.NumericalValue.infinity x.signBit)

Attach the signed-infinity interpretation of an executable value known to be infinite.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.ofNaN {fmt : FloatFormat} (x : Model fmt) (hnan : x.isNaN = true) : AtValue fmt (Numerics.NumericalValue.exceptional (Numerics.ExceptionalValue.nan (some x.fracField)))

Attach the payload-preserving interpretation of an executable value known to be a NaN.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.posInf (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : AtValue fmt (Numerics.NumericalValue.infinity false)

Positive infinity with its total interpretation in a conventional IEEE format.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.negInf (fmt : FloatFormat) (hfmt : fmt.isIEEE = true) : AtValue fmt (Numerics.NumericalValue.infinity true)

Negative infinity with its total interpretation in a conventional IEEE format.

@[simp]

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.denote {fmt : FloatFormat} {v : Numerics.NumericalValue ℝ} (x : AtValue fmt v) : toNumericalValue ↑x = v

The bundled executable value has its indexed total interpretation.

theorem FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.numericalSystem_denote {fmt : FloatFormat} {v : Numerics.NumericalValue ℝ} (x : AtValue fmt v) : (numericalSystem fmt).denote ↑x = v

The bundled value has the same interpretation through the generic numerical-system adapter.

@[inline]

def FloatLib.Floats.Formats.BinaryInterchange.Model.AtValue.toAt {fmt : FloatFormat} {r : ℝ} (x : AtValue fmt (Numerics.NumericalValue.finite r)) : At fmt r

A finite total refinement is the ordinary real-indexed refinement.