diff options
Diffstat (limited to 'doc/sphinx/addendum/ring.rst')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 736 |
1 files changed, 736 insertions, 0 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst new file mode 100644 index 000000000..d9b8b8c52 --- /dev/null +++ b/doc/sphinx/addendum/ring.rst @@ -0,0 +1,736 @@ +\achapter{The \texttt{ring} and \texttt{field} tactic families} +%HEVEA\cutname{ring.html} +\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. +\end{coq_example*} +\begin{coq_example} +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 relevant. 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 behavior 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 outputting 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/InitialRing.v} for examples of sign function. +\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use monomials +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/InitialRing.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 expression. 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. +\end{coq_example*} +\begin{coq_example} +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 + canceled. + + \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 relevant. 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 behavior of the tactic. Since field tactics are +built upon ring tactics, all modifiers 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{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 (Z.mul_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: |