From 58abe4ac66a05d4cffd8ed7f7b0ed3acd112abcc Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 22 Mar 2018 15:01:53 +0100 Subject: [Sphinx] Move chapter 25 to new infrastructure --- Makefile.doc | 1 - doc/refman/Polynom.tex | 736 ---------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/addendum/ring.rst | 736 ++++++++++++++++++++++++++++++++++++++++ 4 files changed, 736 insertions(+), 738 deletions(-) delete mode 100644 doc/refman/Polynom.tex create mode 100644 doc/sphinx/addendum/ring.rst diff --git a/Makefile.doc b/Makefile.doc index 08b4cb7fb..8dd73a153 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -60,7 +60,6 @@ REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex \ - Polynom.v.tex \ Setoid.v.tex Universes.v.tex \ Misc.v.tex) diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex deleted file mode 100644 index d9b8b8c52..000000000 --- a/doc/refman/Polynom.tex +++ /dev/null @@ -1,736 +0,0 @@ -\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: diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 13c3c0aac..57d867060 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -117,7 +117,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \part{Addendum to the Reference Manual} \include{AddRefMan-pre}% -\include{Polynom.v}% = Ring \include{Setoid.v}% Tactique pour les setoides \include{AsyncProofs}% Paral-ITP \include{Universes.v}% Universe polymorphes 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: -- cgit v1.2.3