[WIP] doc

README.md

@@ -13,11 +13,7 @@ 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
+algebraic structures of the Mathematical Components library. 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
@@ -62,10 +58,99 @@ make install
 ```
 
 
-## Caveat
 
-The `lra`, `nra`, and `psatz` tactics are considered experimental features and
-subject to change.
+## Documentation
+
+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 is
+`f x + y%:~R * z%:~R`.
+Thanks to the preprocessor, the ring tactic supports the following constructs
+in addition to homomorphism applications:
+`GRing.zero`, `GRing.add`, `addn`, `N.add`, `Z.add`, `GRing.natmul`,
+`GRing.opp`, `Z.opp`, `Z.sub`, `intmul`,
+`GRing.one`, `GRing.mul`, `muln`, `N.mul`, `Z.mul`,
+`GRing.exp`, `exprz`[^exprz_nneg], `expn`, `N.pow`, `Z.pow`, `GRing.inv`,
+`S`, `Posz`, `Negz`, and constants of type `nat`, `N`, or `Z`.
+
+[^exprz_nneg]: The exponent must be a non-negative constant.
+
+### 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
+
+**Caveat: the `lra`, `nra`, and `psatz` tactics are considered experimental
+features and subject to change.**
+
+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`.
 
 ## Credits
 

coq-mathcomp-algebra-tactics.opam

@@ -13,11 +13,7 @@ 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
+algebraic structures of the Mathematical Components library. 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

meta.yml

@@ -10,11 +10,7 @@ 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
+  algebraic structures of the Mathematical Components library. 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
@@ -87,10 +83,99 @@ dependencies:
 namespace: mathcomp.algebra_tactics
 
 documentation: |-
-  ## Caveat
 
-  The `lra`, `nra`, and `psatz` tactics are considered experimental features and
-  subject to change.
+  ## Documentation
+
+  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 is
+  `f x + y%:~R * z%:~R`.
+  Thanks to the preprocessor, the ring tactic supports the following constructs
+  in addition to homomorphism applications:
+  `GRing.zero`, `GRing.add`, `addn`, `N.add`, `Z.add`, `GRing.natmul`,
+  `GRing.opp`, `Z.opp`, `Z.sub`, `intmul`,
+  `GRing.one`, `GRing.mul`, `muln`, `N.mul`, `Z.mul`,
+  `GRing.exp`, `exprz`[^exprz_nneg], `expn`, `N.pow`, `Z.pow`, `GRing.inv`,
+  `S`, `Posz`, `Negz`, and constants of type `nat`, `N`, or `Z`.
+
+  [^exprz_nneg]: The exponent must be a non-negative constant.
+
+  ### 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
+
+  **Caveat: the `lra`, `nra`, and `psatz` tactics are considered experimental
+  features and subject to change.**
+
+  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`.
 
   ## Credits