Algebra Tactics

This library provides ring and field tactics for Mathematical Components, that work with any comRingType and fieldType instances, respectively. Their instance resolution is done through canonical structure inference. Therefore, they work with abstract rings and do not require Add Ring and Add Field commands. Another key feature of this library is that they automatically push down ring morphisms and additive functions to leaves of ring/field expressions before normalization to the Horner form.

Meta

• Author(s):
  • Kazuhiko Sakaguchi (initial)
• License: CeCILL-B Free Software License Agreement
• Compatible Coq versions: 8.13 or later
• Additional dependencies:
  • MathComp ssreflect 1.12 or later
  • MathComp algebra
  • Mczify 1.1.0 or later
  • Coq-Elpi 1.10.1 or later
• Coq namespace: mathcomp.algebra_tactics
• Related publication(s):
  • Reflexive tactics for algebra, revisited

Building and installation instructions

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

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-algebra-tactics

To instead build and install manually, do:

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

Credits

• The way we adapt the internals of Coq's ring and field tactics to algebraic structures of the Mathematical Components library is inspired by the elliptic-curves-ssr library by Evmorfia-Iro Bartzia and Pierre-Yves Strub.
• The example from_sander.v contributed by Assia Mahboubi was given to her by Sander Dahmen. It is related to a computational proof that elliptic curves are endowed with a group law. As suggested by Laurent Théry a while ago, this problem is a good benchmark for proof systems. Laurent Théry and Guillaume Hanrot formally verified this property in Coq in 2007.