Chapter 19 The `ring` tactic

Patrick Loiseleur and Samuel Boutin

This chapter presents the ring tactic.

19.1 What does this tactic?

ring does associative-commutative rewriting in ring and semi-ring structures. Assume you have two binary functions + and × that are associative and commutative, with + distributive on ×, and two constants 0 and 1 that are unities for + and ×. A polynomial is an expression built on variables V₀, V₁, ... and constants by application of + and ×.

Let an ordered product be a product of variables V_i₁ × ... × V_{i_n} verifying i₁ <= i₂ <= ... <= i_n. Let a monomial be the product of a constant (possibly equal to 1, in which case we omit it) and an ordered product. We can order the monomials by the lexicographic order on products of variables. Let a 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 normal form of the polynomial. So what does ring? It normalizes polynomials over any ring or semi-ring structure. The basic use of ring is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity.

Examples:

In the ring of integers, the normal form of x (3 + yx + 25(1 - z)) + zx is 28x + (-24)xz + xxy.
For the classical propositional calculus (or the boolean rings) the normal form is what logicians call disjunctive normal form: every formula is equivalent to a disjunction of conjunctions of atoms. (Here + is \/, × is /\, variables are atoms and the only constants are T and F)

19.2 The variables map

It is frequent to have an expression built with + and ×, 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 nat, consider the expression:

(plus (mult (plus (f (5)) x) x)
      (mult (if b then (4) else (f (3))) (2)))

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

0	\|->	`if b then (4) else (f (3))`
1	\|->	`(f (5))`
2	\|->	`x`

Then normalize the ``abstract'' polynomial

((V₁ × V₂) + V₂) + (V₀ × 2)

In our example the normal form is:

(2 × V₀) + (V₁ × V₂) + (V₂ × V₂)

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

(plus (mult (2) (if b then (4) else (f (3)))) 
      (plus (mult (f (5)) x) (mult x x)))

19.3 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.

19.4 Concrete usage in Coq

Under a session launched by coqtop or coqtop -full, load the ring files with the command:

Require Ring.

It does not work under coqtop -opt because the compiled ML objects used by the tactic are not linked in this binary image, and dynamic loading of native code is not possible in Objective Caml.

In order to use ring on naturals, load ArithRing instead; for binary integers, load the module ZArithRing.

Then, to normalize the terms term₁, ..., term_n in the current subgoal, use the tactic:

ring term₁ ... term_n

Then the tactic guesses the type of given terms, the ring theory to use, the variables map, and replace each term with its normal form. The variables map is common to all terms

Warning: ring term₁; ring term₂ is not equivalent to ring term₁ term₂. In the latter case the variables map is shared between the two terms, and common subterm t of term₁ and term₂ will have the same associated variable number.

Error messages:

All terms must have the same type
Don't know what to do with this goal
No Declared Ring Theory for term.

Use Add [Semi] Ring to declare it

That happens when all terms have the same type term, but there is no declared ring theory for this set. See below.

Variants:

ring

That works if the current goal is an equality between two polynomials. It will normalize both sides of the equality, solve it if the normal forms are equal and in other cases try to simplify the equality using congr_eqT and refl_equal to reduce x + y = x + z to y = z and x * z = x * y to y = z.

Error message: This goal is not an equality

19.5 Add a ring structure

It can be done in the Coqtoplevel (No ML file to edit and to link with Coq). First, 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

contrib/ring/Ring_theory.v

The typical example of ring is Z, the typical example of semi-ring is nat.

The specification of a ring is divided in two parts: first the record of constants (+, ×, 1, 0, -) and then the theorems (associativity, commutativity, etc.).

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
}.

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
}.

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 Build_Ring_Theory constructor.

Finally to register a ring the syntax is:

Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ...cn ].

where A is a term of type Set, Aplus is a term of type A->A->A, Amult is a term of type A->A->A, Aone is a term of type A, Azero is a term of type A, Ainv is a term of type A->A, Aeq is a term of type A->bool, T is a term of type (Ring_Theory A Aplus Amult Aone Azero Ainv Aeq). The arguments c1 ...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 c1 ...cn or the application of one of these terms to closed terms. For nat, the given constructors are S and O, and the closed terms are O, (S O), (S (S O)), ...

Variants:

Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].

There are two differences with the Add Ring command: there is no inverse function and the term T must be of type (Semi_Ring_Theory A Aplus Amult Aone Azero Aeq).
Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T.

This command should be used for when the operations of rings are not computable; for example the real numbers of theories/REALS/. Here 0+1 is not beta-reduced to 1 but you still may want to rewrite it to 1 using the ring axioms. The argument Aeq is not used; a good choice for that function is [x:A]false.
Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T.

Error messages:

Not a valid (semi)ring theory.

That happens when the typing condition does not hold.

Currently, the hypothesis is made than no more than one ring structure may be declared for a given type in Set or 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 Add Ring commands of this file that are not inside a section will be loaded.

The typical example of ring is Z, and the typical example of semi-ring is nat. Another ring structure is defined on the booleans.

Warning: Only the ring of booleans is loaded by default with the Ring module. To load the ring structure for nat, load the module ArithRing, and for Z, load the module ZArithRing.

19.6 How does it work?

The code of ring is a good example of tactic written using reflection (or internalization, it is synonymous). What is reflection? Basically, it is writing Coq tactics in Coq, rather than in Objective Caml. From the philosophical point of view, it is using the ability of the Calculus of Constructions to speak and reason about itself. For the 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 Ring_normalize.v. Here a type for polynomials is defined:

Inductive Type polynomial := 
  Pvar : idx -> polynomial
| Pconst : A -> polynomial
| Pplus : polynomial -> polynomial -> polynomial
| Pmult : polynomial -> polynomial -> polynomial
| Popp : polynomial -> polynomial.

There is also a type to represent variables maps, and an interpretation function, that maps a variables map and a polynomial to an element of the concrete ring:

Definition polynomial_simplify := [...]
Definition interp : (varmap A) -> (polynomial A) -> A := [...]

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

Theorem polynomial_simplify_correct : forall (v:(varmap A))(p:polynomial)
  (interp v (polynomial_simplify p))
  =(interp v p).

(The actual code is slightly more complex: for efficiency, there is a special datatype to represent normalized polynomials, i.e. ``canonical sums''. But the idea is still the same).

So now, what is the scheme for a normalization proof? Let p be the polynomial expression that the user wants to normalize. First a little piece of ML code guesses the type of p, the ring theory T to use, an abstract polynomial ap and a variables map v such that p is betadeltaiota-equivalent to (interp v ap). Then we replace it by (interp v (polynomial_simplify ap)), using the main correctness theorem and we reduce it to a concrete expression p', which is the concrete normal form of p. This is summarized in this diagram:

`p`	->_{betadeltaiota}	`(interp v ap)`
		=_{(by the main correctness theorem)}
`p'`	<-_{betadeltaiota}	`(interp v (polynomial_simplify ap))`

The user do not see the right part of the diagram. From outside, the tactic behaves like a betadeltaiota simplification extended with AC rewriting rules. Basically, the proof is only the application of the main correctness theorem to well-chosen arguments.

19.7 History of `ring`

First Samuel Boutin designed the tactic 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:

Coq < Goal forall x y z:Z, x + 3 + y + y * z = x + 3 + y + z * y.
1 subgoal

  ============================
   forall x y z : Z, x + 3 + y + y * z = x + 3 + y + z * y

Coq < intros; rewrite (Zmult_comm y z); reflexivity.

Coq < Save toto.

Coq < Print  toto.
toto =
fun x y z : Z =>
eq_ind_r (fun z0 : Z => x + 3 + y + z0 = x + 3 + y + z * y)
  (refl_equal (x + 3 + y + z * y)) (Zmult_comm y z)
     : forall x y z : Z, x + 3 + y + y * z = x + 3 + y + z * y
Argument scopes are [Z_scope Z_scope Z_scope]

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 ACDSimpl was too slow, Samuel Boutin rewrote it using reflection (see his article in TACS'97 [17]). Later, the stuff was rewritten by Patrick Loiseleur: the new tactic does not any more require ACDSimpl to compile and it makes use of betadeltaiota-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see 19.8). He also wrote a few ML code for the Add Ring command, that allow to register new rings dynamically.

Proofs terms generated by ring are quite small, they are linear in the number of + and × 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.

19.8 Discussion

Efficiency is not the only motivation to use reflection here. 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 ACDSimpl, the only constants were 0 and 1. So the expression 34 + 2*(x - 1) + 12 is interpreted as V₀ + V₁ × (V₂ - 1) + V₃, with the variables mapping {V₀ |-> 34; V₁ |-> 2; V₂ |-> x; V₃ |-> 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 computation) to achieve the normalization.

The tactic 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 ring tactic uses intensively the conversion rule of pCic, 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 Auto or Linear: that do many complex computations, using side-effects and backtracking, and generate a small proof term. Clearly, it would be a non-sense to replace them by tactics using reflection.

Another argument against the reflection is that Coq, as a programming language, has many nice features, like dependent types, but is very far from the speed and the expressive power of Objective Caml. Wait a minute! With Coq it is possible to extract ML code from pCic terms, right? So, why not to link the extracted code with Coq to inherit the benefits of the reflection and the speed of ML tactics? That is called total reflection, and is still an active research subject. With these technologies it will become possible to bootstrap the type-checker of pCic, but there is still some work to achieve that goal.

Another brilliant idea from Benjamin Werner: reflection could be used to couple a external tool (a rewriting program or a model checker) with Coq. We define (in Coq) a type of terms, a type of traces, and prove a correction theorem that states that replaying traces is safe w.r.t some interpretation. Then we let the external tool do every computation (using side-effects, backtracking, exception, or others features that are not available in pure lambda calculus) to produce the trace: now we replay the trace in Coq, and apply the correction lemma. So internalization seems to be the best way to import ... external proofs!

Chapter 19 The ring tactic