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.

• 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

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

opam repo add coq-released https://coq.inria.fr/opam/released
opam install rocq-mathcomp-zify

To instead build and install manually, do:

git clone https://github.com/math-comp/mczify.git
cd mczify
make   # or make -j <number-of-cores-on-your-machine> 
make install

• 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