Flocq-style generic formats as ordinary FloatLib formats

The radix/exponent-function model of FloatRep supplies a representation-independent EncodedFormat interface.

The runtime code is a canonical integer-mantissa/integer-exponent pair. Lean erases its proof of canonicality, and its denotation is the corresponding real number. The central theorem representable_iff_genericFormat proves that common-system representability coincides with genericFormat.

The definitions mirror the separation in Flocq between:

• generic_format, which characterizes representable real values,
• Valid_exp, which constrains exponent-selection functions,
• a rounding operator proved to return a generic-format value.

Primary references:

• S. Boldo and G. Melquiond, “Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq,” ARITH 2011, pp. 243–252, §III-D, DOI 10.1109/ARITH.2011.40.
• Flocq 4.2.2 release, src/Core/Generic_fmt.v, definitions generic_format and Valid_exp: https://flocq.gitlabpages.inria.fr/releases/flocq-4.2.2.tar.gz.
• Flocq project documentation: https://flocq.gitlabpages.inria.fr/flocq/.

inductive FloatLib.Floats.Formats.Flocq.GenericFormat (β : Numerics.Radix) (fexp : ℤ → ℤ) : Type

Type-level identity of the generic radix/exponent-function format.

The constructor carries no format data. The radix and exponent function are type parameters, so specialized users do not pass a runtime descriptor through arithmetic kernels.

• format {β : Numerics.Radix} {fexp : ℤ → ℤ} : GenericFormat β fexp

@[reducible, inline]

abbrev FloatLib.Floats.Formats.Flocq.CanonicalCode (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : Type

Canonical mantissa/exponent codes of a valid Flocq-style generic format.

@[instance_reducible]

instance FloatLib.Floats.Formats.Flocq.instEncodedFormatGenericFormatOfValidExp (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : Numerics.EncodedFormat (GenericFormat β fexp)

@[instance_reducible]

noncomputable instance FloatLib.Floats.Formats.Flocq.instFormatSemanticsGenericFormat (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : Numerics.FormatSemantics (GenericFormat β fexp)

@[simp]

theorem FloatLib.Floats.Formats.Flocq.represents_iff (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (code : Numerics.FormatCode (GenericFormat β fexp)) (x : ℝ) : Numerics.FormatRepresents (GenericFormat β fexp) code x ↔ toReal ↑code = x

A canonical code represents exactly the real obtained from its mantissa and exponent.

theorem FloatLib.Floats.Formats.Flocq.representable_iff_genericFormat (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) : (Numerics.formatSystem (GenericFormat β fexp)).Representable x ↔ genericFormat β fexp x

Common FloatLib representability coincides with the Flocq-style generic_format predicate.

noncomputable def FloatLib.Floats.Formats.Flocq.encodeGeneric (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) (hx : genericFormat β fexp x) : Numerics.FormatCode (GenericFormat β fexp)

Choose a canonical code for a value already known to belong to the generic format.

It is noncomputable and meant for proofs. Concrete fixed-precision format families supply their own executable packing kernels.

theorem FloatLib.Floats.Formats.Flocq.encodeGeneric_represents (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (x : ℝ) (hx : genericFormat β fexp x) : Numerics.FormatRepresents (GenericFormat β fexp) (encodeGeneric β fexp x hx) x

encodeGeneric denotes the real value from which it was chosen.

noncomputable def FloatLib.Floats.Formats.Flocq.roundCode (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (mode : BinaryInterchange.Model.IEEERoundingMode) (x : ℝ) : Numerics.FormatCode (GenericFormat β fexp)

Round a real input and choose a canonical code for the rounded generic-format value.

theorem FloatLib.Floats.Formats.Flocq.roundCode_represents (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] (mode : BinaryInterchange.Model.IEEERoundingMode) (x : ℝ) : Numerics.FormatRepresents (GenericFormat β fexp) (roundCode β fexp mode x) (round (roundingFunction mode) x)

The selected code denotes the rounded result in the given direction.

noncomputable def FloatLib.Floats.Formats.Flocq.roundingSpec (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : Numerics.Quantization.Spec BinaryInterchange.Model.IEEERoundingMode ℝ (Numerics.FormatCode (GenericFormat β fexp))

Relational quantization contract for the six rounding directions of IEEERoundingMode.

theorem FloatLib.Floats.Formats.Flocq.roundCode_refines (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] : (roundingSpec β fexp).Implements (roundCode β fexp)

roundCode implements the common relational quantization contract.

theorem FloatLib.Floats.Formats.Flocq.roundCode_of_representable (β : Numerics.Radix) (fexp : ℤ → ℤ) [ValidExp fexp] {x : ℝ} (hx : (Numerics.formatSystem (GenericFormat β fexp)).Representable x) : Numerics.FormatRepresents (GenericFormat β fexp) (roundCode β fexp BinaryInterchange.Model.IEEERoundingMode.nearest x) x

Rounding an already representable real denotes that same real.