Formal Vindications S.L. is happy to announce the availability of the FormalV Library version 1.0.0.
The library includes three 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 1, 2 or 3 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).
The code and installation instructions through opam are available here.
A coqdoc presentation of the documentation is available here.
This release is compatible with Coq 8.14 and 8.15, and with MathComp 1.12, 1.13 and 1.14.
The library has been developed by the FormalV Development Team, with former and current members: Ana de Almeida Borges, Quim Casals Buñuel, Juan Conejero Rodriguez, Mireia González Bedmar, and Eduardo Hermo Reyes.
You are welcome to contribute by opening issues.
Best regards,
The FormalV Development Team