This library provides ring
, field
, lra
, nra
, and psatz
tactics for
the Mathematical Components library. These tactics use the algebraic
structures defined in the MathComp library and their canonical instances for
the instance resolution, and do not require any special instance declaration,
like the Add Ring
and Add Field
commands. Therefore, each of these tactics
works with any instance of the respective structure, including concrete
instances declared through Hierarchy Builder, abstract instances, and mixed
concrete and abstract instances, e.g., int * R
where R
is an abstract
commutative ring. Another key feature of Algebra Tactics is that they
automatically push down ring morphisms and additive functions to leaves of
ring/field expressions before applying the proof procedures.
- Author(s):
- Kazuhiko Sakaguchi (initial)
- Pierre Roux
- License: CeCILL-B Free Software License Agreement
- Compatible Coq versions: 8.16 or later
- Additional dependencies:
- Coq namespace:
mathcomp.algebra_tactics
- Related publication(s):
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
Caveat: the lra
, nra
, and psatz
tactics are considered experimental
features and subject to change.
This Coq library provides an adaptation of the
ring
, field
,
lra
, nra
, and psatz
tactics to the MathComp library.
See the Coq reference manual for the basic functionalities of these tactics.
The descriptions of these tactics below mainly focus on the differences
between ones provided by Coq and ones provided by this library, including the
additional features introduced by this library.
The ring
tactic solves a goal of the form p = q :> R
representing a
polynomial equation. The type R
must have a canonical comRingType
(commutative ring) or at least comSemiRingType
(commutative semiring)
instance.
The ring
tactic solves the equation by normalizing each side as a
polynomial, whose coefficients are either integers Z
(if R
is a
comRingType
) or natural numbers N
.
The ring
tactic can decide the given polynomial equation modulo given
monomial equations. The syntax to use this feature is ring: t_1 .. t_n
where
each t_i
is a proof of equality m_i = p_i
, m_i
is a monomial, and p_i
is a polynomial.
Although the ring
tactic supports ring homomorphisms (explained below), all
the monomials and polynomials m_1, .., m_n, p_1, .., p_n, p, q
must have the
same type R
for the moment.
Each tactic provided by this library has a preprocessor and supports
applications of (semi)ring homomorphisms and additive functions (N-module or
Z-module homomorphisms).
For example, suppose f : S -> T
and g : R -> S
are ring homomorphisms. The
preprocessor turns a ring sub-expression of the form f (x + g (y * z))
into
f x + f (g y) * f (g z)
.
A composition of homomorphisms from the initial objects nat
, N
, int
, and
Z
is automatically normalized to the canonical one. For example, if R
in
the above example is int
, the result of the preprocessing should be
f x + y%:~R * z%:~R
where f \o g : int -> T
is replaced with intr
(_%:~R
).
Thanks to the preprocessor, the ring
tactic supports the following
constructs apart from homomorphism applications:
GRing.zero
(0%R
),GRing.add
(+%R
),addn
,N.add
,Z.add
,GRing.natmul
,GRing.opp
(-%R
),Z.opp
,Z.sub
,intmul
,GRing.one
(1%R
),GRing.mul
(*%R
),muln
,N.mul
,Z.mul
,GRing.exp
,1exprz
,1expn
,1N.pow
,1Z.pow
,1S
,Posz
,Negz
, and- constants of type
nat
,N
, orZ
.
The field
tactic solves a goal of the form p = q :> F
representing a
rational equation. The type F
must have a canonical fieldType
(field)
instance.
The field
tactic solves the equation by normalizing each side to a pair of
two polynomials representing a fraction, whose coefficients are integers Z
.
As is the case for the ring
tactic, the field
tactic can decide the given
rational equation modulo given monomial equations. The syntax to use this
feature is the same as the ring
tactic: field: t_1 .. t_n
.
The field
tactic generates proof obligations that all the denominators in
the equation are not zero.
A proof obligation of the form p * q != 0 :> F
is always automatically
reduced to p != 0 /\ q != 0
.
If the field F
is a numFieldType
(partially ordered field), a proof
obligation of the form c%:~R != 0 :> F
where c
is a non-zero integer
constant is automatically resolved.
The field
tactic has a preprocessor similar to the ring
tactic.
In addition to the constructs supported by the ring
tactic, the field
tactic supports GRing.inv
and exprz
with a negative exponent.
The lra
tactic is a decision procedure for linear real arithmetic. The nra
and psatz
tactics are incomplete proof procedures for non-linear real
arithmetic.
The carrier type must have a canonical realDomainType
(totally ordered
integral domain) or realFieldType
(totally ordered field) instance.
The multiplicative inverse is supported only if the carrier type is a
realFieldType
.
If the carrier type is not a realFieldType
but a realDomainType
, these
three tactics use the same preprocessor as the ring
tactic.
If the carrier type is a realFieldType
, these tactics support GRing.inv
and exprz
with a negative exponent.
In contrast to the field
tactic, these tactics push down the multiplicative
inverse through multiplication and exponentiation, e.g., turning (x * y)^-1
into x^-1 * y^-1
.
theories/
common.v
: provides the reflexive preprocessors (syntax, interpretation function, and normalization functions),common.elpi
: provides the reification procedure for (semi)ring and module expressions, except for the case that the carrier type is arealFieldType
in thelra
,nra
, andpsatz
tactics,ring.v
: provides the Coq code specific to thering
andfield
tactics, including the reflection lemmas,ring.elpi
: provides the Elpi code specific to thering
andfield
tactics,ring_tac.elpi
: provides the entry point for thering
tactic,field_tac.elpi
: provides the entry point for thefield
tactic,lra.v
: provides the Coq code specific to thelra
,nra
, andpsatz
tactics, including the reflection lemmas,lra.elpi
: provides the Elpi code specific to thelra
,nra
, andpsatz
tactics, including the reification procedure and the entry point.
- The adaptation of the
lra
,nra
, andpsatz
tactics is contributed by Pierre Roux. - The way we adapt the internal lemmas of Coq's
ring
andfield
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.