From 4bf81ebd260da7b7505655ef4817b19b53fa05c4 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 9 Oct 2023 15:00:41 +0200 Subject: [PATCH 1/2] Documentation --- README.md | 158 +++++++++++++++++++++++++++--- coq-mathcomp-algebra-tactics.opam | 22 ++--- meta.yml | 158 +++++++++++++++++++++++++++--- 3 files changed, 296 insertions(+), 42 deletions(-) diff --git a/README.md b/README.md index 35e9a9a..b3c2393 100644 --- a/README.md +++ b/README.md @@ -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 @@ -62,10 +60,140 @@ 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] +- `GRing.inv`, +- `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 diff --git a/coq-mathcomp-algebra-tactics.opam b/coq-mathcomp-algebra-tactics.opam index 90c647d..3991b57 100644 --- a/coq-mathcomp-algebra-tactics.opam +++ b/coq-mathcomp-algebra-tactics.opam @@ -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"] diff --git a/meta.yml b/meta.yml index 53b9bdd..428bb6d 100644 --- a/meta.yml +++ b/meta.yml @@ -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/ @@ -87,10 +85,140 @@ 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] + - `GRing.inv`, + - `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 From 892c683d3b9fa6303b1f92a0bfd7c4ebd8a2351b Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Wed, 11 Oct 2023 14:19:50 +0200 Subject: [PATCH 2/2] Fix Co-authored-by: Pierre Roux --- README.md | 3 +-- meta.yml | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index b3c2393..14c9da4 100644 --- a/README.md +++ b/README.md @@ -98,7 +98,7 @@ 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)`. +`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 @@ -126,7 +126,6 @@ constructs apart from homomorphism applications: - `expn`,[^constant_exponent] - `N.pow`,[^constant_exponent] - `Z.pow`,[^constant_exponent] -- `GRing.inv`, - `S`, - `Posz`, - `Negz`, and diff --git a/meta.yml b/meta.yml index 428bb6d..a2db58e 100644 --- a/meta.yml +++ b/meta.yml @@ -123,7 +123,7 @@ documentation: |- 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)`. + `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 @@ -151,7 +151,6 @@ documentation: |- - `expn`,[^constant_exponent] - `N.pow`,[^constant_exponent] - `Z.pow`,[^constant_exponent] - - `GRing.inv`, - `S`, - `Posz`, - `Negz`, and