\achapter{The \texttt{ring} tactic} \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 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$. \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, 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} 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} \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} 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} 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} \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. \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{Legacy implementation} \Warning This tactic is the {\tt ring} tactic of previous versions of \Coq{} and it should be considered as deprecated. It will probably be removed in future releases. It has been kept only for compatibility reasons and in order to help moving existing code to the newer implementation described above. For more details, please refer to the Coq Reference Manual, version 8.0. \subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$ \tacindex{legacy ring} \comindex{Add Legacy Ring} \comindex{Add Legacy Semi Ring}} This tactic, written by Samuel Boutin and Patrick Loiseleur, applies associative commutative rewriting on every ring. The tactic must be loaded by \texttt{Require Import LegacyRing}. The ring must be declared in the \texttt{Add Ring} command. The ring of booleans is predefined; if one wants to use the tactic on \texttt{nat} one must first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do \texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require Import LegacyNArithRing}. The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal conclusion. The tactic \texttt{ring} normalizes these terms w.r.t. associativity and commutativity and replace them by their normal form. \begin{Variants} \item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then solves the equality by reflexivity. \item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a proof that \texttt{forall (n:nat), S n = plus (S O) n}. \end{Variants} You can have a look at the files \texttt{LegacyRing.v}, \texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the \texttt{Add Ring} command. \subsection{Add a ring structure} It can be done in the \Coq toplevel (No ML file to edit and to link with \Coq). First, \texttt{ring} can handle two kinds of structure: rings and semi-rings. Semi-rings are like rings without an opposite to addition. Their precise specification (in \gallina) can be found in the file \begin{quotation} \begin{verbatim} 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 Legacy Ring} \begin{quotation} \texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T} \texttt{[} \textit{c1 \dots cn} \texttt{].} \end{quotation} \noindent where \textit{A} is a term of type \texttt{Set}, \textit{Aplus} is a term of type \texttt{A->A->A}, \textit{Amult} is a term of type \texttt{A->A->A}, \textit{Aone} is a term of type \texttt{A}, \textit{Azero} is a term of type \texttt{A}, \textit{Ainv} is a term of type \texttt{A->A}, \textit{Aeq} is a term of type \texttt{A->bool}, \textit{T} is a term of type \texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv Aeq}\texttt{)}. The arguments \textit{c1 \dots cn}, are the names of constructors which define closed terms: a subterm will be considered as a constant if it is either one of the terms \textit{c1 \dots cn} or the application of one of these terms to closed terms. For \texttt{nat}, the given constructors are \texttt{S} and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)}, \texttt{(S (S O))}, \ldots \begin{Variants} \item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T} \texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi Ring} There are two differences with the \texttt{Add Ring} command: there is no inverse function and the term $T$ must be of type \texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero Aeq}\texttt{)}. \item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring} This command should be used for when the operations of rings are not computable; for example the real numbers of \texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but you still may want to \textit{rewrite} it to $1$ using the ring axioms. The argument \texttt{Aeq} is not used; a good choice for that function is \verb+[x:A]false+. \item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring} \end{Variants} \begin{ErrMsgs} \item \errindex{Not a valid (semi)ring theory}. That happens when the typing condition does not hold. \end{ErrMsgs} Currently, the hypothesis is made than no more than one ring structure may be declared for a given type in \texttt{Set} or \texttt{Type}. This allows automatic detection of the theory used to achieve the normalization. On popular demand, we can change that and allow several ring structures on the same set. The table of ring theories is compatible with the \Coq\ sectioning mechanism. If you declare a ring inside a section, the declaration will be thrown away when closing the section. And when you load a compiled file, all the \texttt{Add Ring} commands of this file that are not inside a section will be loaded. The typical example of ring is \texttt{Z}, and the typical example of semi-ring is \texttt{nat}. Another ring structure is defined on the booleans. \Warning Only the ring of booleans is loaded by default with the \texttt{Ring} module. To load the ring structure for \texttt{nat}, load the module \texttt{ArithRing}, and for \texttt{Z}, load the module \texttt{ZArithRing}. \asection{History of \texttt{ring}} First Samuel Boutin designed the tactic \texttt{ACDSimpl}. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big for \Coq's type-checker. Let us see why: \begin{coq_eval} Require Import ZArith. Open Scope Z_scope. \end{coq_eval} \begin{coq_example} Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y. \end{coq_example} \begin{coq_example*} intros; rewrite (Zmult_comm y z); reflexivity. Save toto. \end{coq_example*} \begin{coq_example} Print toto. \end{coq_example} At each step of rewriting, the whole context is duplicated in the proof term. Then, a tactic that does hundreds of rewriting generates huge proof terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it using reflection (see his article in TACS'97 \cite{Bou97}). Later, the stuff was rewritten by Patrick Loiseleur: the new tactic does not any more require \texttt{ACDSimpl} to compile and it makes use of $\beta\delta\iota$-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see \ref{DiscussReflection}). He also wrote a few ML code for the \texttt{Add Ring} command, that allow to register new rings dynamically. Proofs terms generated by \texttt{ring} are quite small, they are linear in the number of $\oplus$ and $\otimes$ operations in the normalized terms. Type-checking those terms requires some time because it makes a large use of the conversion rule, but memory requirements are much smaller. \asection{Discussion} \label{DiscussReflection} Efficiency is not the only motivation to use reflection here. \texttt{ring} also deals with constants, it rewrites for example the expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the expression $34 + 2*(x - 1) + 12$ is interpreted as $V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$, with the variables mapping $\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is rewritten to $34 - x + 2*x + 12$, very far from the expected result. Here rewriting is not sufficient: you have to do some kind of reduction (some kind of \textit{computation}) to achieve the normalization. The tactic \texttt{ring} is not only faster than a classical one: using reflection, we get for free integration of computation and reasoning that would be very complex to implement in the classic fashion. Is it the ultimate way to write tactics? The answer is: yes and no. The \texttt{ring} tactic uses intensively the conversion rule of \CIC, that is replaces proof by computation the most as it is possible. It can be useful in all situations where a classical tactic generates huge proof terms. Symbolic Processing and Tautologies are in that case. But there are also tactics like \texttt{auto} or \texttt{linear} that do many complex computations, using side-effects and backtracking, and generate a small proof term. Clearly, it would be significantly less efficient to replace them by tactics using reflection. Another idea suggested by Benjamin Werner: reflection could be used to couple an external tool (a rewriting program or a model checker) with \Coq. We define (in \Coq) a type of terms, a type of \emph{traces}, and prove a correction theorem that states that \emph{replaying traces} is safe w.r.t some interpretation. Then we let the external tool do every computation (using side-effects, backtracking, exception, or others features that are not available in pure lambda calculus) to produce the trace: now we can check in Coq{} that the trace has the expected semantic by applying the correction lemma. %%% Local Variables: %%% mode: latex %%% TeX-master: "Reference-Manual" %%% End: