Interval arithmetic

FloatLib's executable interval interfaces share outward rounding and real containment proofs:

• Numerics.Interval α pairs endpoints in any representation. Its operations use a supplied Numerics.OutwardRounding; binary, decimal, and posit adapters provide rational decoders and checked endpoint rounding. Successful results enclose arbitrary real values between the inputs, through the theorems in Numerics.Enclosure.Interval.Real.
• BinaryInterchange.Model.Interval fmt and ExecFloat.Binary.Interval provide directed binary arithmetic. Their IEEE arithmetic theorems accept finite input bounds and permit infinite output bounds after overflow. Finite-only formats have explicit range premises.
• Numerics.RationalInterval supports the exact rational bounds used by the elementary function kernels.

For proofs directly over ℝ, Floats.Interval.Quantized supplies noncomputable intervals whose endpoints lie on a Flocq-style rounding grid. Concrete endpoint adapters are in each format's Interval module; the optional Arb comparison adapter is in FloatLibTests.Arb.ModelTranscendentals.

References

• S. M. Rump, Verification methods: Rigorous results using floating-point arithmetic, Acta Numerica 19 (2010), §§5.1–5.5: endpoint arithmetic, outward rounding, and containment under composition.
• S. Boldo and G. Melquiond, Flocq: A Unified Library for Proving Floating-Point Algorithms in Coq, ARITH 2011: the rounded-real grids used by the proof-side interval interface.