The package contains a package to reasoning with big enough objects (mostly natural numbers). This package is essentially for backward compatibility purposes as bigenough will be subsumed by the near tactics. The formalization is based on the Mathematical Components library.

Meta

• Author(s):
  • Cyril Cohen
• License: CeCILL-B
• Compatible Rocq/Coq versions: 8.10 or later
• Additional dependencies:
  • MathComp boot 1.6 or later (MathComp ssreflect for versions <= 2.4.0)
• Rocq/Coq namespace: mathcomp.bigenough
• Related publication(s): none

Building and installation instructions

The easiest way to install the latest released version of bigenough is via OPAM:

opam repo add rocq-released https://rocq-prover.org/opam/released
opam install rocq-mathcomp-bigenough

To instead build and install manually, you need to make sure that all the libraries this development depends on are installed. The easiest way to do that is still to rely on opam:

git clone https://github.com/math-comp/bigenough.git
cd bigenough
opam repo add rocq-released https://rocq-prover.org/opam/released
opam install --deps-only .
make   # or make -j <number-of-cores-on-your-machine> 
make install

A small library to do epsilon - N reasoning.

This repository is essentially for archiving purposes as bigenough will be subsumed by the near tactics.

The formalization is based on the Mathematical Components library for the Coq proof assistant, although it requires only the boot package.