diff options
Diffstat (limited to 'doc/refman/Polynom.tex')
| -rw-r--r-- | doc/refman/Polynom.tex | 543 |
1 files changed, 362 insertions, 181 deletions
diff --git a/doc/refman/Polynom.tex b/doc/refman/Polynom.tex index 70889c9d..30dfa93d 100644 --- a/doc/refman/Polynom.tex +++ b/doc/refman/Polynom.tex @@ -1,10 +1,13 @@ \achapter{The \texttt{ring} tactic} -\aauthor{Patrick Loiseleur and Samuel Boutin} +\aauthor{Bruno Barras, Benjamin Gr\'egoire and Assia + Mahboubi\footnote{based on previous work from + 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 @@ -14,20 +17,21 @@ $\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 +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} @@ -55,7 +59,7 @@ expression in the \gallina\ language. For example in the ring \end{verbatim} \end{quotation} -\noindent As a ring expression, is has 3 subterms. Give each subterm a +\noindent As a ring expression, it has 3 subterms. Give each subterm a number in an arbitrary order: \begin{tabular}{ccl} @@ -90,64 +94,339 @@ 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: +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) 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 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}; for \texttt{Z}, do \texttt{Require Import +ZArithRing}; for \texttt{N}, do \texttt{Require Import +NArithRing}. + +\Example +\begin{coq_eval} +Reset Initial. +Require Import ZArith. +Open Scope Z_scope. +\end{coq_eval} +\begin{coq_example} +Require Import ZArithRing. +Goal forall a b c:Z, + (a + b + c) * (a + b + c) = + a * a + b * b + 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} +Reset Initial. +\end{coq_eval} -\begin{quotation} +\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} + +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} -Require Ring. + 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} -\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. +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} + +The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$ +($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used +for error messages. $ring$ is a proof that the ring signature +satisfies the (semi-)ring axioms. The optional list of modifiers is +used to tailor the behaviour 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. \term{} is + the correctness proof of an equality test {\tt ?=!}. 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. \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. \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 + Ring\_tac.NotConstant}. Abstract (semi-)rings need not define this. +\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. +\end{description} -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{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} -\begin{quotation} -\texttt{ring} $term_1$ \dots{} $term_n$ -\end{quotation} -\tacindex{ring} +\asection{How does it work?} -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 +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. -\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. +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{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.} +\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. +\end{verbatim} +\end{flushleft} +\end{small} - \texttt{Use Add [Semi] Ring to declare it} +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}$. - 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} +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{Legacy implementation} - 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$. +\Warning This tactic is the {\tt ring} tactic of previous versions of +\Coq{} and it should be considered as deprecated. It will probably be +removed in future releases. It has been kept only for compatibility +reasons and in order to help moving existing code to the newer +implementation described above. For more details, please refer to the +Coq Reference Manual, version 8.0. - \ErrMsg\errindex{This goal is not an equality} + +\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$ +\tacindex{legacy ring} +\comindex{Add Legacy Ring} +\comindex{Add Legacy Semi Ring}} + +This tactic, written by Samuel Boutin and Patrick Loiseleur, applies +associative commutative rewriting on every ring. The tactic must be +loaded by \texttt{Require Import LegacyRing}. The ring must be declared in +the \texttt{Add Ring} command. The ring of booleans +is predefined; if one wants to use the tactic on \texttt{nat} one must +first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do +\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require +Import LegacyNArithRing}. + +The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal +conclusion. The tactic \texttt{ring} normalizes these terms +w.r.t. associativity and commutativity and replace them by their +normal form. + +\begin{Variants} +\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it + acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then + solves the equality by reflexivity. + +\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite + S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a + proof that \texttt{forall (n:nat), S n = plus (S O) n}. \end{Variants} -\asection{Add a ring structure} +You can have a look at the files \texttt{LegacyRing.v}, +\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the +\texttt{Add Ring} command. + +\subsection{Add a ring structure} It can be done in the \Coq toplevel (No ML file to edit and to link with \Coq). First, \texttt{ring} can handle two kinds of structure: @@ -242,9 +521,9 @@ constructor. Finally to register a ring the syntax is: -\comindex{Add Ring} +\comindex{Add Legacy Ring} \begin{quotation} - \texttt{Add Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T} + \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T} \texttt{[} \textit{c1 \dots cn} \texttt{].} \end{quotation} @@ -267,8 +546,8 @@ 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 +\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} + \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi Ring} There are two differences with the \texttt{Add Ring} command: there @@ -276,8 +555,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, \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} +\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv + Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring} This command should be used for when the operations of rings are not computable; for example the real numbers of @@ -286,8 +565,8 @@ and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, 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} +\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero + Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring} \end{Variants} @@ -318,90 +597,6 @@ booleans. 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}. @@ -463,40 +658,26 @@ 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 +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! - +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 |