diff options
Diffstat (limited to 'doc/sphinx/addendum/ring.rst')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index d5c33dc1d4..8cb86e2267 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -19,7 +19,7 @@ field equations. What does this tactic do? ------------------------------ -``ring`` does associative-commutative rewriting in ring and semi-ring +``ring`` does associative-commutative rewriting in ring and semiring structures. Assume you have two binary functions :math:`\oplus` and :math:`\otimes` that are associative and commutative, with :math:`\oplus` distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for @@ -37,7 +37,7 @@ order. It is an easy theorem to show that every polynomial is equivalent (modulo the ring properties) to exactly one canonical sum. This canonical sum is called the normal form of the polynomial. In fact, the actual representation shares monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over -any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring +any ring or semiring structure. The basic use of ``ring`` is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity. @@ -103,7 +103,7 @@ Concrete usage in Coq .. tacn:: ring The ``ring`` tactic solves equations upon polynomial expressions of a ring -(or semi-ring) structure. It proceeds by normalizing both sides +(or semiring) structure. It proceeds by normalizing both sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation, rewriting of monomials) and comparing syntactically the results. @@ -264,13 +264,13 @@ are the implementations of the ring operations, ``==`` is the equality of the coefficients, ``?+!`` is an implementation of this equality, and ``[x]`` is a notation for the image of ``x`` by the ring morphism. -Since |Z| is an initial ring (and |N| is an initial semi-ring), it can +Since |Z| is an initial ring (and |N| is an initial semiring), it can always be considered as a set of coefficients. There are basically three kinds of (semi-)rings: abstract rings to be used when operations are not effective. The set - of coefficients is |Z| (or |N| for semi-rings). + of coefficients is |Z| (or |N| for semirings). computational rings to be used when operations are effective. The @@ -505,10 +505,10 @@ expression `F` to a common denominator :math:`N/D = 0` where `N` and `D` are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve :math:`N = 0`. -Note that ``field`` also generates non-zero conditions for all the +Note that ``field`` also generates nonzero conditions for all the denominators it encounters in the reduction. In our example, it generates the condition :math:`x \neq 0`. These conditions appear as one subgoal -which is a conjunction if there are several denominators. Non-zero +which is a conjunction if there are several denominators. Nonzero conditions are always polynomial expressions. For example when reducing the expression :math:`1/(1 + 1/x)`, two side conditions are generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since @@ -616,7 +616,7 @@ carrier set, an equality, and field operations: satisfies the field axioms. Semi-fields (fields without + inverse) are also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see :ref:`tactics-enabled-on-user-provided-relations`). The definition of -fields and semi-fields is: +fields and semifields is: .. coqtop:: in @@ -670,7 +670,7 @@ specific modifier: completeness :n:`@term` allows the field tactic to prove automatically - that the image of non-zero coefficients are mapped to non-zero + that the image of nonzero coefficients are mapped to nonzero elements of the field. :n:`@term` is a proof of ``forall x y, [x] == [y] -> x ?=! y = true``, @@ -684,7 +684,7 @@ History of ring First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big -for |Coq|’s type-checker. Let us see why: +for |Coq|’s type checker. Let us see why: .. coqtop:: all @@ -707,7 +707,7 @@ interleaving of computation and reasoning (see :ref:`discussion_reflection`). He some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. Proofs terms generated by ring are quite small, they are linear in the -number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking +number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking those terms requires some time because it makes a large use of the conversion rule, but memory requirements are much smaller. |