diff options
Diffstat (limited to 'doc/refman/Polynom.tex')
| -rw-r--r-- | doc/refman/Polynom.tex | 504 |
1 files changed, 504 insertions, 0 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex new file mode 100644 index 00000000..70889c9d --- /dev/null +++ b/doc/refman/Polynom.tex @@ -0,0 +1,504 @@ +\achapter{The \texttt{ring} tactic} +\aauthor{Patrick Loiseleur and Samuel Boutin} +\label{ring} +\tacindex{ring} + +This chapter presents the \texttt{ring} tactic. + +\asection{What does this tactic?} + +\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 (possibly equal to 1, in +which case we omit it) 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. 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$. +\item For the classical propositional calculus (or the boolean rings) + the normal form is what logicians call \textit{disjunctive normal + form}: every formula is equivalent to a disjunction of + conjunctions of atoms. (Here $\oplus$ is $\vee$, $\otimes$ is + $\wedge$, variables are atoms and the only constants are T and F) +\end{Examples} + +\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, is 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} + +Under a session launched by \texttt{coqtop} or \texttt{coqtop -full}, +load the \texttt{ring} files with the command: + +\begin{quotation} +\begin{verbatim} +Require Ring. +\end{verbatim} +\end{quotation} + +It does not work under \texttt{coqtop -opt} because the compiled ML +objects used by the tactic are not linked in this binary image, and +dynamic loading of native code is not possible in \ocaml. + +In order to use \texttt{ring} on naturals, load \texttt{ArithRing} +instead; for binary integers, load the module \texttt{ZArithRing}. + +Then, to normalize the terms $term_1$, \dots, $term_n$ in +the current subgoal, use the tactic: + +\begin{quotation} +\texttt{ring} $term_1$ \dots{} $term_n$ +\end{quotation} +\tacindex{ring} + +Then the tactic guesses the type of given terms, the ring theory to +use, the variables map, and replace each term with its normal form. +The variables map is common to all terms + +\Warning \texttt{ring $term_1$; ring $term_2$} is not equivalent to +\texttt{ring $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. + +\begin{ErrMsgs} +\item \errindex{All terms must have the same type} +\item \errindex{Don't know what to do with this goal} +\item \errindex{No Declared Ring Theory for \term.} + + \texttt{Use Add [Semi] Ring to declare it} + + That happens when all terms have the same type \term, but there is + no declared ring theory for this set. See below. +\end{ErrMsgs} + +\begin{Variants} +\item \texttt{ring} + + That works if the current goal is an equality between two + polynomials. It will normalize both sides of the + equality, solve it if the normal forms are equal and in other cases + try to simplify the equality using \texttt{congr\_eqT} and \texttt{refl\_equal} + to reduce $x + y = x + z$ to $y = z$ and $x * z = x * y$ to $y = z$. + + \ErrMsg\errindex{This goal is not an equality} + +\end{Variants} + +\asection{Add a ring structure} + +It can be done in the \Coq toplevel (No ML file to edit and to link +with \Coq). First, \texttt{ring} can handle two kinds of structure: +rings and semi-rings. Semi-rings are like rings without an opposite to +addition. Their precise specification (in \gallina) can be found in +the file + +\begin{quotation} +\begin{verbatim} +contrib/ring/Ring_theory.v +\end{verbatim} +\end{quotation} + +The typical example of ring is \texttt{Z}, the typical +example of semi-ring is \texttt{nat}. + +The specification of a +ring is divided in two parts: first the record of constants +($\oplus$, $\otimes$, 1, 0, $\ominus$) and then the theorems +(associativity, commutativity, etc.). + +\begin{small} +\begin{flushleft} +\begin{verbatim} +Section Theory_of_semi_rings. + +Variable A : Type. +Variable Aplus : A -> A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +(* There is also a "weakly decidable" equality on A. That means + that if (A_eq x y)=true then x=y but x=y can arise when + (A_eq x y)=false. On an abstract ring the function [x,y:A]false + is a good choice. The proof of A_eq_prop is in this case easy. *) +Variable Aeq : A -> A -> bool. + +Record Semi_Ring_Theory : Prop := +{ SR_plus_sym : (n,m:A)[| n + m == m + n |]; + SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |]; + + SR_mult_sym : (n,m:A)[| n*m == m*n |]; + SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |]; + SR_plus_zero_left :(n:A)[| 0 + n == n|]; + SR_mult_one_left : (n:A)[| 1*n == n |]; + SR_mult_zero_left : (n:A)[| 0*n == 0 |]; + SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; + SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p; + SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. +\end{verbatim} +\end{flushleft} +\end{small} + +\begin{small} +\begin{flushleft} +\begin{verbatim} +Section Theory_of_rings. + +Variable A : Type. + +Variable Aplus : A -> A -> A. +Variable Amult : A -> A -> A. +Variable Aone : A. +Variable Azero : A. +Variable Aopp : A -> A. +Variable Aeq : A -> A -> bool. + + +Record Ring_Theory : Prop := +{ Th_plus_sym : (n,m:A)[| n + m == m + n |]; + Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |]; + Th_mult_sym : (n,m:A)[| n*m == m*n |]; + Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |]; + Th_plus_zero_left :(n:A)[| 0 + n == n|]; + Th_mult_one_left : (n:A)[| 1*n == n |]; + Th_opp_def : (n:A) [| n + (-n) == 0 |]; + Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |]; + Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y +}. +\end{verbatim} +\end{flushleft} +\end{small} + +To define a ring structure on A, you must provide an addition, a +multiplication, an opposite function and two unities 0 and 1. + +You must then prove all theorems that make +(A,Aplus,Amult,Aone,Azero,Aeq) +a ring structure, and pack them with the \verb|Build_Ring_Theory| +constructor. + +Finally to register a ring the syntax is: + +\comindex{Add Ring} +\begin{quotation} + \texttt{Add Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T} + \texttt{[} \textit{c1 \dots cn} \texttt{].} +\end{quotation} + +\noindent where \textit{A} is a term of type \texttt{Set}, +\textit{Aplus} is a term of type \texttt{A->A->A}, +\textit{Amult} is a term of type \texttt{A->A->A}, +\textit{Aone} is a term of type \texttt{A}, +\textit{Azero} is a term of type \texttt{A}, +\textit{Ainv} is a term of type \texttt{A->A}, +\textit{Aeq} is a term of type \texttt{A->bool}, +\textit{T} is a term of type +\texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv + Aeq}\texttt{)}. +The arguments \textit{c1 \dots cn}, +are the names of constructors which define closed terms: a +subterm will be considered as a constant if it is either one of the +terms \textit{c1 \dots cn} or the application of one of these terms to +closed terms. For \texttt{nat}, the given constructors are \texttt{S} +and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, +\texttt{(S (S O))}, \ldots + +\begin{Variants} +\item \texttt{Add Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} + \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Semi + Ring} + + There are two differences with the \texttt{Add Ring} command: there + is no inverse function and the term $T$ must be of type + \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero + Aeq}\texttt{)}. + +\item \texttt{Add Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv + Aeq T}\texttt{.}\comindex{Add Abstract Ring} + + This command should be used for when the operations of rings are not + computable; for example the real numbers of + \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but + you still may want to \textit{rewrite} it to $1$ using the ring + axioms. The argument \texttt{Aeq} is not used; a good choice for + that function is \verb+[x:A]false+. + +\item \texttt{Add Abstract Semi Ring} \textit{A Aplus Amult Aone Azero + Aeq T}\texttt{.}\comindex{Add Abstract Semi Ring} + +\end{Variants} + +\begin{ErrMsgs} +\item \errindex{Not a valid (semi)ring theory}. + + That happens when the typing condition does not hold. +\end{ErrMsgs} + +Currently, the hypothesis is made than no more than one ring structure +may be declared for a given type in \texttt{Set} or \texttt{Type}. +This allows automatic detection of the theory used to achieve the +normalization. On popular demand, we can change that and allow several +ring structures on the same set. + +The table of ring theories is compatible with the \Coq\ +sectioning mechanism. If you declare a ring inside a section, the +declaration will be thrown away when closing the section. +And when you load a compiled file, all the \texttt{Add Ring} +commands of this file that are not inside a section will be loaded. + +The typical example of ring is \texttt{Z}, and the typical example of +semi-ring is \texttt{nat}. Another ring structure is defined on the +booleans. + +\Warning Only the ring of booleans is loaded by default with the +\texttt{Ring} module. To load the ring structure for \texttt{nat}, +load the module \texttt{ArithRing}, and for \texttt{Z}, +load the module \texttt{ZArithRing}. + + +\asection{How does it work?} + +The code of \texttt{ring} is a good example of tactic written using +\textit{reflection} (or \textit{internalization}, it is synonymous). +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\_normalize.v}. Here a type for polynomials is defined: + +\begin{small} +\begin{flushleft} +\begin{verbatim} +Inductive Type polynomial := + Pvar : idx -> polynomial +| Pconst : A -> polynomial +| Pplus : polynomial -> polynomial -> polynomial +| Pmult : polynomial -> polynomial -> polynomial +| Popp : polynomial -> polynomial. +\end{verbatim} +\end{flushleft} +\end{small} + +There is also a type to represent variables maps, and an +interpretation function, that maps a variables map and a polynomial to an +element of the concrete ring: + +\begin{small} +\begin{flushleft} +\begin{verbatim} +Definition polynomial_simplify := [...] +Definition interp : (varmap A) -> (polynomial A) -> A := [...] +\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} +Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial) + (interp v (polynomial_simplify p)) + =(interp v p). +\end{verbatim} +\end{flushleft} +\end{small} + +(The actual code is slightly more complex: for efficiency, +there is a special datatype to represent normalized polynomials, +i.e. ``canonical sums''. But the idea is still the same). + +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|(interp v ap)|. Then we +replace it by \verb|(interp v (polynomial_simplify 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{(interp v ap)} \\ + & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\ +\texttt{p'} + & $\leftarrow_{\beta\delta\iota}$ + & \texttt{(interp v (polynomial\_simplify 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{History of \texttt{ring}} + +First Samuel Boutin designed the tactic \texttt{ACDSimpl}. +This tactic did lot of rewriting. But the proofs +terms generated by rewriting were too big for \Coq's type-checker. +Let us see why: + +\begin{coq_eval} +Require Import ZArith. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example} +Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y. +\end{coq_example} +\begin{coq_example*} +intros; rewrite (Zmult_comm y z); reflexivity. +Save toto. +\end{coq_example*} +\begin{coq_example} +Print toto. +\end{coq_example} + +At each step of rewriting, the whole context is duplicated in the proof +term. Then, a tactic that does hundreds of rewriting generates huge proof +terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it +using reflection (see his article in TACS'97 \cite{Bou97}). Later, the +stuff was rewritten by Patrick +Loiseleur: the new tactic does not any more require \texttt{ACDSimpl} +to compile and it makes use of $\beta\delta\iota$-reduction +not only to replace the rewriting steps, but also to achieve the +interleaving of computation and +reasoning (see \ref{DiscussReflection}). He also wrote a +few ML code for the \texttt{Add Ring} command, that allow to register +new rings dynamically. + +Proofs terms generated by \texttt{ring} are quite small, they are +linear in the number of $\oplus$ and $\otimes$ operations in the +normalized terms. Type-checking those terms requires some time because it +makes a large use of the conversion rule, but +memory requirements are much smaller. + +\asection{Discussion} +\label{DiscussReflection} + +Efficiency is not the only motivation to use reflection +here. \texttt{ring} also deals with constants, it rewrites for example the +expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the +tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the +expression $34 + 2*(x - 1) + 12$ is interpreted as +$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$, +with the variables mapping +$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is +rewritten to $34 - x + 2*x + 12$, very far from the expected +result. Here rewriting is not sufficient: you have to do some kind of +reduction (some kind of \textit{computation}) to achieve the +normalization. + +The tactic \texttt{ring} is not only faster than a classical one: +using reflection, we get for free integration of computation and +reasoning that would be very complex to implement in the classic fashion. + +Is it the ultimate way to write tactics? +The answer is: yes and no. The \texttt{ring} tactic +uses intensively the conversion +rule of \CIC, that is replaces proof by computation the most as it is +possible. It can be useful in all situations where a classical tactic +generates huge proof terms. Symbolic Processing and Tautologies are +in that case. But there are also tactics like \texttt{Auto} or +\texttt{Linear}: that do many complex computations, using side-effects +and backtracking, and generate + a small proof term. Clearly, it would be a non-sense to +replace them by tactics using reflection. + +Another argument against the reflection is that \Coq, as a +programming language, has many nice features, like dependent types, +but is very far from the +speed and the expressive power of \ocaml. Wait a minute! With \Coq\ +it is possible to extract ML code from \CIC\ terms, right? So, why not +to link the extracted code with \Coq\ to inherit the benefits of the +reflection and the speed of ML tactics? That is called \textit{total + reflection}, and is still an active research subject. With these +technologies it will become possible to bootstrap the type-checker of +\CIC, but there is still some work to achieve that goal. + +Another brilliant idea from Benjamin Werner: reflection could be used +to couple a 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 replay the trace in +Coq{}, and apply the correction lemma. So internalization seems to be +the best way to import \dots{} external proofs! + + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |