Exact semantics with representation metadata

ExactSemantics supplements a NumericalSystem with a decoder that can retain signed zero, NaN metadata, tags, or block structure. It is used in proofs; executable arithmetic calls the concrete family functions directly.

structure FloatLib.Numerics.ExactSemantics (S : NumericalSystem) : Type (max (max (u + 1) u_1) u_2)

A richer exact interpretation that forgets coherently to a numerical system's denotation.

• Exact : Type u

  Representation-specific exact semantic domain.

• decode : S.Code → self.Exact

  Exact interpretation of one runtime code.

• forget : self.Exact → NumericalValue S.Scalar

  Forget representation-specific distinctions.

• forget_decode (code : S.Code) : self.forget (self.decode code) = S.denote code

  Exact decoding agrees with the common numerical interpretation.

@[reducible, inline]

abbrev FloatLib.Numerics.ExactSemantics.At {S : NumericalSystem} (E : ExactSemantics S) (value : E.Exact) : Type u_1

A runtime code bundled with an erased proof of its richer exact interpretation.

@[inline]

def FloatLib.Numerics.ExactSemantics.ofCode {S : NumericalSystem} (E : ExactSemantics S) (code : S.Code) : E.At (E.decode code)

Attach the exact interpretation computed from an existing runtime code.

@[simp]

theorem FloatLib.Numerics.ExactSemantics.decode_eq {S : NumericalSystem} (E : ExactSemantics S) {value : E.Exact} (code : E.At value) : E.decode code.val = value

The bundled runtime code has its indexed exact interpretation.

@[inline]

def FloatLib.Numerics.ExactSemantics.toAt {S : NumericalSystem} (E : ExactSemantics S) {value : E.Exact} (code : E.At value) : S.At (E.forget value)

Forget exact distinctions while retaining the same runtime code.

def FloatLib.Numerics.ExactSemantics.ofDenote (S : NumericalSystem) : ExactSemantics S

Use a system's complete denotation as its exact interpretation.