FormalV Library
The FormalV Library is the Coq/MathComp library developed in a public source-code setting by Formal Vindications S.L. It includes the following packages:
-
FV Prim63 to MathComp provides conversions from the Coq primitive integers Uint63 and Sint63 to the MathComp natural and integer numbers nat and int, and vice versa, as well as lemmas to rewrite between their respective operations.
-
FV Check Range provides tactics to automatically prove Boolean goals involving one, two, or three Uint63.int/Sint63.int bounded variables through brute-force computation.
-
FV Time is a library for managing conversions between time formats (UTC and timestamps), as well as commonly used functions for time arithmetic. As a library for time conversions, its novelty is the implementation of leap seconds (which are part of the UTC standard but usually not implemented in commercial libraries).
Co-authors
- Joaquim Casals Buñuel
- Juan Conejero Rodriguez
- Mireia González Bedmar
- Eduardo Hermo Reyes