Proof-indexed application of numerical operations #
These helpers apply existing executable functions to proof-indexed inputs. Runtime data remains the concrete code returned by those functions; representation proofs are propositions erased by the compiler.
The imports collect total, finite, checked, and quantizer proof helpers. The composition laws
below combine refinement facts directly, without wrapping the executable functions. Import a
Proof.* submodule when only one proof-indexed contract family is needed.
Composition of executable refinements #
theorem
FloatLib.Numerics.Operation.total1_comp
{A : NumericalSystem}
{B : NumericalSystem}
{C : NumericalSystem}
{run₁ : A.Code → B.Code}
{run₂ : B.Code → C.Code}
{spec₁ : NumericalValue A.Scalar → NumericalValue B.Scalar}
{spec₂ : NumericalValue B.Scalar → NumericalValue C.Scalar}
(h₁ : Total1 A B run₁ spec₁)
(h₂ : Total1 B C run₂ spec₂)
:
Total unary refinement is closed under composition.
theorem
FloatLib.Numerics.Operation.finite1_comp
{A : NumericalSystem}
{B : NumericalSystem}
{C : NumericalSystem}
{run₁ : A.Code → B.Code}
{run₂ : B.Code → C.Code}
{spec₁ : A.Scalar → B.Scalar}
{spec₂ : B.Scalar → C.Scalar}
(h₁ : Finite1 A B run₁ spec₁)
(h₂ : Finite1 B C run₂ spec₂)
:
Finite unary refinement is closed under composition.
theorem
FloatLib.Numerics.Operation.castFiniteOn_comp
{A : NumericalSystem}
{B : NumericalSystem}
{C : NumericalSystem}
{run₁ : A.Code → B.Code}
{run₂ : B.Code → C.Code}
{embed₁ : A.Scalar → B.Scalar}
{embed₂ : B.Scalar → C.Scalar}
{pre₁ : A.Scalar → Prop}
{pre₂ : B.Scalar → Prop}
(h₁ : CastFiniteOn A B run₁ embed₁ pre₁)
(h₂ : CastFiniteOn B C run₂ embed₂ pre₂)
:
CastFiniteOn A C (run₂ ∘ run₁) (embed₂ ∘ embed₁) fun (x : A.Scalar) => pre₁ x ∧ pre₂ (embed₁ x)
Casts implement the composed scalar maps when the intermediate value meets its precondition.
theorem
FloatLib.Numerics.Operation.quantizer_exactOn
{S : NumericalSystem}
{quantize : S.Scalar → S.Code}
{round : S.Scalar → S.Scalar}
{pre fixed : S.Scalar → Prop}
(hrefines : QuantizerOn S quantize round pre)
(hfixed : ∀ (x : S.Scalar), fixed x → round x = x)
(x : S.Scalar)
:
pre x → fixed x → S.Represents (quantize x) x
A refining quantizer is exact wherever its mathematical rounding map fixes the input.