Skip to content

Commit

Permalink
Merge pull request #89 from math-comp/doc
Browse files Browse the repository at this point in the history 
Documentation
  • Loading branch information
@pi8027
pi8027 authored Oct 11, 2023
2 parents 97a2ceb + 892c683 commit d2e6f9e
Show file tree
Hide file tree
Showing 3 changed files with 294 additions and 42 deletions.
157 changes: 142 additions & 15 deletions README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,16 @@ Follow the instructions on https://github.com/coq-community/templates to regener


This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
algebraic structures of the Mathematical Components library. The `ring` tactic
works with any `comRingType` (commutative ring) or `comSemiRingType`
(commutative semiring). The `field` tactic works with any `fieldType` (field).
The other (Micromega) tactics work with any `realDomainType` (totally ordered
integral domain) or `realFieldType` (totally ordered field). Algebra Tactics
do not provide a way to declare instances, like the `Add Ring` and `Add Field`
commands, but use canonical structure inference instead. Therefore, each of
these tactics works with any canonical (or abstract) instance of the
respective structure declared through Hierarchy Builder. 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.
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.

## Meta

Expand Down Expand Up @@ -62,10 +60,139 @@ make install
```


## Caveat

The `lra`, `nra`, and `psatz` tactics are considered experimental features and
subject to change.
## Documentation

**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`](https://coq.inria.fr/refman/addendum/ring),
[`lra`, `nra`, and `psatz`](https://coq.inria.fr/refman/addendum/micromega)
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

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`,[^constant_exponent]
- `exprz`,[^constant_exponent]
- `expn`,[^constant_exponent]
- `N.pow`,[^constant_exponent]
- `Z.pow`,[^constant_exponent]
- `S`,
- `Posz`,
- `Negz`, and
- constants of type `nat`, `N`, or `Z`.

[^constant_exponent]: The exponent must be a constant value. In addition, it
must be non-negative for `exprz`.

### The `field` tactic

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 ot the constructs supported by the `ring` tactic, the `field`
tactic supports `GRing.inv` and `exprz` with a negative exponent.

### The `lra`, `nra`, and `psatz` tactics

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`.

## Files

- `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 a
`realFieldType` in the `lra`, `nra`, and `psatz` tactics,
- `ring.v`: provides the Coq code specific to the `ring` and `field`
tactics, including the reflection lemmas,
- `ring.elpi`: provides the Elpi code specific to the `ring` and `field`
tactics,
- `ring_tac.elpi`: provides the entry point for the `ring` tactic,
- `field_tac.elpi`: provides the entry point for the `field` tactic,
- `lra.v`: provides the Coq code specific to the `lra`, `nra`, and `psatz`
tactics, including the reflection lemmas,
- `lra.elpi`: provides the Elpi code specific to the `lra`, `nra`, and
`psatz` tactics, including the reification procedure and the entry point.

## Credits

Expand Down
22 changes: 10 additions & 12 deletions coq-mathcomp-algebra-tactics.opam
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,16 @@ license: "CECILL-B"
synopsis: "Ring, field, lra, nra, and psatz tactics for Mathematical Components"
description: """
This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
algebraic structures of the Mathematical Components library. The `ring` tactic
works with any `comRingType` (commutative ring) or `comSemiRingType`
(commutative semiring). The `field` tactic works with any `fieldType` (field).
The other (Micromega) tactics work with any `realDomainType` (totally ordered
integral domain) or `realFieldType` (totally ordered field). Algebra Tactics
do not provide a way to declare instances, like the `Add Ring` and `Add Field`
commands, but use canonical structure inference instead. Therefore, each of
these tactics works with any canonical (or abstract) instance of the
respective structure declared through Hierarchy Builder. 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."""
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."""

build: [make "-j%{jobs}%"]
install: [make "install"]
Expand Down
157 changes: 142 additions & 15 deletions meta.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -10,18 +10,16 @@ synopsis: >-
description: |-
This library provides `ring`, `field`, `lra`, `nra`, and `psatz` tactics for
algebraic structures of the Mathematical Components library. The `ring` tactic
works with any `comRingType` (commutative ring) or `comSemiRingType`
(commutative semiring). The `field` tactic works with any `fieldType` (field).
The other (Micromega) tactics work with any `realDomainType` (totally ordered
integral domain) or `realFieldType` (totally ordered field). Algebra Tactics
do not provide a way to declare instances, like the `Add Ring` and `Add Field`
commands, but use canonical structure inference instead. Therefore, each of
these tactics works with any canonical (or abstract) instance of the
respective structure declared through Hierarchy Builder. 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.
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.
publications:
- pub_url: https://drops.dagstuhl.de/opus/volltexte/2022/16738/
Expand Down Expand Up @@ -87,10 +85,139 @@ dependencies:
namespace: mathcomp.algebra_tactics

documentation: |-
## Caveat
The `lra`, `nra`, and `psatz` tactics are considered experimental features and
subject to change.
## Documentation
**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`](https://coq.inria.fr/refman/addendum/ring),
[`lra`, `nra`, and `psatz`](https://coq.inria.fr/refman/addendum/micromega)
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
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`,[^constant_exponent]
- `exprz`,[^constant_exponent]
- `expn`,[^constant_exponent]
- `N.pow`,[^constant_exponent]
- `Z.pow`,[^constant_exponent]
- `S`,
- `Posz`,
- `Negz`, and
- constants of type `nat`, `N`, or `Z`.
[^constant_exponent]: The exponent must be a constant value. In addition, it
must be non-negative for `exprz`.
### The `field` tactic
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 ot the constructs supported by the `ring` tactic, the `field`
tactic supports `GRing.inv` and `exprz` with a negative exponent.
### The `lra`, `nra`, and `psatz` tactics
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`.
## Files
- `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 a
`realFieldType` in the `lra`, `nra`, and `psatz` tactics,
- `ring.v`: provides the Coq code specific to the `ring` and `field`
tactics, including the reflection lemmas,
- `ring.elpi`: provides the Elpi code specific to the `ring` and `field`
tactics,
- `ring_tac.elpi`: provides the entry point for the `ring` tactic,
- `field_tac.elpi`: provides the entry point for the `field` tactic,
- `lra.v`: provides the Coq code specific to the `lra`, `nra`, and `psatz`
tactics, including the reflection lemmas,
- `lra.elpi`: provides the Elpi code specific to the `lra`, `nra`, and
`psatz` tactics, including the reification procedure and the entry point.
## Credits
Expand Down

0 comments on commit d2e6f9e

Please sign in to comment.