This small library enables the use of the Micromega arithmetic solvers of Coq for goals stated with the definitions of the Mathematical Components library by extending the zify tactic.

Meta

• Author(s):
  • Kazuhiko Sakaguchi (initial)
• License: CeCILL-B Free Software License Agreement
• Compatible Rocq/Coq versions: 8.18 or later
• Additional dependencies:
  • MathComp ssreflect 2.3 or later
  • MathComp algebra
• Rocq/Coq namespace: mathcomp.zify
• Related publication(s): none

Building and installation instructions

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

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

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/mczify.git
cd mczify
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

File contents

• zify_ssreflect.v: Z-ification instances for the coq-mathcomp-ssreflect library
• zify_algebra.v: Z-ification instances for the coq-mathcomp-algebra library
• zify.v: re-exports all the Z-ification instances
• ssrZ.v: provides a minimal facility for reasoning about Z and relating Z and int