aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/Polynom.tex
blob: 0664bf9095b6ca0029d1bdc6f4480c0fa7114a24 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
\achapter{The \texttt{ring} and \texttt{field} tactic families}
\aauthor{Bruno Barras, Benjamin Gr\'egoire, Assia
  Mahboubi, Laurent Th\'ery\footnote{based on previous work from
  Patrick Loiseleur and Samuel Boutin}}
\label{ring}
\tacindex{ring}

This chapter presents the tactics dedicated to deal with ring and
field equations.

\asection{What does this tactic do?}

\texttt{ring} does associative-commutative rewriting in ring and semi-ring
structures. Assume you have two binary functions $\oplus$ and $\otimes$
that are associative and commutative, with $\oplus$ distributive on
$\otimes$, and two constants 0 and 1 that are unities for $\oplus$ and
$\otimes$. A \textit{polynomial} is an expression built on variables $V_0, V_1,
\dots$ and constants by application of $\oplus$ and $\otimes$.

Let an {\it ordered product} be a product of variables $V_{i_1}
\otimes \ldots \otimes V_{i_n}$ verifying $i_1 \le i_2 \le \dots \le
i_n$. Let a \textit{monomial} be the product of a constant and an
ordered product.  We can order the monomials by the lexicographic
order on products of variables. Let a \textit{canonical sum} be an
ordered sum of monomials that are all different, i.e. each monomial in
the sum is strictly less than the following monomial according to the
lexicographic order. It is an easy theorem to show that every
polynomial is equivalent (modulo the ring properties) to exactly one
canonical sum. This canonical sum is called the \textit{normal form}
of the polynomial. In fact, the actual representation shares monomials
with same prefixes. So what does \texttt{ring}? It normalizes
polynomials over any ring or semi-ring structure. The basic use of
\texttt{ring} is to simplify ring expressions, so that the user does
not have to deal manually with the theorems of associativity and
commutativity.

\begin{Examples}
\item In the ring of integers, the normal form of 
$x (3 + yx + 25(1 - z)) + zx$ is $28x + (-24)xz + xxy$.
\end{Examples}

\texttt{ring} is also able to compute a normal form modulo monomial 
equalities. For example, under the hypothesis that $2x^2 = yz+1$,
 the normal form of $2(x + 1)x - x - zy$ is $x+1$.

\asection{The variables map}

It is frequent to have an expression built with + and
  $\times$, but rarely on variables only.
Let us associate a number to each subterm of a ring
expression in the \gallina\ language. For example in the ring
\texttt{nat}, consider the expression:

\begin{quotation}
\begin{verbatim}
(plus (mult (plus (f (5)) x) x)
      (mult (if b then (4) else (f (3))) (2)))
\end{verbatim}
\end{quotation}

\noindent As a ring expression, it has 3 subterms. Give each subterm a
number in an arbitrary order:

\begin{tabular}{ccl}
0 & $\mapsto$ & \verb|if b then (4) else (f (3))| \\
1 & $\mapsto$ & \verb|(f (5))| \\
2 & $\mapsto$ & \verb|x| \\
\end{tabular}

\noindent Then normalize the ``abstract'' polynomial 

$$((V_1 \otimes V_2) \oplus V_2) \oplus (V_0 \otimes 2) $$

\noindent In our example the normal form is:

$$(2 \otimes V_0) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2)$$

\noindent Then substitute the variables by their values in the variables map to
get the concrete normal polynomial:

\begin{quotation}
\begin{verbatim}
(plus (mult (2) (if b then (4) else (f (3)))) 
      (plus (mult (f (5)) x) (mult x x))) 
\end{verbatim}
\end{quotation}

\asection{Is it automatic?}

Yes, building the variables map and doing the substitution after
normalizing is automatically done by the tactic. So you can just forget
this paragraph and use the tactic according to your intuition.

\asection{Concrete usage in \Coq
\tacindex{ring}
\tacindex{ring\_simplify}}

The {\tt ring} tactic solves equations upon polynomial expressions of
a ring (or semi-ring) structure. It proceeds by normalizing both hand
sides of the equation (w.r.t. associativity, commutativity and
distributivity, constant propagation, rewriting of monomials) 
and comparing syntactically the results.

{\tt ring\_simplify} applies the normalization procedure described
above to the terms given. The tactic then replaces all occurrences of
the terms given in the conclusion of the goal by their normal
forms. If no term is given, then the conclusion should be an equation
and both hand sides are normalized. 
The tactic can also be applied in a hypothesis.

The tactic must be loaded by \texttt{Require Import Ring}. The ring
structures must be declared with the \texttt{Add Ring} command (see
below). The ring of booleans is predefined; if one wants to use the
tactic on \texttt{nat} one must first require the module
\texttt{ArithRing} (exported by \texttt{Arith});
for \texttt{Z}, do \texttt{Require Import
ZArithRing} or simply \texttt{Require Import ZArith}; 
for \texttt{N}, do \texttt{Require Import NArithRing} or 
\texttt{Require Import NArith}.

\Example
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example*}
Require Import ZArith.
\end{coq_example*}
\begin{coq_example}
Open Scope Z_scope.
Goal forall a b c:Z,
  (a + b + c)^2  =
  a * a + b^2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c.
\end{coq_example}
\begin{coq_example}
intros; ring.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}
\begin{coq_example}
Goal forall a b:Z, 2*a*b = 30 ->
        (a+b)^2 = a^2 + b^2 + 30.
\end{coq_example}
\begin{coq_example}
intros a b H; ring [H].
\end{coq_example} 
\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\begin{Variants}
  \item {\tt ring [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
    terms modulo ring operations and rewriting of the equalities
    defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
    {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
    where $m$ is a monomial (after ``abstraction''),
    $p$ a polynomial and $=$ the corresponding equality of the ring structure.

  \item {\tt ring\_simplify [\term$_1$ {\ldots} \term$_n$] $t_1 \ldots t_m$ in 
{\ident}}
     performs the simplification in the hypothesis named {\tt ident}.
\end{Variants}

\Warning \texttt{ring\_simplify \term$_1$; ring\_simplify \term$_2$} is
not equivalent to \texttt{ring\_simplify \term$_1$ \term$_2$}. In the
latter case the variables map is shared between the two terms, and
common subterm $t$ of \term$_1$ and \term$_2$ will have the same
associated variable number. So the first alternative should be
avoided for terms belonging to the same ring theory.


\begin{ErrMsgs}
\item \errindex{not a valid ring equation}
  The conclusion of the goal is not provable in the corresponding ring
  theory.
\item \errindex{arguments of ring\_simplify do not have all the same type}
  {\tt ring\_simplify} cannot simplify terms of several rings at the
  same time. Invoke the tactic once per ring structure.
\item \errindex{cannot find a declared ring structure over {\tt term}}
  No ring has been declared for the type of the terms to be
  simplified. Use {\tt Add Ring} first.
\item \errindex{cannot find a declared ring structure for equality
  {\tt term}}
  Same as above is the case of the {\tt ring} tactic.
\end{ErrMsgs}

\asection{Adding a ring structure
\comindex{Add Ring}}

Declaring a new ring consists in proving that a ring signature (a
carrier set, an equality, and ring operations: {\tt
Ring\_theory.ring\_theory} and {\tt Ring\_theory.semi\_ring\_theory})
satisfies the ring axioms. Semi-rings (rings without $+$ inverse) are
also supported. The equality can be either Leibniz equality, or any
relation declared as a setoid (see~\ref{setoidtactics}). The definition
of ring and semi-rings (see module {\tt Ring\_theory}) is:
\begin{verbatim}
Record ring_theory : Prop := mk_rt {
  Radd_0_l    : forall x, 0 + x == x;
  Radd_sym    : forall x y, x + y == y + x;
  Radd_assoc  : forall x y z, x + (y + z) == (x + y) + z;
  Rmul_1_l    : forall x, 1 * x == x;
  Rmul_sym    : forall x y, x * y == y * x;
  Rmul_assoc  : forall x y z, x * (y * z) == (x * y) * z;
  Rdistr_l    : forall x y z, (x + y) * z == (x * z) + (y * z);
  Rsub_def    : forall x y, x - y == x + -y;
  Ropp_def    : forall x, x + (- x) == 0
}.

Record semi_ring_theory : Prop := mk_srt {
  SRadd_0_l   : forall n, 0 + n == n;
  SRadd_sym   : forall n m, n + m == m + n ;
  SRadd_assoc : forall n m p, n + (m + p) == (n + m) + p;
  SRmul_1_l   : forall n, 1*n == n;
  SRmul_0_l   : forall n, 0*n == 0;
  SRmul_sym   : forall n m, n*m == m*n;
  SRmul_assoc : forall n m p, n*(m*p) == (n*m)*p;
  SRdistr_l   : forall n m p, (n + m)*p == n*p + m*p
}.
\end{verbatim}

This implementation of {\tt ring} also features a notion of constant
that can be parameterized. This can be used to improve the handling of
closed expressions when operations are effective. It consists in
introducing a type of \emph{coefficients} and an implementation of the
ring operations, and a morphism from the coefficient type to the ring
carrier type. The morphism needs not be injective, nor surjective.  

As
an example, one can consider the real numbers. The set of coefficients
could be the rational numbers, upon which the ring operations can be
implemented. The fact that there exists a morphism is defined by the
following properties:
\begin{verbatim}
Record ring_morph : Prop := mkmorph {
  morph0    : [cO] == 0;
  morph1    : [cI] == 1;
  morph_add : forall x y, [x +! y] == [x]+[y];
  morph_sub : forall x y, [x -! y] == [x]-[y];
  morph_mul : forall x y, [x *! y] == [x]*[y];
  morph_opp : forall x, [-!x] == -[x];
  morph_eq  : forall x y, x?=!y = true -> [x] == [y]
}.

Record semi_morph : Prop := mkRmorph {
  Smorph0 : [cO] == 0;
  Smorph1 : [cI] == 1;
  Smorph_add : forall x y, [x +! y] == [x]+[y];
  Smorph_mul : forall x y, [x *! y] == [x]*[y];
  Smorph_eq  : forall x y, x?=!y = true -> [x] == [y]
}.
\end{verbatim}
where {\tt c0} and {\tt cI} denote the 0 and 1 of the coefficient set,
{\tt +!}, {\tt *!}, {\tt -!} are the implementations of the ring
operations, {\tt ==} is the equality of the coefficients, {\tt ?+!} is
an implementation of this equality, and {\tt [x]} is a notation for
the image of {\tt x} by the ring morphism.



Since {\tt Z} is an initial ring (and {\tt N} is an initial
semi-ring), it can always be considered as a set of
coefficients. There are basically three kinds of (semi-)rings:
\begin{description}
\item[abstract rings] to be used when operations are not
  effective. The set of coefficients is {\tt Z} (or {\tt N} for
  semi-rings).
\item[computational rings] to be used when operations are
  effective. The set of coefficients is the ring itself. The user only
  has to provide an implementation for the equality.
\item[customized ring] for other cases. The user has to provide the
  coefficient set and the morphism.
\end{description}

This implementation of ring can also recognize simple 
power expressions as ring expressions. A power function is specified by 
the following property:
\begin{verbatim}
Section POWER.
  Variable Cpow : Set.
  Variable Cp_phi : N -> Cpow.
  Variable rpow : R -> Cpow -> R.

  Record power_theory : Prop := mkpow_th {
    rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n)
  }.

End POWER.
\end{verbatim}


The syntax for adding a new ring is {\tt Add Ring $name$ : $ring$
($mod_1$,\dots,$mod_2$)}.  The name is not relevant. It is just used
for error messages. The term $ring$ is a proof that the ring signature
satisfies the (semi-)ring axioms. The optional list of modifiers is
used to tailor the behavior of the tactic. The following list
describes their syntax and effects:
\begin{description}
\item[abstract] declares the ring as abstract. This is the default.
\item[decidable \term] declares the ring as computational. The expression 
  \term{} is
  the correctness proof of an equality test {\tt ?=!} (which should be
  evaluable). Its type should be of
  the form {\tt forall x y, x?=!y = true $\rightarrow$ x == y}.
\item[morphism \term] declares the ring as a customized one. The expression 
  \term{} is
  a proof that there exists a morphism between a set of coefficient
  and the ring carrier (see {\tt Ring\_theory.ring\_morph} and {\tt
  Ring\_theory.semi\_morph}).
\item[setoid \term$_1$ \term$_2$] forces the use of given setoid. The 
  expression \term$_1$ is a proof that the equality is indeed a setoid
  (see {\tt Setoid.Setoid\_Theory}), and \term$_2$ a proof that the
  ring operations are morphisms (see {\tt Ring\_theory.ring\_eq\_ext} and
  {\tt Ring\_theory.sring\_eq\_ext}). This modifier needs not be used if the
  setoid and morphisms have been declared.
\item[constants [\ltac]] specifies a tactic expression that, given a term,
  returns either an object of the coefficient set that is mapped to
  the expression via the morphism, or returns {\tt
  InitialRing.NotConstant}. The default behavior is to map only 0 and
  1 to their counterpart in the coefficient set. This is generally not
  desirable for non trivial computational rings.
\item[preprocess [\ltac]]
  specifies a tactic that is applied as a preliminary step for {\tt
  ring} and {\tt ring\_simplify}. It can be used to transform a goal
  so that it is better recognized. For instance, {\tt S n} can be
  changed to {\tt plus 1 n}.
\item[postprocess [\ltac]] specifies a tactic that is applied as a final step
  for {\tt ring\_simplify}. For instance, it can be used to undo
  modifications of the preprocessor.
\item[power\_tac {\term} [\ltac]] allows {\tt ring} and {\tt ring\_simplify} to
  recognize power expressions with a constant positive integer exponent 
  (example: $x^2$). The term {\term} is a proof that a given power function
  satisfies the specification of a power function ({\term} has to be a
  proof of {\tt Ring\_theory.power\_theory}) and {\ltac} specifies a
  tactic expression that, given a term, ``abstracts'' it into an
  object of type {\tt N} whose interpretation via {\tt Cp\_phi} (the
  evaluation function of power coefficient) is the original term, or
  returns {\tt InitialRing.NotConstant} if not a constant coefficient
  (i.e. {\ltac} is the inverse function of {\tt Cp\_phi}).
  See files {\tt plugins/setoid\_ring/ZArithRing.v} and
  {\tt plugins/setoid\_ring/RealField.v} for examples.
  By default the tactic does not recognize power expressions as ring
  expressions.
\item[sign {\term}] allows {\tt ring\_simplify} to use a minus operation
  when outputing its normal form, i.e writing $x - y$ instead of $x + (-y)$. 
  The term {\term} is a proof that a given sign function indicates expressions
   that are signed ({\term} has to be a
  proof of {\tt Ring\_theory.get\_sign}). See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of sign function.
\item[div {\term}] allows  {\tt ring} and {\tt ring\_simplify} to use moniomals
with coefficient other than 1 in the rewriting. The term {\term} is a proof that a given division function  satisfies the specification of an euclidean
  division function  ({\term} has to be a
  proof of {\tt Ring\_theory.div\_theory}). For example, this function is
  called when trying to rewrite $7x$ by $2x = z$ to tell that $7 = 3 * 2 + 1$.
   See  {\tt plugins/setoid\_ring/IntialRing.v} for examples of div function.
  
\end{description}


\begin{ErrMsgs}
\item \errindex{bad ring structure}
  The proof of the ring structure provided is not of the expected type.
\item \errindex{bad lemma for decidability of equality}
  The equality function provided in the case of a computational ring
  has not the expected type.
\item \errindex{ring {\it operation} should be declared as a morphism}
  A setoid associated to the carrier of the ring structure as been
  found, but the ring operation should be declared as
  morphism. See~\ref{setoidtactics}.
\end{ErrMsgs}

\asection{How does it work?}

The code of \texttt{ring} is a good example of tactic written using
\textit{reflection}.  What is reflection? Basically, it is writing
\Coq{} tactics in \Coq, rather than in \ocaml. From the philosophical
point of view, it is using the ability of the Calculus of
Constructions to speak and reason about itself.  For the \texttt{ring}
tactic we used \Coq\ as a programming language and also as a proof
environment to build a tactic and to prove it correctness.

The interested reader is strongly advised to have a look at the file
\texttt{Ring\_polynom.v}. Here a type for polynomials is defined: 

\begin{small}
\begin{flushleft}
\begin{verbatim}
Inductive PExpr : Type :=
  | PEc : C -> PExpr
  | PEX : positive -> PExpr
  | PEadd : PExpr -> PExpr -> PExpr
  | PEsub : PExpr -> PExpr -> PExpr
  | PEmul : PExpr -> PExpr -> PExpr
  | PEopp : PExpr -> PExpr
  | PEpow : PExpr -> N -> PExpr.
\end{verbatim}
\end{flushleft}
\end{small}

Polynomials in normal form are defined as:
\begin{small}
\begin{flushleft}
\begin{verbatim}
Inductive Pol : Type :=
  | Pc : C -> Pol 
  | Pinj : positive -> Pol -> Pol                   
  | PX : Pol -> positive -> Pol -> Pol.
\end{verbatim}
\end{flushleft}
\end{small}
where {\tt Pinj n P} denotes $P$ in which $V_i$ is replaced by
$V_{i+n}$, and {\tt PX P n Q} denotes $P \otimes V_1^{n} \oplus Q'$,
$Q'$ being $Q$ where $V_i$ is replaced by $V_{i+1}$. 


Variables maps are represented by list of ring elements, and two
interpretation functions, one that maps a variables map and a
polynomial to an element of the concrete ring, and the second one that
does the same for normal forms:
\begin{small}
\begin{flushleft}
\begin{verbatim}
Definition PEeval : list R -> PExpr -> R := [...].
Definition Pphi_dev : list R -> Pol -> R := [...].
\end{verbatim}
\end{flushleft}
\end{small}

A function to normalize polynomials is defined, and the big theorem is
its correctness w.r.t interpretation, that is:

\begin{small}
\begin{flushleft}
\begin{verbatim}
Definition norm : PExpr -> Pol := [...].
Lemma Pphi_dev_ok :
   forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
\end{verbatim}
\end{flushleft}
\end{small}

So now, what is the scheme for a normalization proof? Let \texttt{p}
be the polynomial expression that the user wants to normalize. First a
little piece of ML code guesses the type of \texttt{p}, the ring
theory \texttt{T} to use, an abstract polynomial \texttt{ap} and a
variables map \texttt{v} such that \texttt{p} is
$\beta\delta\iota$-equivalent to \verb|(PEeval v ap)|. Then we
replace it by \verb|(Pphi_dev v (norm ap))|, using the
main correctness theorem and we reduce it to a concrete expression
\texttt{p'}, which is the concrete normal form of
\texttt{p}. This is summarized in this diagram:
\begin{center}
\begin{tabular}{rcl}
\texttt{p} & $\rightarrow_{\beta\delta\iota}$  
   & \texttt{(PEeval v ap)} \\
 & & $=_{\mathrm{(by\ the\ main\ correctness\ theorem)}}$ \\
\texttt{p'} 
   & $\leftarrow_{\beta\delta\iota}$ 
   & \texttt{(Pphi\_dev v (norm ap))}
\end{tabular}
\end{center}
The user do not see the right part of the diagram. 
From outside, the tactic behaves like a
$\beta\delta\iota$ simplification extended with AC rewriting rules.
Basically, the proof is only the application of the main
correctness theorem to well-chosen arguments.


\asection{Dealing with fields
\tacindex{field}
\tacindex{field\_simplify}
\tacindex{field\_simplify\_eq}}


The {\tt field} tactic is  an extension of the {\tt ring} to deal with
rational expression. Given a rational expression $F=0$. It first reduces the
expression $F$ to a common denominator $N/D= 0$ where $N$ and $D$ are two ring
expressions.
For example, if we take $F = (1 - 1/x) x - x + 1$, this gives 
$ N= (x -1)  x - x^2 + x$ and $D= x$. It then calls {\tt ring} 
to solve $N=0$. Note that {\tt field} also generates non-zero conditions
for all the denominators it encounters in the reduction.
In our example, it generates the condition $x \neq 0$. These
conditions appear as one subgoal which is a conjunction if there are
several denominators.
Non-zero conditions are {\it always} polynomial expressions. For example 
when reducing the expression $1/(1 + 1/x)$, two side conditions are
generated: $x\neq 0$ and $x + 1 \neq 0$. Factorized expressions are
broken since a field is an integral domain, and when the equality test
on coefficients is complete w.r.t. the equality of the target field,
constants can be proven different from zero automatically.

The tactic must be loaded by \texttt{Require Import Field}. New field
structures can be declared to the system with the \texttt{Add Field}
command (see below). The field of real numbers is defined in module
\texttt{RealField} (in texttt{plugins/setoid\_ring}). It is exported
by module \texttt{Rbase}, so that requiring \texttt{Rbase} or
\texttt{Reals} is enough to use the field tactics on real
numbers. Rational numbers in canonical form are also declared as a
field in module \texttt{Qcanon}.


\Example
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example*}
Require Import Reals.
\end{coq_example*}
\begin{coq_example}
Open Scope R_scope.
Goal forall x,  x <> 0 ->
   (1 - 1/x) * x - x + 1 = 0.
\end{coq_example}
\begin{coq_example}
intros; field; auto.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}
\begin{coq_example}
Goal forall x y, y <> 0 -> y = x -> x/y = 1.
\end{coq_example}
\begin{coq_example}
intros x y H H1; field [H1]; auto.
\end{coq_example} 
\begin{coq_eval}
Reset Initial.
\end{coq_eval}

\begin{Variants}
  \item {\tt field [\term$_1$ {\ldots} \term$_n$]} decides the equality of two
    terms modulo field operations and rewriting of the equalities
    defined by \term$_1$ {\ldots} \term$_n$. Each of \term$_1$
    {\ldots} \term$_n$ has to be a proof of some equality $m = p$,
    where $m$ is a monomial (after ``abstraction''),
    $p$ a polynomial and $=$ the corresponding equality of the field structure.
    Beware that rewriting works with the equality $m=p$ only if $p$ is a 
    polynomial since rewriting is handled by the underlying {\tt ring}
    tactic.
  \item {\tt field\_simplify} 
     performs the simplification in the conclusion of the goal, $F_1 = F_2$
     becomes $N_1/D_1 = N_2/D_2$. A normalization step (the same as the
     one for rings) is then applied to $N_1$, $D_1$, $N_2$ and
     $D_2$. This way, polynomials remain in factorized form during the
     fraction simplifications. This yields smaller expressions when
     reducing to the same denominator since common factors can be
     canceled.

  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$]}
     performs the simplification in the conclusion of the goal using
    the equalities
    defined by \term$_1$ {\ldots} \term$_n$.

  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
$t_m$}
     performs the simplification in the terms $t_1$ \ldots $t_m$
    of the conclusion of the goal using
    the equalities
    defined by \term$_1$ {\ldots} \term$_n$. 

  \item {\tt field\_simplify in $H$}  
     performs the simplification in the assumption $H$.

  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] in $H$}
     performs the simplification in the assumption $H$ using
    the equalities
    defined by \term$_1$ {\ldots} \term$_n$. 

  \item {\tt field\_simplify   [\term$_1$ {\ldots} \term$_n$] $t_1$ \ldots
$t_m$ in $H$}
     performs the simplification in the terms $t_1$ \ldots $t_n$
    of the assumption $H$ using
    the equalities
    defined by \term$_1$ {\ldots} \term$_m$. 

  \item {\tt field\_simplify\_eq}
     performs the simplification in the conclusion of the goal removing
     the denominator. $F_1 = F_2$
     becomes $N_1 D_2 = N_2  D_1$.

  \item {\tt field\_simplify\_eq   [\term$_1$ {\ldots} \term$_n$]}
     performs the simplification in the conclusion of the goal using
    the equalities
    defined by \term$_1$ {\ldots} \term$_n$. 

  \item {\tt field\_simplify\_eq} in $H$
     performs the simplification in the assumption $H$.

  \item {\tt field\_simplify\_eq   [\term$_1$ {\ldots} \term$_n$] in $H$}
     performs the simplification in the assumption $H$ using
    the equalities
    defined by \term$_1$ {\ldots} \term$_n$. 
\end{Variants}

\asection{Adding a new field structure
\comindex{Add Field}}

Declaring a new field consists in proving that a field signature (a
carrier set, an equality, and field operations: {\tt
Field\_theory.field\_theory} and {\tt Field\_theory.semi\_field\_theory})
satisfies the field axioms. Semi-fields (fields without $+$ inverse) are
also supported. The equality can be either Leibniz equality, or any
relation declared as a setoid (see~\ref{setoidtactics}). The definition
of fields and semi-fields is:
\begin{verbatim}
Record field_theory : Prop := mk_field {
  F_R : ring_theory rO rI radd rmul rsub ropp req;
  F_1_neq_0 : ~ 1 == 0;
  Fdiv_def : forall p q, p / q == p * / q;
  Finv_l : forall p, ~ p == 0 ->  / p * p == 1
}.

Record semi_field_theory : Prop := mk_sfield {
  SF_SR : semi_ring_theory rO rI radd rmul req;
  SF_1_neq_0 : ~ 1 == 0;
  SFdiv_def : forall p q, p / q == p * / q;
  SFinv_l : forall p, ~ p == 0 ->  / p * p == 1
}.
\end{verbatim}

The result of the normalization process is a fraction represented by
the following type:
\begin{verbatim}
Record linear : Type := mk_linear {
  num : PExpr C;
  denum : PExpr C;
  condition : list (PExpr C)
}.
\end{verbatim}
where {\tt num} and {\tt denum} are the numerator and denominator;
{\tt condition} is a list of expressions that have appeared as a
denominator during the normalization process. These expressions must
be proven different from zero for the correctness of the algorithm.

The syntax for adding a new field is {\tt Add Field $name$ : $field$
($mod_1$,\dots,$mod_2$)}.  The name is not relevant. It is just used
for error messages. $field$ is a proof that the field signature
satisfies the (semi-)field axioms. The optional list of modifiers is
used to tailor the behavior of the tactic. Since field tactics are
built upon ring tactics, all modifiers of the {\tt Add Ring}
apply. There is only one specific modifier:
\begin{description}
\item[completeness \term] allows the field tactic to prove
  automatically that the image of non-zero coefficients are mapped to
  non-zero elements of the field. \term is a proof of {\tt forall x y,
    [x] == [y] -> x?=!y = true}, which is the completeness of equality
  on coefficients w.r.t. the field equality.
\end{description}

\asection{History of \texttt{ring}}

First Samuel Boutin designed the tactic \texttt{ACDSimpl}. 
This tactic did lot of rewriting. But the proofs
terms generated by rewriting were too big for \Coq's type-checker.
Let us see why:

\begin{coq_eval}
Require Import ZArith.
Open Scope Z_scope.
\end{coq_eval}
\begin{coq_example}
Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
\end{coq_example}
\begin{coq_example*}
intros; rewrite (Z.mul_comm y z); reflexivity.
Save toto.
\end{coq_example*}
\begin{coq_example}
Print toto.
\end{coq_example}

At each step of rewriting, the whole context is duplicated in the proof
term. Then, a tactic that does hundreds of rewriting generates huge proof
terms. Since \texttt{ACDSimpl} was too slow, Samuel Boutin rewrote it
using reflection (see his article in TACS'97 \cite{Bou97}). Later, the
stuff was rewritten by Patrick
Loiseleur: the new tactic does not any more require \texttt{ACDSimpl}
to compile and it makes use of $\beta\delta\iota$-reduction 
not only to replace the rewriting steps, but also to achieve the
interleaving of computation and 
reasoning (see \ref{DiscussReflection}). He also wrote a
few ML code for the \texttt{Add Ring} command, that allow to register
new rings dynamically.

Proofs terms generated by \texttt{ring} are quite small, they are
linear in the number of $\oplus$ and $\otimes$ operations in the
normalized terms. Type-checking those terms requires some time because it
makes a large use of the conversion rule, but
memory requirements are much smaller. 

\asection{Discussion}
\label{DiscussReflection}

Efficiency is not the only motivation to use reflection
here. \texttt{ring} also deals with constants, it rewrites for example the
expression $34 + 2*x -x + 12$ to the expected result $x + 46$. For the
tactic \texttt{ACDSimpl}, the only constants were 0 and 1. So the
expression $34 + 2*(x - 1) + 12$ is interpreted as 
$V_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3$, 
with the variables mapping 
$\{V_0 \mt 34; V_1 \mt 2; V_2 \mt x; V_3 \mt 12 \}$. Then it is
rewritten to $34 - x + 2*x + 12$, very far from the expected
result. Here rewriting is not sufficient: you have to do some kind of
reduction (some kind of \textit{computation}) to achieve the
normalization.

The tactic \texttt{ring} is not only faster than a classical one:
using reflection, we get for free integration of computation and
reasoning that would be very complex to implement in the classic fashion.

Is it the ultimate way to write tactics?  The answer is: yes and
no. The \texttt{ring} tactic uses intensively the conversion rule of
\CIC, that is replaces proof by computation the most as it is
possible. It can be useful in all situations where a classical tactic
generates huge proof terms. Symbolic Processing and Tautologies are in
that case. But there are also tactics like \texttt{auto} or
\texttt{linear} that do many complex computations, using side-effects
and backtracking, and generate a small proof term. Clearly, it would
be significantly less efficient to replace them by tactics using
reflection.

Another idea suggested by Benjamin Werner: reflection could be used to
couple an external tool (a rewriting program or a model checker) with
\Coq. We define (in \Coq) a type of terms, a type of \emph{traces},
and prove a correction theorem that states that \emph{replaying
traces} is safe w.r.t some interpretation. Then we let the external
tool do every computation (using side-effects, backtracking,
exception, or others features that are not available in pure lambda
calculus) to produce the trace: now we can check in Coq{} that the
trace has the expected semantic by applying the correction lemma.
 
%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: