summaryrefslogtreecommitdiff
path: root/doc/refman/Polynom.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/Polynom.tex')
-rw-r--r--doc/refman/Polynom.tex1000
1 files changed, 0 insertions, 1000 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex
deleted file mode 100644
index 3898bf4c..00000000
--- a/doc/refman/Polynom.tex
+++ /dev/null
@@ -1,1000 +0,0 @@
-\achapter{The \texttt{ring} and \texttt{field} tactic families}
-\aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia
- Mahboubi, Laurent Th\'ery\footnote{based on previous work from
- Patrick Loiseleur and Samuel Boutin}}
-\label{ring}
-\tacindex{ring}
-
-This chapter presents the tactics dedicated to deal with ring and
-field equations.
-
-\asection{What does this tactic do?}
-
-\texttt{ring} does associative-commutative rewriting in ring and semi-ring
-structures. Assume you have two binary functions $\oplus$ and $\otimes$
-that are associative and commutative, with $\oplus$ distributive on
-$\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
-$\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1,
-\dots$ and constants by application of $\oplus$ and $\otimes$.
-
-Let an {\it ordered product} be a product of variables $V_{i_1}
-\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le
-i_n$. Let a \textit{monomial} be the product of a constant and an
-ordered product. We can order the monomials by the lexicographic
-order on products of variables. Let a \textit{canonical sum} be an
-ordered sum of monomials that are all different, i.e. each monomial in
-the sum is strictly less than the following monomial according to the
-lexicographic 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 \textit{normal form}
-of the polynomial. In fact, the actual representation shares monomials
-with same prefixes. So what does \texttt{ring}? It normalizes
-polynomials over any ring or semi-ring structure. The basic use of
-\texttt{ring} is to simplify ring expressions, so that the user does
-not have to deal manually with the theorems of associativity and
-commutativity.
-
-\begin{Examples}
-\item In the ring of integers, the normal form of
-$x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
-\end{Examples}
-
-\texttt{ring} is also able to compute a normal form modulo monomial
-equalities. For example, under the hypothesis that $2x^2 = yz+1$,
- the normal form of $2(x + 1)x - x - zy$ is $x+1$.
-
-\asection{The variables map}
-
-It is frequent to have an expression built with + and
- $\times$, but rarely on variables only.
-Let us associate a number to each subterm of a ring
-expression in the \gallina\ language. For example in the ring
-\texttt{nat}, consider the expression:
-
-\begin{quotation}
-\begin{verbatim}
-(plus (mult (plus (f (5)) x) x)
- (mult (if b then (4) else (f (3))) (2)))
-\end{verbatim}
-\end{quotation}
-
-\noindent As a ring expression, it has 3 subterms. Give each subterm a
-number in an arbitrary order:
-
-\begin{tabular}{ccl}
-0 & $\mapsto$ & \verb|if b then (4) else (f (3))| \\
-1 & $\mapsto$ & \verb|(f (5))| \\
-2 & $\mapsto$ & \verb|x| \\
-\end{tabular}
-
-\noindent Then normalize the ``abstract'' polynomial
-
-$$((V_1 \otimes V_2) \oplus V_2) \oplus (V_0 \otimes 2) $$
-
-\noindent In our example the normal form is:
-
-$$(2 \otimes V_0) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2)$$
-
-\noindent Then substitute the variables by their values in the variables map to
-get the concrete normal polynomial:
-
-\begin{quotation}
-\begin{verbatim}
-(plus (mult (2) (if b then (4) else (f (3))))
- (plus (mult (f (5)) x) (mult x x)))
-\end{verbatim}
-\end{quotation}
-
-\asection{Is it automatic?}
-
-Yes, building the variables map and doing the substitution after
-normalizing is automatically done by the tactic. So you can just forget
-this paragraph and use the tactic according to your intuition.
-
-\asection{Concrete usage in \Coq
-\tacindex{ring}
-\tacindex{ring\_simplify}}
-
-The {\tt ring} tactic solves equations upon polynomial expressions of
-a ring (or semi-ring) structure. It proceeds by normalizing both hand
-sides of the equation (w.r.t. associativity, commutativity and
-distributivity, constant propagation, rewriting of monomials)
-and comparing syntactically the results.
-
-{\tt ring\_simplify} applies the normalization procedure described
-above to the terms given. The tactic then replaces all occurrences of
-the terms given in the conclusion of the goal by their normal
-forms. If no term is given, then the conclusion should be an equation
-and both hand sides are normalized.
-The tactic can also be applied in a hypothesis.
-
-The tactic must be loaded by \texttt{Require Import Ring}. The ring
-structures must be declared with the \texttt{Add Ring} command (see
-below). The ring of booleans is predefined; if one wants to use the
-tactic on \texttt{nat} one must first require the module
-\texttt{ArithRing} (exported by \texttt{Arith});
-for \texttt{Z}, do \texttt{Require Import
-ZArithRing} or simply \texttt{Require Import ZArith};
-for \texttt{N}, do \texttt{Require Import NArithRing} or
-\texttt{Require Import NArith}.
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Require Import ZArith.
-Open Scope Z_scope.
-Goal forall a b c:Z,
- (a + b + c)^2 =
- a * a + b^2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
-\end{coq_example}
-\begin{coq_example}
-intros; ring.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall a b:Z, 2*a*b = 30 ->
- (a+b)^2 = a^2 + b^2 + 30.
-\end{coq_example}
-\begin{coq_example}
-intros a b H; ring [H].
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Variants}
- \item {\tt ring [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
- terms modulo ring operations and rewriting of the equalities
- defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
- {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
- where $m$ is a monomial (after ``abstraction''),
- $p$ a polynomial and $=$ the corresponding equality of the ring structure.
-
- \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in
-{\ident}}
- performs the simplification in the hypothesis named {\tt ident}.
-\end{Variants}
-
-\Warning \texttt{ring\_simplify \term$_1$; ring\_simplify \term$_2$} is
-not equivalent to \texttt{ring\_simplify \term$_1$ \term$_2$}. In the
-latter case the variables map is shared between the two terms, and
-common subterm $t$ of \term$_1$ and \term$_2$ will have the same
-associated variable number. So the first alternative should be
-avoided for terms belonging to the same ring theory.
-
-
-\begin{ErrMsgs}
-\item \errindex{not a valid ring equation}
- The conclusion of the goal is not provable in the corresponding ring
- theory.
-\item \errindex{arguments of ring\_simplify do not have all the same type}
- {\tt ring\_simplify} cannot simplify terms of several rings at the
- same time. Invoke the tactic once per ring structure.
-\item \errindex{cannot find a declared ring structure over {\tt term}}
- No ring has been declared for the type of the terms to be
- simplified. Use {\tt Add Ring} first.
-\item \errindex{cannot find a declared ring structure for equality
- {\tt term}}
- Same as above is the case of the {\tt ring} tactic.
-\end{ErrMsgs}
-
-\asection{Adding a ring structure
-\comindex{Add Ring}}
-
-Declaring a new ring consists in proving that a ring signature (a
-carrier set, an equality, and ring operations: {\tt
-Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory})
-satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are
-also supported. The equality can be either Leibniz equality, or any
-relation declared as a setoid (see~\ref{setoidtactics}). The definition
-of ring and semi-rings (see module {\tt Ring\_theory}) is:
-\begin{verbatim}
- Record ring_theory : Prop := mk_rt {
- Radd_0_l : forall x, 0 + x == x;
- Radd_sym : forall x y, x + y == y + x;
- Radd_assoc : forall x y z, x + (y + z) == (x + y) + z;
- Rmul_1_l : forall x, 1 * x == x;
- Rmul_sym : forall x y, x * y == y * x;
- Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z;
- Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z);
- Rsub_def : forall x y, x - y == x + -y;
- Ropp_def : forall x, x + (- x) == 0
- }.
-
-Record semi_ring_theory : Prop := mk_srt {
- SRadd_0_l : forall n, 0 + n == n;
- SRadd_sym : forall n m, n + m == m + n ;
- SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
- SRmul_1_l : forall n, 1*n == n;
- SRmul_0_l : forall n, 0*n == 0;
- SRmul_sym : forall n m, n*m == m*n;
- SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
- SRdistr_l : forall n m p, (n + m)*p == n*p + m*p
- }.
-\end{verbatim}
-
-This implementation of {\tt ring} also features a notion of constant
-that can be parameterized. This can be used to improve the handling of
-closed expressions when operations are effective. It consists in
-introducing a type of \emph{coefficients} and an implementation of the
-ring operations, and a morphism from the coefficient type to the ring
-carrier type. The morphism needs not be injective, nor surjective. As
-an example, one can consider the real numbers. The set of coefficients
-could be the rational numbers, upon which the ring operations can be
-implemented. The fact that there exists a morphism is defined by the
-following properties:
-\begin{verbatim}
- Record ring_morph : Prop := mkmorph {
- morph0 : [cO] == 0;
- morph1 : [cI] == 1;
- morph_add : forall x y, [x +! y] == [x]+[y];
- morph_sub : forall x y, [x -! y] == [x]-[y];
- morph_mul : forall x y, [x *! y] == [x]*[y];
- morph_opp : forall x, [-!x] == -[x];
- morph_eq : forall x y, x?=!y = true -> [x] == [y]
- }.
-
- Record semi_morph : Prop := mkRmorph {
- Smorph0 : [cO] == 0;
- Smorph1 : [cI] == 1;
- Smorph_add : forall x y, [x +! y] == [x]+[y];
- Smorph_mul : forall x y, [x *! y] == [x]*[y];
- Smorph_eq : forall x y, x?=!y = true -> [x] == [y]
- }.
-\end{verbatim}
-where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set,
-{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring
-operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is
-an implementation of this equality, and {\tt [x]} is a notation for
-the image of {\tt x} by the ring morphism.
-
-Since {\tt Z} is an initial ring (and {\tt N} is an initial
-semi-ring), it can always be considered as a set of
-coefficients. There are basically three kinds of (semi-)rings:
-\begin{description}
-\item[abstract rings] to be used when operations are not
- effective. The set of coefficients is {\tt Z} (or {\tt N} for
- semi-rings).
-\item[computational rings] to be used when operations are
- effective. The set of coefficients is the ring itself. The user only
- has to provide an implementation for the equality.
-\item[customized ring] for other cases. The user has to provide the
- coefficient set and the morphism.
-\end{description}
-
-This implementation of ring can also recognize simple
-power expressions as ring expressions. A power function is specified by
-the following property:
-\begin{verbatim}
- Section POWER.
- Variable Cpow : Set.
- Variable Cp_phi : N -> Cpow.
- Variable rpow : R -> Cpow -> R.
-
- Record power_theory : Prop := mkpow_th {
- rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
- }.
-
- End POWER.
-\end{verbatim}
-
-
-The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
-($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used
-for error messages. The term $ring$ is a proof that the ring signature
-satisfies the (semi-)ring axioms. The optional list of modifiers is
-used to tailor the behavior of the tactic. The following list
-describes their syntax and effects:
-\begin{description}
-\item[abstract] declares the ring as abstract. This is the default.
-\item[decidable \term] declares the ring as computational. The expression
- \term{} is
- the correctness proof of an equality test {\tt ?=!} (which should be
- evaluable). Its type should be of
- the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
-\item[morphism \term] declares the ring as a customized one. The expression
- \term{} is
- a proof that there exists a morphism between a set of coefficient
- and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt
- Ring\_theory.semi\_morph}).
-\item[setoid \term$_1$ \term$_2$] forces the use of given setoid. The
- expression \term$_1$ is a proof that the equality is indeed a setoid
- (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the
- ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and
- {\tt Ring\_theory.sring\_eq\_ext}). This modifier needs not be used if the
- setoid and morphisms have been declared.
-\item[constants [\ltac]] specifies a tactic expression that, given a term,
- returns either an object of the coefficient set that is mapped to
- the expression via the morphism, or returns {\tt
- InitialRing.NotConstant}. The default behaviour is to map only 0 and
- 1 to their counterpart in the coefficient set. This is generally not
- desirable for non trivial computational rings.
-\item[preprocess [\ltac]]
- specifies a tactic that is applied as a preliminary step for {\tt
- ring} and {\tt ring\_simplify}. It can be used to transform a goal
- so that it is better recognized. For instance, {\tt S n} can be
- changed to {\tt plus 1 n}.
-\item[postprocess [\ltac]] specifies a tactic that is applied as a final step
- for {\tt ring\_simplify}. For instance, it can be used to undo
- modifications of the preprocessor.
-\item[power\_tac {\term} [\ltac]] allows {\tt ring} and {\tt ring\_simplify} to
- recognize power expressions with a constant positive integer exponent
- (example: $x^2$). The term {\term} is a proof that a given power function
- satisfies the specification of a power function ({\term} has to be a
- proof of {\tt Ring\_theory.power\_theory}) and {\ltac} specifies a
- tactic expression that, given a term, ``abstracts'' it into an
- object of type {\tt N} whose interpretation via {\tt Cp\_phi} (the
- evaluation function of power coefficient) is the original term, or
- returns {\tt InitialRing.NotConstant} if not a constant coefficient
- (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
- See files {\tt plugins/setoid\_ring/ZArithRing.v} and
- {\tt plugins/setoid\_ring/RealField.v} for examples.
- By default the tactic does not recognize power expressions as ring
- expressions.
-\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
- when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$.
- The term {\term} is a proof that a given sign function indicates expressions
- that are signed ({\term} has to be a
- proof of {\tt Ring\_theory.get\_sign}). See {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
-\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals
-with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function satisfies the specification of an euclidean
- division function ({\term} has to be a
- proof of {\tt Ring\_theory.div\_theory}). For example, this function is
- called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
- See {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
-
-\end{description}
-
-
-\begin{ErrMsgs}
-\item \errindex{bad ring structure}
- The proof of the ring structure provided is not of the expected type.
-\item \errindex{bad lemma for decidability of equality}
- The equality function provided in the case of a computational ring
- has not the expected type.
-\item \errindex{ring {\it operation} should be declared as a morphism}
- A setoid associated to the carrier of the ring structure as been
- found, but the ring operation should be declared as
- morphism. See~\ref{setoidtactics}.
-\end{ErrMsgs}
-
-\asection{How does it work?}
-
-The code of \texttt{ring} is a good example of tactic written using
-\textit{reflection}. What is reflection? Basically, it is writing
-\Coq{} tactics in \Coq, rather than in \ocaml. From the philosophical
-point of view, it is using the ability of the Calculus of
-Constructions to speak and reason about itself. For the \texttt{ring}
-tactic we used \Coq\ as a programming language and also as a proof
-environment to build a tactic and to prove it correctness.
-
-The interested reader is strongly advised to have a look at the file
-\texttt{Ring\_polynom.v}. Here a type for polynomials is defined:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Inductive PExpr : Type :=
- | PEc : C -> PExpr
- | PEX : positive -> PExpr
- | PEadd : PExpr -> PExpr -> PExpr
- | PEsub : PExpr -> PExpr -> PExpr
- | PEmul : PExpr -> PExpr -> PExpr
- | PEopp : PExpr -> PExpr
- | PEpow : PExpr -> N -> PExpr.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-Polynomials in normal form are defined as:
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
- Inductive Pol : Type :=
- | Pc : C -> Pol
- | Pinj : positive -> Pol -> Pol
- | PX : Pol -> positive -> Pol -> Pol.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by
-$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$,
-$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$.
-
-
-Variables maps are represented by list of ring elements, and two
-interpretation functions, one that maps a variables map and a
-polynomial to an element of the concrete ring, and the second one that
-does the same for normal forms:
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Definition PEeval : list R -> PExpr -> R := [...].
-Definition Pphi_dev : list R -> Pol -> R := [...].
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-A function to normalize polynomials is defined, and the big theorem is
-its correctness w.r.t interpretation, that is:
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Definition norm : PExpr -> Pol := [...].
-Lemma Pphi_dev_ok :
- forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-So now, what is the scheme for a normalization proof? Let \texttt{p}
-be the polynomial expression that the user wants to normalize. First a
-little piece of ML code guesses the type of \texttt{p}, the ring
-theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
-variables map \texttt{v} such that \texttt{p} is
-$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we
-replace it by \verb|(Pphi_dev v (norm ap))|, using the
-main correctness theorem and we reduce it to a concrete expression
-\texttt{p'}, which is the concrete normal form of
-\texttt{p}. This is summarized in this diagram:
-\begin{center}
-\begin{tabular}{rcl}
-\texttt{p} & $\rightarrow_{\beta\delta\iota}$
- & \texttt{(PEeval v ap)} \\
- & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
-\texttt{p'}
- & $\leftarrow_{\beta\delta\iota}$
- & \texttt{(Pphi\_dev v (norm ap))}
-\end{tabular}
-\end{center}
-The user do not see the right part of the diagram.
-From outside, the tactic behaves like a
-$\beta\delta\iota$ simplification extended with AC rewriting rules.
-Basically, the proof is only the application of the main
-correctness theorem to well-chosen arguments.
-
-
-\asection{Dealing with fields
-\tacindex{field}
-\tacindex{field\_simplify}
-\tacindex{field\_simplify\_eq}}
-
-
-The {\tt field} tactic is an extension of the {\tt ring} to deal with
-rational expresision. Given a rational expression $F=0$. It first reduces the expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring
-expressions.
-For example, if we take $F = (1 - 1/x) x - x + 1$, this gives
-$ N= (x -1) x - x^2 + x$ and $D= x$. It then calls {\tt ring}
-to solve $N=0$. Note that {\tt field} also generates non-zero conditions
-for all the denominators it encounters in the reduction.
-In our example, it generates the condition $x \neq 0$. These
-conditions appear as one subgoal which is a conjunction if there are
-several denominators.
-Non-zero conditions are {\it always} polynomial expressions. For example
-when reducing the expression $1/(1 + 1/x)$, two side conditions are
-generated: $x\neq 0$ and $x + 1 \neq 0$. Factorized expressions are
-broken since a field is an integral domain, and when the equality test
-on coefficients is complete w.r.t. the equality of the target field,
-constants can be proven different from zero automatically.
-
-The tactic must be loaded by \texttt{Require Import Field}. New field
-structures can be declared to the system with the \texttt{Add Field}
-command (see below). The field of real numbers is defined in module
-\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported
-by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
-\texttt{Reals} is enough to use the field tactics on real
-numbers. Rational numbers in canonical form are also declared as a
-field in module \texttt{Qcanon}.
-
-
-\Example
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-\begin{coq_example}
-Require Import Reals.
-Open Scope R_scope.
-Goal forall x, x <> 0 ->
- (1 - 1/x) * x - x + 1 = 0.
-\end{coq_example}
-\begin{coq_example}
-intros; field; auto.
-\end{coq_example}
-\begin{coq_eval}
-Abort.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall x y, y <> 0 -> y = x -> x/y = 1.
-\end{coq_example}
-\begin{coq_example}
-intros x y H H1; field [H1]; auto.
-\end{coq_example}
-\begin{coq_eval}
-Reset Initial.
-\end{coq_eval}
-
-\begin{Variants}
- \item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
- terms modulo field operations and rewriting of the equalities
- defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
- {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
- where $m$ is a monomial (after ``abstraction''),
- $p$ a polynomial and $=$ the corresponding equality of the field structure.
- Beware that rewriting works with the equality $m=p$ only if $p$ is a
- polynomial since rewriting is handled by the underlying {\tt ring}
- tactic.
- \item {\tt field\_simplify}
- performs the simplification in the conclusion of the goal, $F_1 = F_2$
- becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the
- one for rings) is then applied to $N_1$, $D_1$, $N_2$ and
- $D_2$. This way, polynomials remain in factorized form during the
- fraction simplifications. This yields smaller expressions when
- reducing to the same denominator since common factors can be
- cancelled.
-
- \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$]}
- performs the simplification in the conclusion of the goal using
- the equalities
- defined by \term$_1$ {\ldots} \term$_n$.
-
- \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
-$t_m$}
- performs the simplification in the terms $t_1$ \ldots $t_m$
- of the conclusion of the goal using
- the equalities
- defined by \term$_1$ {\ldots} \term$_n$.
-
- \item {\tt field\_simplify in $H$}
- performs the simplification in the assumption $H$.
-
- \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] in $H$}
- performs the simplification in the assumption $H$ using
- the equalities
- defined by \term$_1$ {\ldots} \term$_n$.
-
- \item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
-$t_m$ in $H$}
- performs the simplification in the terms $t_1$ \ldots $t_n$
- of the assumption $H$ using
- the equalities
- defined by \term$_1$ {\ldots} \term$_m$.
-
- \item {\tt field\_simplify\_eq}
- performs the simplification in the conclusion of the goal removing
- the denominator. $F_1 = F_2$
- becomes $N_1 D_2 = N_2 D_1$.
-
- \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$]}
- performs the simplification in the conclusion of the goal using
- the equalities
- defined by \term$_1$ {\ldots} \term$_n$.
-
- \item {\tt field\_simplify\_eq} in $H$
- performs the simplification in the assumption $H$.
-
- \item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$] in $H$}
- performs the simplification in the assumption $H$ using
- the equalities
- defined by \term$_1$ {\ldots} \term$_n$.
-\end{Variants}
-
-\asection{Adding a new field structure
-\comindex{Add Field}}
-
-Declaring a new field consists in proving that a field signature (a
-carrier set, an equality, and field operations: {\tt
-Field\_theory.field\_theory} and {\tt Field\_theory.semi\_field\_theory})
-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{setoidtactics}). The definition
-of fields and semi-fields is:
-\begin{verbatim}
-Record field_theory : Prop := mk_field {
- F_R : ring_theory rO rI radd rmul rsub ropp req;
- F_1_neq_0 : ~ 1 == 0;
- Fdiv_def : forall p q, p / q == p * / q;
- Finv_l : forall p, ~ p == 0 -> / p * p == 1
-}.
-
-Record semi_field_theory : Prop := mk_sfield {
- SF_SR : semi_ring_theory rO rI radd rmul req;
- SF_1_neq_0 : ~ 1 == 0;
- SFdiv_def : forall p q, p / q == p * / q;
- SFinv_l : forall p, ~ p == 0 -> / p * p == 1
-}.
-\end{verbatim}
-
-The result of the normalization process is a fraction represented by
-the following type:
-\begin{verbatim}
-Record linear : Type := mk_linear {
- num : PExpr C;
- denum : PExpr C;
- condition : list (PExpr C) }.
-\end{verbatim}
-where {\tt num} and {\tt denum} are the numerator and denominator;
-{\tt condition} is a list of expressions that have appeared as a
-denominator during the normalization process. These expressions must
-be proven different from zero for the correctness of the algorithm.
-
-The syntax for adding a new field is {\tt Add Field $name$ : $field$
-($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used
-for error messages. $field$ is a proof that the field signature
-satisfies the (semi-)field axioms. The optional list of modifiers is
-used to tailor the behaviour of the tactic. Since field tactics are
-built upon ring tactics, all mofifiers of the {\tt Add Ring}
-apply. There is only one specific modifier:
-\begin{description}
-\item[completeness \term] allows the field tactic to prove
- automatically that the image of non-zero coefficients are mapped to
- non-zero elements of the field. \term is a proof of {\tt forall x y,
- [x] == [y] -> x?=!y = true}, which is the completeness of equality
- on coefficients w.r.t. the field equality.
-\end{description}
-
-\asection{Legacy implementation}
-
-\Warning This tactic is the {\tt ring} tactic of previous versions of
-\Coq{} and it should be considered as deprecated. It will probably be
-removed in future releases. It has been kept only for compatibility
-reasons and in order to help moving existing code to the newer
-implementation described above. For more details, please refer to the
-Coq Reference Manual, version 8.0.
-
-
-\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
-\tacindex{legacy ring}
-\comindex{Add Legacy Ring}
-\comindex{Add Legacy Semi Ring}}
-
-This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
-associative commutative rewriting on every ring. The tactic must be
-loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
-the \texttt{Add Ring} command. The ring of booleans (with \texttt{andb}
-as multiplication and \texttt{xorb} as addition)
-is predefined; if one wants to use the tactic on \texttt{nat} one must
-first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
-\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require
-Import LegacyNArithRing}.
-
-The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
-conclusion. The tactic \texttt{ring} normalizes these terms
-w.r.t. associativity and commutativity and replace them by their
-normal form.
-
-\begin{Variants}
-\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
- acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
- solves the equality by reflexivity.
-
-\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
- S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
- proof that \texttt{forall (n:nat), S n = plus (S O) n}.
-
-\end{Variants}
-
-You can have a look at the files \texttt{LegacyRing.v},
-\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
-\texttt{Add Ring} command.
-
-\subsection{Add a ring structure}
-
-It can be done in the \Coq toplevel (No ML file to edit and to link
-with \Coq). First, \texttt{ring} can handle two kinds of structure:
-rings and semi-rings. Semi-rings are like rings without an opposite to
-addition. Their precise specification (in \gallina) can be found in
-the file
-
-\begin{quotation}
-\begin{verbatim}
-plugins/ring/Ring_theory.v
-\end{verbatim}
-\end{quotation}
-
-The typical example of ring is \texttt{Z}, the typical
-example of semi-ring is \texttt{nat}.
-
-The specification of a
-ring is divided in two parts: first the record of constants
-($\oplus$, $\otimes$, 1, 0, $\ominus$) and then the theorems
-(associativity, commutativity, etc.).
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_semi_rings.
-
-Variable A : Type.
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-(* There is also a "weakly decidable" equality on A. That means
- that if (A_eq x y)=true then x=y but x=y can arise when
- (A_eq x y)=false. On an abstract ring the function [x,y:A]false
- is a good choice. The proof of A_eq_prop is in this case easy. *)
-Variable Aeq : A -> A -> bool.
-
-Record Semi_Ring_Theory : Prop :=
-{ SR_plus_sym : (n,m:A)[| n + m == m + n |];
- SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
-
- SR_mult_sym : (n,m:A)[| n*m == m*n |];
- SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
- SR_plus_zero_left :(n:A)[| 0 + n == n|];
- SR_mult_one_left : (n:A)[| 1*n == n |];
- SR_mult_zero_left : (n:A)[| 0*n == 0 |];
- SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
- SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
- SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-\begin{small}
-\begin{flushleft}
-\begin{verbatim}
-Section Theory_of_rings.
-
-Variable A : Type.
-
-Variable Aplus : A -> A -> A.
-Variable Amult : A -> A -> A.
-Variable Aone : A.
-Variable Azero : A.
-Variable Aopp : A -> A.
-Variable Aeq : A -> A -> bool.
-
-
-Record Ring_Theory : Prop :=
-{ Th_plus_sym : (n,m:A)[| n + m == m + n |];
- Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
- Th_mult_sym : (n,m:A)[| n*m == m*n |];
- Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
- Th_plus_zero_left :(n:A)[| 0 + n == n|];
- Th_mult_one_left : (n:A)[| 1*n == n |];
- Th_opp_def : (n:A) [| n + (-n) == 0 |];
- Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
- Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
-}.
-\end{verbatim}
-\end{flushleft}
-\end{small}
-
-To define a ring structure on A, you must provide an addition, a
-multiplication, an opposite function and two unities 0 and 1.
-
-You must then prove all theorems that make
-(A,Aplus,Amult,Aone,Azero,Aeq)
-a ring structure, and pack them with the \verb|Build_Ring_Theory|
-constructor.
-
-Finally to register a ring the syntax is:
-
-\comindex{Add Legacy Ring}
-\begin{quotation}
- \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
- \texttt{[} \textit{c1 \dots cn} \texttt{].}
-\end{quotation}
-
-\noindent where \textit{A} is a term of type \texttt{Set},
-\textit{Aplus} is a term of type \texttt{A->A->A},
-\textit{Amult} is a term of type \texttt{A->A->A},
-\textit{Aone} is a term of type \texttt{A},
-\textit{Azero} is a term of type \texttt{A},
-\textit{Ainv} is a term of type \texttt{A->A},
-\textit{Aeq} is a term of type \texttt{A->bool},
-\textit{T} is a term of type
-\texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv
- Aeq}\texttt{)}.
-The arguments \textit{c1 \dots cn},
-are the names of constructors which define closed terms: a
-subterm will be considered as a constant if it is either one of the
-terms \textit{c1 \dots cn} or the application of one of these terms to
-closed terms. For \texttt{nat}, the given constructors are \texttt{S}
-and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
-\texttt{(S (S O))}, \ldots
-
-\begin{Variants}
-\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T}
- \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
- Ring}
-
- There are two differences with the \texttt{Add Ring} command: there
- is no inverse function and the term $T$ must be of type
- \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
- Aeq}\texttt{)}.
-
-\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv
- Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
-
- This command should be used for when the operations of rings are not
- computable; for example the real numbers of
- \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but
- you still may want to \textit{rewrite} it to $1$ using the ring
- axioms. The argument \texttt{Aeq} is not used; a good choice for
- that function is \verb+[x:A]false+.
-
-\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
- Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
-
-\end{Variants}
-
-\begin{ErrMsgs}
-\item \errindex{Not a valid (semi)ring theory}.
-
- That happens when the typing condition does not hold.
-\end{ErrMsgs}
-
-Currently, the hypothesis is made than no more than one ring structure
-may be declared for a given type in \texttt{Set} or \texttt{Type}.
-This allows automatic detection of the theory used to achieve the
-normalization. On popular demand, we can change that and allow several
-ring structures on the same set.
-
-The table of ring theories is compatible with the \Coq\
-sectioning mechanism. If you declare a ring inside a section, the
-declaration will be thrown away when closing the section.
-And when you load a compiled file, all the \texttt{Add Ring}
-commands of this file that are not inside a section will be loaded.
-
-The typical example of ring is \texttt{Z}, and the typical example of
-semi-ring is \texttt{nat}. Another ring structure is defined on the
-booleans.
-
-\Warning Only the ring of booleans is loaded by default with the
-\texttt{Ring} module. To load the ring structure for \texttt{nat},
-load the module \texttt{ArithRing}, and for \texttt{Z},
-load the module \texttt{ZArithRing}.
-
-\subsection{\tt legacy field
-\tacindex{legacy field}}
-
-This tactic written by David~Delahaye and Micaela~Mayero solves equalities
-using commutative field theory. Denominators have to be non equal to zero and,
-as this is not decidable in general, this tactic may generate side conditions
-requiring some expressions to be non equal to zero. This tactic must be loaded
-by {\tt Require Import LegacyField}. Field theories are declared (as for
-{\tt legacy ring}) with
-the {\tt Add Legacy Field} command.
-
-\subsection{\tt Add Legacy Field
-\comindex{Add Legacy Field}}
-
-This vernacular command adds a commutative field theory to the database for the
-tactic {\tt field}. You must provide this theory as follows:
-\begin{flushleft}
-{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
-Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
-\end{flushleft}
-where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
-a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
- A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
- Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
-type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
- {\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
-of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
-and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
- {\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
-To build a ring theory, refer to Chapter~\ref{ring} for more details.
-
-This command adds also an entry in the ring theory table if this theory is not
-already declared. So, it is useless to keep, for a given type, the {\tt Add
-Ring} command if you declare a theory with {\tt Add Field}, except if you plan
-to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
-module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
-Require Import Ring} if you want to call the {\tt ring} tactic.
-
-\begin{Variants}
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Field }with minus:={\it Aminus}}
-
-Adds also the term {\it Aminus} which must be a constant expressed by
-means of {\it Aopp}.
-
-\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
-{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
-{\tt \phantom{Add Legacy Field }with div:={\it Adiv}}
-
-Adds also the term {\it Adiv} which must be a constant expressed by
-means of {\it Ainv}.
-
-\end{Variants}
-
-\SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
-legacy field}.
-
-\asection{History of \texttt{ring}}
-
-First Samuel Boutin designed the tactic \texttt{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:
-
-\begin{coq_eval}
-Require Import ZArith.
-Open Scope Z_scope.
-\end{coq_eval}
-\begin{coq_example}
-Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
-\end{coq_example}
-\begin{coq_example*}
-intros; rewrite (Zmult_comm y z); reflexivity.
-Save toto.
-\end{coq_example*}
-\begin{coq_example}
-Print toto.
-\end{coq_example}
-
-At each step of rewriting, the whole context is duplicated in the proof
-term. Then, a tactic that does hundreds of rewriting generates huge proof
-terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it
-using reflection (see his article in TACS'97 \cite{Bou97}). Later, the
-stuff was rewritten by Patrick
-Loiseleur: the new tactic does not any more require \texttt{ACDSimpl}
-to compile and it makes use of $\beta\delta\iota$-reduction
-not only to replace the rewriting steps, but also to achieve the
-interleaving of computation and
-reasoning (see \ref{DiscussReflection}). He also wrote a
-few ML code for the \texttt{Add Ring} command, that allow to register
-new rings dynamically.
-
-Proofs terms generated by \texttt{ring} are quite small, they are
-linear in the number of $\oplus$ and $\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.
-
-\asection{Discussion}
-\label{DiscussReflection}
-
-Efficiency is not the only motivation to use reflection
-here. \texttt{ring} also deals with constants, it rewrites for example the
-expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the
-tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the
-expression $34 + 2*(x - 1) + 12$ is interpreted as
-$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$,
-with the variables mapping
-$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is
-rewritten to $34 - x + 2*x + 12$, very far from the expected
-result. Here rewriting is not sufficient: you have to do some kind of
-reduction (some kind of \textit{computation}) to achieve the
-normalization.
-
-The tactic \texttt{ring} is not only faster than a classical one:
-using reflection, we get for free integration of computation and
-reasoning that would be very complex to implement in the classic fashion.
-
-Is it the ultimate way to write tactics? The answer is: yes and
-no. The \texttt{ring} tactic uses intensively the conversion rule of
-\CIC, that is replaces proof by computation the most as it is
-possible. It can be useful in all situations where a classical tactic
-generates huge proof terms. Symbolic Processing and Tautologies are in
-that case. But there are also tactics like \texttt{auto} or
-\texttt{linear} that do many complex computations, using side-effects
-and backtracking, and generate a small proof term. Clearly, it would
-be significantly less efficient to replace them by tactics using
-reflection.
-
-Another idea suggested by Benjamin Werner: reflection could be used to
-couple an external tool (a rewriting program or a model checker) with
-\Coq. We define (in \Coq) a type of terms, a type of \emph{traces},
-and prove a correction theorem that states that \emph{replaying
-traces} is safe w.r.t some interpretation. Then we let the external
-tool do every computation (using side-effects, backtracking,
-exception, or others features that are not available in pure lambda
-calculus) to produce the trace: now we can check in Coq{} that the
-trace has the expected semantic by applying the correction lemma.
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "Reference-Manual"
-%%% End:
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-25 12:35:41 +0000