1
\achapter{The \texttt{ring} and \texttt{field} tactic families}
2
\aauthor{Bruno Barras, Benjamin Gr\'egoire and Assia
3
Mahboubi\footnote{based on previous work from
4
Patrick Loiseleur and Samuel Boutin}}
8
This chapter presents the tactics dedicated to deal with ring and
12
\asection{What does this tactic?}
14
\texttt{ring} does associative-commutative rewriting in ring and semi-ring
15
structures. Assume you have two binary functions $\oplus$ and $\otimes$
16
that are associative and commutative, with $\oplus$ distributive on
17
$\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
18
$\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1,
19
\dots$ and constants by application of $\oplus$ and $\otimes$.
21
Let an {\it ordered product} be a product of variables $V_{i_1}
22
\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le
23
i_n$. Let a \textit{monomial} be the product of a constant and an
24
ordered product. We can order the monomials by the lexicographic
25
order on products of variables. Let a \textit{canonical sum} be an
26
ordered sum of monomials that are all different, i.e. each monomial in
27
the sum is strictly less than the following monomial according to the
28
lexicographic order. It is an easy theorem to show that every
29
polynomial is equivalent (modulo the ring properties) to exactly one
30
canonical sum. This canonical sum is called the \textit{normal form}
31
of the polynomial. In fact, the actual representation shares monomials
32
with same prefixes. So what does \texttt{ring}? It normalizes
33
polynomials over any ring or semi-ring structure. The basic use of
34
\texttt{ring} is to simplify ring expressions, so that the user does
35
not have to deal manually with the theorems of associativity and
39
\item In the ring of integers, the normal form of
40
$x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
41
\item For the classical propositional calculus (or the boolean rings)
42
the normal form is what logicians call \textit{disjunctive normal
43
form}: every formula is equivalent to a disjunction of
44
conjunctions of atoms. (Here $\oplus$ is $\vee$, $\otimes$ is
45
$\wedge$, variables are atoms and the only constants are T and F)
48
\texttt{ring} is also able to compute a normal form modulo monomial
49
equalities. For example, under the hypothesis that $x^2 = yz$,
50
the normal form of $(x + 1)x - x - zy$ is 0.
52
\asection{The variables map}
54
It is frequent to have an expression built with + and
55
$\times$, but rarely on variables only.
56
Let us associate a number to each subterm of a ring
57
expression in the \gallina\ language. For example in the ring
58
\texttt{nat}, consider the expression:
62
(plus (mult (plus (f (5)) x) x)
63
(mult (if b then (4) else (f (3))) (2)))
67
\noindent As a ring expression, it has 3 subterms. Give each subterm a
68
number in an arbitrary order:
71
0 & $\mapsto$ & \verb|if b then (4) else (f (3))| \\
72
1 & $\mapsto$ & \verb|(f (5))| \\
73
2 & $\mapsto$ & \verb|x| \\
76
\noindent Then normalize the ``abstract'' polynomial
78
$$((V_1 \otimes V_2) \oplus V_2) \oplus (V_0 \otimes 2) $$
80
\noindent In our example the normal form is:
82
$$(2 \otimes V_0) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2)$$
84
\noindent Then substitute the variables by their values in the variables map to
85
get the concrete normal polynomial:
89
(plus (mult (2) (if b then (4) else (f (3))))
90
(plus (mult (f (5)) x) (mult x x)))
94
\asection{Is it automatic?}
96
Yes, building the variables map and doing the substitution after
97
normalizing is automatically done by the tactic. So you can just forget
98
this paragraph and use the tactic according to your intuition.
100
\asection{Concrete usage in \Coq
102
\tacindex{ring\_simplify}}
104
The {\tt ring} tactic solves equations upon polynomial expressions of
105
a ring (or semi-ring) structure. It proceeds by normalizing both hand
106
sides of the equation (w.r.t. associativity, commutativity and
107
distributivity, constant propagation, rewriting of monomials)
108
and comparing syntactically the results.
110
{\tt ring\_simplify} applies the normalization procedure described
111
above to the terms given. The tactic then replaces all occurrences of
112
the terms given in the conclusion of the goal by their normal
113
forms. If no term is given, then the conclusion should be an equation
114
and both hand sides are normalized.
116
The tactic must be loaded by \texttt{Require Import Ring}. The ring
117
structures must be declared with the \texttt{Add Ring} command (see
118
below). The ring of booleans is predefined; if one wants to use the
119
tactic on \texttt{nat} one must first require the module
120
\texttt{ArithRing} (exported by \texttt{Arith});
121
for \texttt{Z}, do \texttt{Require Import
122
ZArithRing} or simply \texttt{Require Import ZArith};
123
for \texttt{N}, do \texttt{Require Import NArithRing} or
124
\texttt{Require Import NArith}.
131
Require Import ZArith.
135
a * a + b^2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
144
Goal forall a b:Z, a*b = 0 ->
148
intros a b H; ring [H].
155
\item {\tt ring [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
156
terms modulo ring operations and rewriting of the equalities
157
defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
158
{\ldots} \term$_n$ has to be a proof of some equality $m = p$,
159
where $m$ is a monomial (after ``abstraction''),
160
$p$ a polynomial and $=$ the corresponding equality of the ring structure.
162
\item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in
164
performs the simplification in the hypothesis named {\tt ident}.
167
\Warning \texttt{ring\_simplify \term$_1$; ring\_simplify \term$_2$} is
168
not equivalent to \texttt{ring\_simplify \term$_1$ \term$_2$}. In the
169
latter case the variables map is shared between the two terms, and
170
common subterm $t$ of \term$_1$ and \term$_2$ will have the same
171
associated variable number. So the first alternative should be
172
avoided for terms belonging to the same ring theory.
176
\item \errindex{not a valid ring equation}
177
The conclusion of the goal is not provable in the corresponding ring
179
\item \errindex{arguments of ring\_simplify do not have all the same type}
180
{\tt ring\_simplify} cannot simplify terms of several rings at the
181
same time. Invoke the tactic once per ring structure.
182
\item \errindex{cannot find a declared ring structure over {\tt term}}
183
No ring has been declared for the type of the terms to be
184
simplified. Use {\tt Add Ring} first.
185
\item \errindex{cannot find a declared ring structure for equality
187
Same as above is the case of the {\tt ring} tactic.
190
\asection{Adding a ring structure
193
Declaring a new ring consists in proving that a ring signature (a
194
carrier set, an equality, and ring operations: {\tt
195
Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory})
196
satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are
197
also supported. The equality can be either Leibniz equality, or any
198
relation declared as a setoid (see~\ref{setoidtactics}). The definition
199
of ring and semi-rings (see module {\tt Ring\_theory}) is:
201
Record ring_theory : Prop := mk_rt {
202
Radd_0_l : forall x, 0 + x == x;
203
Radd_sym : forall x y, x + y == y + x;
204
Radd_assoc : forall x y z, x + (y + z) == (x + y) + z;
205
Rmul_1_l : forall x, 1 * x == x;
206
Rmul_sym : forall x y, x * y == y * x;
207
Rmul_assoc : forall x y z, x * (y * z) == (x * y) * z;
208
Rdistr_l : forall x y z, (x + y) * z == (x * z) + (y * z);
209
Rsub_def : forall x y, x - y == x + -y;
210
Ropp_def : forall x, x + (- x) == 0
213
Record semi_ring_theory : Prop := mk_srt {
214
SRadd_0_l : forall n, 0 + n == n;
215
SRadd_sym : forall n m, n + m == m + n ;
216
SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
217
SRmul_1_l : forall n, 1*n == n;
218
SRmul_0_l : forall n, 0*n == 0;
219
SRmul_sym : forall n m, n*m == m*n;
220
SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
221
SRdistr_l : forall n m p, (n + m)*p == n*p + m*p
225
This implementation of {\tt ring} also features a notion of constant
226
that can be parameterized. This can be used to improve the handling of
227
closed expressions when operations are effective. It consists in
228
introducing a type of \emph{coefficients} and an implementation of the
229
ring operations, and a morphism from the coefficient type to the ring
230
carrier type. The morphism needs not be injective, nor surjective. As
231
an example, one can consider the real numbers. The set of coefficients
232
could be the rational numbers, upon which the ring operations can be
233
implemented. The fact that there exists a morphism is defined by the
234
following properties:
236
Record ring_morph : Prop := mkmorph {
239
morph_add : forall x y, [x +! y] == [x]+[y];
240
morph_sub : forall x y, [x -! y] == [x]-[y];
241
morph_mul : forall x y, [x *! y] == [x]*[y];
242
morph_opp : forall x, [-!x] == -[x];
243
morph_eq : forall x y, x?=!y = true -> [x] == [y]
246
Record semi_morph : Prop := mkRmorph {
249
Smorph_add : forall x y, [x +! y] == [x]+[y];
250
Smorph_mul : forall x y, [x *! y] == [x]*[y];
251
Smorph_eq : forall x y, x?=!y = true -> [x] == [y]
254
where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set,
255
{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring
256
operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is
257
an implementation of this equality, and {\tt [x]} is a notation for
258
the image of {\tt x} by the ring morphism.
260
Since {\tt Z} is an initial ring (and {\tt N} is an initial
261
semi-ring), it can always be considered as a set of
262
coefficients. There are basically three kinds of (semi-)rings:
264
\item[abstract rings] to be used when operations are not
265
effective. The set of coefficients is {\tt Z} (or {\tt N} for
267
\item[computational rings] to be used when operations are
268
effective. The set of coefficients is the ring itself. The user only
269
has to provide an implementation for the equality.
270
\item[customized ring] for other cases. The user has to provide the
271
coefficient set and the morphism.
274
This implementation of ring can also recognize simple
275
power expressions as ring expressions. A power function is specified by
276
the following property:
280
Variable Cp_phi : N -> Cpow.
281
Variable rpow : R -> Cpow -> R.
283
Record power_theory : Prop := mkpow_th {
284
rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
291
The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
292
($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used
293
for error messages. The term $ring$ is a proof that the ring signature
294
satisfies the (semi-)ring axioms. The optional list of modifiers is
295
used to tailor the behavior of the tactic. The following list
296
describes their syntax and effects:
298
\item[abstract] declares the ring as abstract. This is the default.
299
\item[decidable \term] declares the ring as computational. The expression
301
the correctness proof of an equality test {\tt ?=!}. Its type should be of
302
the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
303
\item[morphism \term] declares the ring as a customized one. The expression
305
a proof that there exists a morphism between a set of coefficient
306
and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt
307
Ring\_theory.semi\_morph}).
308
\item[setoid \term$_1$ \term$_2$] forces the use of given setoid. The
309
expression \term$_1$ is a proof that the equality is indeed a setoid
310
(see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the
311
ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and
312
{\tt Ring\_theory.sring\_eq\_ext}). This modifier needs not be used if the
313
setoid and morphisms have been declared.
314
\item[constants [\ltac]] specifies a tactic expression that, given a term,
315
returns either an object of the coefficient set that is mapped to
316
the expression via the morphism, or returns {\tt
317
InitialRing.NotConstant}. Abstract (semi-)rings need not define this.
318
\item[preprocess [\ltac]]
319
specifies a tactic that is applied as a preliminary step for {\tt
320
ring} and {\tt ring\_simplify}. It can be used to transform a goal
321
so that it is better recognized. For instance, {\tt S n} can be
322
changed to {\tt plus 1 n}.
323
\item[postprocess [\ltac]] specifies a tactic that is applied as a final step
324
for {\tt ring\_simplify}. For instance, it can be used to undo
325
modifications of the preprocessor.
326
\item[power\_tac {\term} [\ltac]] allows {\tt ring} and {\tt ring\_simplify} to
327
recognize power expressions with a constant positive integer exponent
328
(example: $x^2$). The term {\term} is a proof that a given power function
329
satisfies the specification of a power function ({\term} has to be a
330
proof of {\tt Ring\_theory.power\_theory}) and {\ltac} specifies a
331
tactic expression that, given a term, ``abstracts'' it into an
332
object of type {\tt N} whose interpretation via {\tt Cp\_phi} (the
333
evaluation function of power coefficient) is the original term, or
334
returns {\tt InitialRing.NotConstant} if not a constant coefficient
335
(i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
336
See files {\tt contrib/setoid\_ring/ZArithRing.v} and
337
{\tt contrib/setoid\_ring/RealField.v} for examples.
338
By default the tactic does not recognize power expressions as ring
340
\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
341
when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$.
342
The term {\term} is a proof that a given sign function indicates expressions
343
that are signed ({\term} has to be a
344
proof of {\tt Ring\_theory.get\_sign}). See {\tt contrib/setoid\_ring/IntialRing.v} for examples of sign function.
345
\item[div {\term}] allows {\tt ring} and {\tt ring\_simplify} to use moniomals
346
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
347
division function ({\term} has to be a
348
proof of {\tt Ring\_theory.div\_theory}). For example, this function is
349
called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
350
See {\tt contrib/setoid\_ring/IntialRing.v} for examples of div function.
355
\item \errindex{bad ring structure}
356
The proof of the ring structure provided is not of the expected type.
357
\item \errindex{bad lemma for decidability of equality}
358
The equality function provided in the case of a computational ring
359
has not the expected type.
360
\item \errindex{ring {\it operation} should be declared as a morphism}
361
A setoid associated to the carrier of the ring structure as been
362
found, but the ring operation should be declared as
363
morphism. See~\ref{setoidtactics}.
366
\asection{How does it work?}
368
The code of \texttt{ring} is a good example of tactic written using
369
\textit{reflection}. What is reflection? Basically, it is writing
370
\Coq{} tactics in \Coq, rather than in \ocaml. From the philosophical
371
point of view, it is using the ability of the Calculus of
372
Constructions to speak and reason about itself. For the \texttt{ring}
373
tactic we used \Coq\ as a programming language and also as a proof
374
environment to build a tactic and to prove it correctness.
376
The interested reader is strongly advised to have a look at the file
377
\texttt{Ring\_polynom.v}. Here a type for polynomials is defined:
382
Inductive PExpr : Type :=
384
| PEX : positive -> PExpr
385
| PEadd : PExpr -> PExpr -> PExpr
386
| PEsub : PExpr -> PExpr -> PExpr
387
| PEmul : PExpr -> PExpr -> PExpr
388
| PEopp : PExpr -> PExpr.
393
Polynomials in normal form are defined as:
397
Inductive Pol : Type :=
399
| Pinj : positive -> Pol -> Pol
400
| PX : Pol -> positive -> Pol -> Pol.
404
where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by
405
$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$,
406
$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$.
409
Variables maps are represented by list of ring elements, and two
410
interpretation functions, one that maps a variables map and a
411
polynomial to an element of the concrete ring, and the second one that
412
does the same for normal forms:
416
Definition PEeval : list R -> PExpr -> R := [...].
417
Definition Pphi_dev : list R -> Pol -> R := [...].
422
A function to normalize polynomials is defined, and the big theorem is
423
its correctness w.r.t interpretation, that is:
428
Definition norm : PExpr -> Pol := [...].
430
forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
435
So now, what is the scheme for a normalization proof? Let \texttt{p}
436
be the polynomial expression that the user wants to normalize. First a
437
little piece of ML code guesses the type of \texttt{p}, the ring
438
theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
439
variables map \texttt{v} such that \texttt{p} is
440
$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we
441
replace it by \verb|(Pphi_dev v (norm ap))|, using the
442
main correctness theorem and we reduce it to a concrete expression
443
\texttt{p'}, which is the concrete normal form of
444
\texttt{p}. This is summarized in this diagram:
447
\texttt{p} & $\rightarrow_{\beta\delta\iota}$
448
& \texttt{(PEeval v ap)} \\
449
& & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
451
& $\leftarrow_{\beta\delta\iota}$
452
& \texttt{(Pphi\_dev v (norm ap))}
455
The user do not see the right part of the diagram.
456
From outside, the tactic behaves like a
457
$\beta\delta\iota$ simplification extended with AC rewriting rules.
458
Basically, the proof is only the application of the main
459
correctness theorem to well-chosen arguments.
462
\asection{Dealing with fields
464
\tacindex{field\_simplify}
465
\tacindex{field\_simplify\_eq}}
468
The {\tt field} tactic is an extension of the {\tt ring} to deal with
469
rational expresision. 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
471
For example, if we take $F = (1 - 1/x) x - x + 1$, this gives
472
$ N= (x -1) x - x^2 + x$ and $D= x$. It then calls {\tt ring}
473
to solve $N=0$. Note that {\tt field} also generates non-zero conditions
474
for all the denominators it encounters in the reduction.
475
In our example, it generates the condition $x \neq 0$. These
476
conditions appear as one subgoal which is a conjunction if there are
477
several denominators.
478
Non-zero conditions are {\it always} polynomial expressions. For example
479
when reducing the expression $1/(1 + 1/x)$, two side conditions are
480
generated: $x\neq 0$ and $x + 1 \neq 0$. Factorized expressions are
481
broken since a field is an integral domain, and when the equality test
482
on coefficients is complete w.r.t. the equality of the target field,
483
constants can be proven different from zero automatically.
485
The tactic must be loaded by \texttt{Require Import Field}. New field
486
structures can be declared to the system with the \texttt{Add Field}
487
command (see below). The field of real numbers is defined in module
488
\texttt{RealField} (in texttt{contrib/setoid\_ring}). It is exported
489
by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
490
\texttt{Reals} is enough to use the field tactics on real
491
numbers. Rational numbers in canonical form are also declared as a
492
field in module \texttt{Qcanon}.
500
Require Import Reals.
502
Goal forall x, x <> 0 ->
503
(1 - 1/x) * x - x + 1 = 0.
512
Goal forall x y, y <> 0 -> y = x -> x/y = 1.
515
intros x y H H1; field [H1]; auto.
522
\item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
523
terms modulo field operations and rewriting of the equalities
524
defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
525
{\ldots} \term$_n$ has to be a proof of some equality $m = p$,
526
where $m$ is a monomial (after ``abstraction''),
527
$p$ a polynomial and $=$ the corresponding equality of the field structure.
529
\item {\tt field\_simplify}
530
performs the simplification in the conclusion of the goal, $F_1 = F_2$
531
becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the
532
one for rings) is then applied to $N_1$, $D_1$, $N_2$ and
533
$D_2$. This way, polynomials remain in factorized form during the
534
fraction simplifications. This yields smaller expressions when
535
reducing to the same denominator since common factors can be
538
\item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$]}
539
performs the simplification in the conclusion of the goal using
541
defined by \term$_1$ {\ldots} \term$_n$.
543
\item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
545
performs the simplification in the terms $t_1$ \ldots $t_m$
546
of the conclusion of the goal using
548
defined by \term$_1$ {\ldots} \term$_n$.
550
\item {\tt field\_simplify in $H$}
551
performs the simplification in the assumption $H$.
553
\item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] in $H$}
554
performs the simplification in the assumption $H$ using
556
defined by \term$_1$ {\ldots} \term$_n$.
558
\item {\tt field\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
560
performs the simplification in the terms $t_1$ \ldots $t_n$
561
of the assumption $H$ using
563
defined by \term$_1$ {\ldots} \term$_m$.
565
\item {\tt field\_simplify\_eq}
566
performs the simplification in the conclusion of the goal removing
567
the denominator. $F_1 = F_2$
568
becomes $N_1 D_2 = N_2 D_1$.
570
\item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$]}
571
performs the simplification in the conclusion of the goal using
573
defined by \term$_1$ {\ldots} \term$_n$.
575
\item {\tt field\_simplify\_eq} in $H$
576
performs the simplification in the assumption $H$.
578
\item {\tt field\_simplify\_eq [\term$_1$ {\ldots} \term$_n$] in $H$}
579
performs the simplification in the assumption $H$ using
581
defined by \term$_1$ {\ldots} \term$_n$.
584
\asection{Adding a new field structure
585
\comindex{Add Field}}
587
Declaring a new field consists in proving that a field signature (a
588
carrier set, an equality, and field operations: {\tt
589
Field\_theory.field\_theory} and {\tt Field\_theory.semi\_field\_theory})
590
satisfies the field axioms. Semi-fields (fields without $+$ inverse) are
591
also supported. The equality can be either Leibniz equality, or any
592
relation declared as a setoid (see~\ref{setoidtactics}). The definition
593
of fields and semi-fields is:
595
Record field_theory : Prop := mk_field {
596
F_R : ring_theory rO rI radd rmul rsub ropp req;
597
F_1_neq_0 : ~ 1 == 0;
598
Fdiv_def : forall p q, p / q == p * / q;
599
Finv_l : forall p, ~ p == 0 -> / p * p == 1
602
Record semi_field_theory : Prop := mk_sfield {
603
SF_SR : semi_ring_theory rO rI radd rmul req;
604
SF_1_neq_0 : ~ 1 == 0;
605
SFdiv_def : forall p q, p / q == p * / q;
606
SFinv_l : forall p, ~ p == 0 -> / p * p == 1
610
The result of the normalization process is a fraction represented by
613
Record linear : Type := mk_linear {
616
condition : list (PExpr C) }.
618
where {\tt num} and {\tt denum} are the numerator and denominator;
619
{\tt condition} is a list of expressions that have appeared as a
620
denominator during the normalization process. These expressions must
621
be proven different from zero for the correctness of the algorithm.
623
The syntax for adding a new field is {\tt Add Field $name$ : $field$
624
($mod_1$,\dots,$mod_2$)}. The name is not relevent. It is just used
625
for error messages. $field$ is a proof that the field signature
626
satisfies the (semi-)field axioms. The optional list of modifiers is
627
used to tailor the behaviour of the tactic. Since field tactics are
628
built upon ring tactics, all mofifiers of the {\tt Add Ring}
629
apply. There is only one specific modifier:
631
\item[completeness \term] allows the field tactic to prove
632
automatically that the image of non-zero coefficients are mapped to
633
non-zero elements of the field. \term is a proof of {\tt forall x y,
634
[x] == [y] -> x?=!y = true}, which is the completeness of equality
635
on coefficients w.r.t. the field equality.
638
\asection{Legacy implementation}
640
\Warning This tactic is the {\tt ring} tactic of previous versions of
641
\Coq{} and it should be considered as deprecated. It will probably be
642
removed in future releases. It has been kept only for compatibility
643
reasons and in order to help moving existing code to the newer
644
implementation described above. For more details, please refer to the
645
Coq Reference Manual, version 8.0.
648
\subsection{\tt legacy ring \term$_1$ \dots\ \term$_n$
649
\tacindex{legacy ring}
650
\comindex{Add Legacy Ring}
651
\comindex{Add Legacy Semi Ring}}
653
This tactic, written by Samuel Boutin and Patrick Loiseleur, applies
654
associative commutative rewriting on every ring. The tactic must be
655
loaded by \texttt{Require Import LegacyRing}. The ring must be declared in
656
the \texttt{Add Ring} command. The ring of booleans
657
is predefined; if one wants to use the tactic on \texttt{nat} one must
658
first require the module \texttt{LegacyArithRing}; for \texttt{Z}, do
659
\texttt{Require Import LegacyZArithRing}; for \texttt{N}, do \texttt{Require
660
Import LegacyNArithRing}.
662
The terms \term$_1$, \dots, \term$_n$ must be subterms of the goal
663
conclusion. The tactic \texttt{ring} normalizes these terms
664
w.r.t. associativity and commutativity and replace them by their
668
\item \texttt{legacy ring} When the goal is an equality $t_1=t_2$, it
669
acts like \texttt{ring\_simplify} $t_1$ $t_2$ and then
670
solves the equality by reflexivity.
672
\item \texttt{ring\_nat} is a tactic macro for \texttt{repeat rewrite
673
S\_to\_plus\_one; ring}. The theorem \texttt{S\_to\_plus\_one} is a
674
proof that \texttt{forall (n:nat), S n = plus (S O) n}.
678
You can have a look at the files \texttt{LegacyRing.v},
679
\texttt{ArithRing.v}, \texttt{ZArithRing.v} to see examples of the
680
\texttt{Add Ring} command.
682
\subsection{Add a ring structure}
684
It can be done in the \Coq toplevel (No ML file to edit and to link
685
with \Coq). First, \texttt{ring} can handle two kinds of structure:
686
rings and semi-rings. Semi-rings are like rings without an opposite to
687
addition. Their precise specification (in \gallina) can be found in
692
contrib/ring/Ring_theory.v
696
The typical example of ring is \texttt{Z}, the typical
697
example of semi-ring is \texttt{nat}.
699
The specification of a
700
ring is divided in two parts: first the record of constants
701
($\oplus$, $\otimes$, 1, 0, $\ominus$) and then the theorems
702
(associativity, commutativity, etc.).
707
Section Theory_of_semi_rings.
710
Variable Aplus : A -> A -> A.
711
Variable Amult : A -> A -> A.
714
(* There is also a "weakly decidable" equality on A. That means
715
that if (A_eq x y)=true then x=y but x=y can arise when
716
(A_eq x y)=false. On an abstract ring the function [x,y:A]false
717
is a good choice. The proof of A_eq_prop is in this case easy. *)
718
Variable Aeq : A -> A -> bool.
720
Record Semi_Ring_Theory : Prop :=
721
{ SR_plus_sym : (n,m:A)[| n + m == m + n |];
722
SR_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
724
SR_mult_sym : (n,m:A)[| n*m == m*n |];
725
SR_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
726
SR_plus_zero_left :(n:A)[| 0 + n == n|];
727
SR_mult_one_left : (n:A)[| 1*n == n |];
728
SR_mult_zero_left : (n:A)[| 0*n == 0 |];
729
SR_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
730
SR_plus_reg_left : (n,m,p:A)[| n + m == n + p |] -> m==p;
731
SR_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
740
Section Theory_of_rings.
744
Variable Aplus : A -> A -> A.
745
Variable Amult : A -> A -> A.
748
Variable Aopp : A -> A.
749
Variable Aeq : A -> A -> bool.
752
Record Ring_Theory : Prop :=
753
{ Th_plus_sym : (n,m:A)[| n + m == m + n |];
754
Th_plus_assoc : (n,m,p:A)[| n + (m + p) == (n + m) + p |];
755
Th_mult_sym : (n,m:A)[| n*m == m*n |];
756
Th_mult_assoc : (n,m,p:A)[| n*(m*p) == (n*m)*p |];
757
Th_plus_zero_left :(n:A)[| 0 + n == n|];
758
Th_mult_one_left : (n:A)[| 1*n == n |];
759
Th_opp_def : (n:A) [| n + (-n) == 0 |];
760
Th_distr_left : (n,m,p:A) [| (n + m)*p == n*p + m*p |];
761
Th_eq_prop : (x,y:A) (Is_true (Aeq x y)) -> x==y
767
To define a ring structure on A, you must provide an addition, a
768
multiplication, an opposite function and two unities 0 and 1.
770
You must then prove all theorems that make
771
(A,Aplus,Amult,Aone,Azero,Aeq)
772
a ring structure, and pack them with the \verb|Build_Ring_Theory|
775
Finally to register a ring the syntax is:
777
\comindex{Add Legacy Ring}
779
\texttt{Add Legacy Ring} \textit{A Aplus Amult Aone Azero Ainv Aeq T}
780
\texttt{[} \textit{c1 \dots cn} \texttt{].}
783
\noindent where \textit{A} is a term of type \texttt{Set},
784
\textit{Aplus} is a term of type \texttt{A->A->A},
785
\textit{Amult} is a term of type \texttt{A->A->A},
786
\textit{Aone} is a term of type \texttt{A},
787
\textit{Azero} is a term of type \texttt{A},
788
\textit{Ainv} is a term of type \texttt{A->A},
789
\textit{Aeq} is a term of type \texttt{A->bool},
790
\textit{T} is a term of type
791
\texttt{(Ring\_Theory }\textit{A Aplus Amult Aone Azero Ainv
793
The arguments \textit{c1 \dots cn},
794
are the names of constructors which define closed terms: a
795
subterm will be considered as a constant if it is either one of the
796
terms \textit{c1 \dots cn} or the application of one of these terms to
797
closed terms. For \texttt{nat}, the given constructors are \texttt{S}
798
and \texttt{O}, and the closed terms are \texttt{O}, \texttt{(S O)},
799
\texttt{(S (S O))}, \ldots
802
\item \texttt{Add Legacy Semi Ring} \textit{A Aplus Amult Aone Azero Aeq T}
803
\texttt{[} \textit{c1 \dots\ cn} \texttt{].}\comindex{Add Legacy Semi
806
There are two differences with the \texttt{Add Ring} command: there
807
is no inverse function and the term $T$ must be of type
808
\texttt{(Semi\_Ring\_Theory }\textit{A Aplus Amult Aone Azero
811
\item \texttt{Add Legacy Abstract Ring} \textit{A Aplus Amult Aone Azero Ainv
812
Aeq T}\texttt{.}\comindex{Add Legacy Abstract Ring}
814
This command should be used for when the operations of rings are not
815
computable; for example the real numbers of
816
\texttt{theories/REALS/}. Here $0+1$ is not beta-reduced to $1$ but
817
you still may want to \textit{rewrite} it to $1$ using the ring
818
axioms. The argument \texttt{Aeq} is not used; a good choice for
819
that function is \verb+[x:A]false+.
821
\item \texttt{Add Legacy Abstract Semi Ring} \textit{A Aplus Amult Aone Azero
822
Aeq T}\texttt{.}\comindex{Add Legacy Abstract Semi Ring}
827
\item \errindex{Not a valid (semi)ring theory}.
829
That happens when the typing condition does not hold.
832
Currently, the hypothesis is made than no more than one ring structure
833
may be declared for a given type in \texttt{Set} or \texttt{Type}.
834
This allows automatic detection of the theory used to achieve the
835
normalization. On popular demand, we can change that and allow several
836
ring structures on the same set.
838
The table of ring theories is compatible with the \Coq\
839
sectioning mechanism. If you declare a ring inside a section, the
840
declaration will be thrown away when closing the section.
841
And when you load a compiled file, all the \texttt{Add Ring}
842
commands of this file that are not inside a section will be loaded.
844
The typical example of ring is \texttt{Z}, and the typical example of
845
semi-ring is \texttt{nat}. Another ring structure is defined on the
848
\Warning Only the ring of booleans is loaded by default with the
849
\texttt{Ring} module. To load the ring structure for \texttt{nat},
850
load the module \texttt{ArithRing}, and for \texttt{Z},
851
load the module \texttt{ZArithRing}.
853
\subsection{\tt legacy field
854
\tacindex{legacy field}}
856
This tactic written by David~Delahaye and Micaela~Mayero solves equalities
857
using commutative field theory. Denominators have to be non equal to zero and,
858
as this is not decidable in general, this tactic may generate side conditions
859
requiring some expressions to be non equal to zero. This tactic must be loaded
860
by {\tt Require Import LegacyField}. Field theories are declared (as for
861
{\tt legacy ring}) with
862
the {\tt Add Legacy Field} command.
864
\subsection{\tt Add Legacy Field
865
\comindex{Add Legacy Field}}
867
This vernacular command adds a commutative field theory to the database for the
868
tactic {\tt field}. You must provide this theory as follows:
870
{\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero} {\it
871
Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}
873
where {\tt {\it A}} is a term of type {\tt Type}, {\tt {\it Aplus}} is
874
a term of type {\tt A->A->A}, {\tt {\it Amult}} is a term of type {\tt
875
A->A->A}, {\tt {\it Aone}} is a term of type {\tt A}, {\tt {\it
876
Azero}} is a term of type {\tt A}, {\tt {\it Aopp}} is a term of
877
type {\tt A->A}, {\tt {\it Aeq}} is a term of type {\tt A->bool}, {\tt
878
{\it Ainv}} is a term of type {\tt A->A}, {\tt {\it Rth}} is a term
879
of type {\tt (Ring\_Theory {\it A Aplus Amult Aone Azero Ainv Aeq})},
880
and {\tt {\it Tinvl}} is a term of type {\tt forall n:{\it A},
881
{\~{}}(n={\it Azero})->({\it Amult} ({\it Ainv} n) n)={\it Aone}}.
882
To build a ring theory, refer to Chapter~\ref{ring} for more details.
884
This command adds also an entry in the ring theory table if this theory is not
885
already declared. So, it is useless to keep, for a given type, the {\tt Add
886
Ring} command if you declare a theory with {\tt Add Field}, except if you plan
887
to use specific features of {\tt ring} (see Chapter~\ref{ring}). However, the
888
module {\tt ring} is not loaded by {\tt Add Field} and you have to make a {\tt
889
Require Import Ring} if you want to call the {\tt ring} tactic.
893
\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
894
{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
895
{\tt \phantom{Add Field }with minus:={\it Aminus}}
897
Adds also the term {\it Aminus} which must be a constant expressed by
900
\item {\tt Add Legacy Field {\it A} {\it Aplus} {\it Amult} {\it Aone} {\it Azero}
901
{\it Aopp} {\it Aeq} {\it Ainv} {\it Rth} {\it Tinvl}}\\
902
{\tt \phantom{Add Legacy Field }with div:={\it Adiv}}
904
Adds also the term {\it Adiv} which must be a constant expressed by
909
\SeeAlso \cite{DelMay01} for more details regarding the implementation of {\tt
912
\asection{History of \texttt{ring}}
914
First Samuel Boutin designed the tactic \texttt{ACDSimpl}.
915
This tactic did lot of rewriting. But the proofs
916
terms generated by rewriting were too big for \Coq's type-checker.
920
Require Import ZArith.
924
Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
927
intros; rewrite (Zmult_comm y z); reflexivity.
934
At each step of rewriting, the whole context is duplicated in the proof
935
term. Then, a tactic that does hundreds of rewriting generates huge proof
936
terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it
937
using reflection (see his article in TACS'97 \cite{Bou97}). Later, the
938
stuff was rewritten by Patrick
939
Loiseleur: the new tactic does not any more require \texttt{ACDSimpl}
940
to compile and it makes use of $\beta\delta\iota$-reduction
941
not only to replace the rewriting steps, but also to achieve the
942
interleaving of computation and
943
reasoning (see \ref{DiscussReflection}). He also wrote a
944
few ML code for the \texttt{Add Ring} command, that allow to register
945
new rings dynamically.
947
Proofs terms generated by \texttt{ring} are quite small, they are
948
linear in the number of $\oplus$ and $\otimes$ operations in the
949
normalized terms. Type-checking those terms requires some time because it
950
makes a large use of the conversion rule, but
951
memory requirements are much smaller.
953
\asection{Discussion}
954
\label{DiscussReflection}
956
Efficiency is not the only motivation to use reflection
957
here. \texttt{ring} also deals with constants, it rewrites for example the
958
expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the
959
tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the
960
expression $34 + 2*(x - 1) + 12$ is interpreted as
961
$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$,
962
with the variables mapping
963
$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is
964
rewritten to $34 - x + 2*x + 12$, very far from the expected
965
result. Here rewriting is not sufficient: you have to do some kind of
966
reduction (some kind of \textit{computation}) to achieve the
969
The tactic \texttt{ring} is not only faster than a classical one:
970
using reflection, we get for free integration of computation and
971
reasoning that would be very complex to implement in the classic fashion.
973
Is it the ultimate way to write tactics? The answer is: yes and
974
no. The \texttt{ring} tactic uses intensively the conversion rule of
975
\CIC, that is replaces proof by computation the most as it is
976
possible. It can be useful in all situations where a classical tactic
977
generates huge proof terms. Symbolic Processing and Tautologies are in
978
that case. But there are also tactics like \texttt{auto} or
979
\texttt{linear} that do many complex computations, using side-effects
980
and backtracking, and generate a small proof term. Clearly, it would
981
be significantly less efficient to replace them by tactics using
984
Another idea suggested by Benjamin Werner: reflection could be used to
985
couple an external tool (a rewriting program or a model checker) with
986
\Coq. We define (in \Coq) a type of terms, a type of \emph{traces},
987
and prove a correction theorem that states that \emph{replaying
988
traces} is safe w.r.t some interpretation. Then we let the external
989
tool do every computation (using side-effects, backtracking,
990
exception, or others features that are not available in pure lambda
991
calculus) to produce the trace: now we can check in Coq{} that the
992
trace has the expected semantic by applying the correction lemma.
996
%%% TeX-master: "Reference-Manual"
added
removed
refman/Polynom.tex
