Chapter 23  The ring and field tactic families

• What does this tactic do?
• The variables map
• Is it automatic?
• Concrete usage in Coq
• Adding a ring structure
• How does it work?
• Dealing with fields
• Adding a new field structure
• Legacy implementation
• History of ring
• Discussion

Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry¹

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

23.1  What does this tactic do?

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_i1 ⊗ … ⊗ V_in verifying i₁ ≤ i₂ ≤ … ≤ i_n. Let a 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 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. In fact, the actual representation shares monomials with same prefixes. 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:

1. In the ring of integers, the normal form of x (3 + yx + 25(1 − z)) + zx is 28x + (−24)xz + xxy.
2. 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)

ring is also able to compute a normal form modulo monomial equalities. For example, under the hypothesis that 2x² = yz+1, the normal form of 2(x + 1)x − x − zy is x+1.

23.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, it has 3 subterms. Give each subterm a number in an arbitrary order:

Then normalize the “abstract” polynomial

In our example the normal form is:

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))) 

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

23.4  Concrete usage in Coq

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

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 Require Import Ring. The ring structures must be declared with the Add Ring command (see below). The ring of booleans is predefined; if one wants to use the tactic on nat one must first require the module ArithRing (exported by Arith); for Z, do Require Import ZArithRing or simply Require Import ZArith; for N, do Require Import NArithRing or Require Import NArith.

Example:

Variants:

1. ring [term₁ … term_n] decides the equality of two terms modulo ring operations and rewriting of the equalities defined by term₁ … term_n. Each of term₁ … 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.
2. ring_simplify [term₁ … term_n] t₁ … t_m in ident performs the simplification in the hypothesis named ident.

Warning: ring_simplify term₁; ring_simplify term₂ is not equivalent to ring_simplify 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. So the first alternative should be avoided for terms belonging to the same ring theory.

Error messages:

1. not a valid ring equation The conclusion of the goal is not provable in the corresponding ring theory.
2. arguments of ring_simplify do not have all the same type ring_simplify cannot simplify terms of several rings at the same time. Invoke the tactic once per ring structure.
3. cannot find a declared ring structure over term No ring has been declared for the type of the terms to be simplified. Use Add Ring first.
4. cannot find a declared ring structure for equality term Same as above is the case of the ring tactic.

23.5  Adding a ring structure

Declaring a new ring consists in proving that a ring signature (a carrier set, an equality, and ring operations: Ring_theory.ring_theory and 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 24.7). The definition of ring and semi-rings (see module Ring_theory) is:

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

This implementation of 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 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:

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

where c0 and cI denote the 0 and 1 of the coefficient set, +!, *!, -! are the implementations of the ring operations, == is the equality of the coefficients, ?+! is an implementation of this equality, and [x] is a notation for the image of x by the ring morphism.

Since Z is an initial ring (and N is an initial semi-ring), it can always be considered as a set of coefficients. There are basically three kinds of (semi-)rings:

abstract rings

to be used when operations are not effective. The set of coefficients is Z (or N for semi-rings).

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.

customized ring

for other cases. The user has to provide the coefficient set and the morphism.

This implementation of ring can also recognize simple power expressions as ring expressions. A power function is specified by the following property:

 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.

The syntax for adding a new ring is Add Ring name : ring (mod₁,…,mod₂). The name is not relevent. 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:

abstract

declares the ring as abstract. This is the default.

decidable term

declares the ring as computational. The expression term is the correctness proof of an equality test ?=! (which should be evaluable). Its type should be of the form forall x y, x?=!y = true → x == y.

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 Ring_theory.ring_morph and Ring_theory.semi_morph).

setoid term₁ term₂

forces the use of given setoid. The expression term₁ is a proof that the equality is indeed a setoid (see Setoid.Setoid_Theory), and term₂ a proof that the ring operations are morphisms (see Ring_theory.ring_eq_ext and Ring_theory.sring_eq_ext). This modifier needs not be used if the setoid and morphisms have been declared.

constants [ L_tac

] 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 InitialRing.NotConstant. The default behaviour is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings.

preprocess [ L_tac

] specifies a tactic that is applied as a preliminary step for ring and ring_simplify. It can be used to transform a goal so that it is better recognized. For instance, S n can be changed to plus 1 n.

postprocess [ L_tac

] specifies a tactic that is applied as a final step for ring_simplify. For instance, it can be used to undo modifications of the preprocessor.

power_tac term [ L_tac

] allows ring and ring_simplify to recognize power expressions with a constant positive integer exponent (example: x²). 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 Ring_theory.power_theory) and L_tac specifies a tactic expression that, given a term, “abstracts” it into an object of type N whose interpretation via Cp_phi (the evaluation function of power coefficient) is the original term, or returns InitialRing.NotConstant if not a constant coefficient (i.e. L_tac is the inverse function of Cp_phi). See files contrib/setoid_ring/ZArithRing.v and contrib/setoid_ring/RealField.v for examples. By default the tactic does not recognize power expressions as ring expressions.

sign term

allows 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 Ring_theory.get_sign). See contrib/setoid_ring/IntialRing.v for examples of sign function.

div term

allows ring and 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 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 contrib/setoid_ring/IntialRing.v for examples of div function.

Error messages:

1. bad ring structure The proof of the ring structure provided is not of the expected type.
2. bad lemma for decidability of equality The equality function provided in the case of a computational ring has not the expected type.
3. ring 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 24.7.

23.6  How does it work?

The code of ring is a good example of tactic written using reflection. 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_polynom.v. Here a type for polynomials is defined:

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.

Polynomials in normal form are defined as:

 Inductive Pol : Type :=
  | Pc : C -> Pol 
  | Pinj : positive -> Pol -> Pol                   
  | PX : Pol -> positive -> Pol -> Pol.

where Pinj n P denotes P in which V_i is replaced by V_i+n, and PX P n Q denotes P ⊗ V₁ⁿ ⊕ 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:

Definition PEeval : list R -> PExpr -> R := [...].
Definition Pphi_dev : list R -> Pol -> R := [...].

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

Definition norm : PExpr -> Pol := [...].
Lemma Pphi_dev_ok :
   forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.

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 βδι-equivalent to (PEeval v ap). Then we replace it by (Pphi_dev v (norm 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:

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

23.7  Dealing with fields

The field tactic is an extension of the ring to deal with 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 expressions. For example, if we take F = (1 − 1/x) x − x + 1, this gives N= (x −1) x − x² + x and D= x. It then calls ring to solve N=0. Note that field also generates non-zero conditions for all the denominators it encounters in the reduction. In our example, it generates the condition x ≠ 0. These conditions appear as one subgoal which is a conjunction if there are several denominators. Non-zero conditions are always polynomial expressions. For example when reducing the expression 1/(1 + 1/x), two side conditions are generated: x≠ 0 and x + 1 ≠ 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 Require Import Field. New field structures can be declared to the system with the Add Field command (see below). The field of real numbers is defined in module RealField (in textttcontrib/setoid_ring). It is exported by module Rbase, so that requiring Rbase or Reals is enough to use the field tactics on real numbers. Rational numbers in canonical form are also declared as a field in module Qcanon.

Example:

Variants:

1. field [term₁ … term_n] decides the equality of two terms modulo field operations and rewriting of the equalities defined by term₁ … term_n. Each of term₁ … 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 ring tactic.
2. field_simplify performs the simplification in the conclusion of the goal, F₁ = F₂ becomes N₁/D₁ = N₂/D₂. A normalization step (the same as the one for rings) is then applied to N₁, D₁, N₂ and D₂. 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 cancelled.
3. field_simplify [term₁ … term_n] performs the simplification in the conclusion of the goal using the equalities defined by term₁ … term_n.
4. field_simplify [term₁ … term_n] t₁ …t_m performs the simplification in the terms t₁ …t_m of the conclusion of the goal using the equalities defined by term₁ … term_n.
5. field_simplify in H performs the simplification in the assumption H.
6. field_simplify [term₁ … term_n] in H performs the simplification in the assumption H using the equalities defined by term₁ … term_n.
7. field_simplify [term₁ … term_n] t₁ …t_m in H performs the simplification in the terms t₁ …t_n of the assumption H using the equalities defined by term₁ … term_m.
8. field_simplify_eq performs the simplification in the conclusion of the goal removing the denominator. F₁ = F₂ becomes N₁ D₂ = N₂ D₁.
9. field_simplify_eq [term₁ … term_n] performs the simplification in the conclusion of the goal using the equalities defined by term₁ … term_n.
10. field_simplify_eq in H performs the simplification in the assumption H.
11. field_simplify_eq [term₁ … term_n] in H performs the simplification in the assumption H using the equalities defined by term₁ … term_n.

23.8  Adding a new field structure

Declaring a new field consists in proving that a field signature (a carrier set, an equality, and field operations: Field_theory.field_theory and 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 24.7). The definition of fields and semi-fields is:

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

The result of the normalization process is a fraction represented by the following type:

Record linear : Type := mk_linear {
   num : PExpr C;
   denum : PExpr C;
   condition : list (PExpr C) }.

where num and denum are the numerator and denominator; 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 Add Field name : field (mod₁,…,mod₂). The name is not relevent. 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 behaviour of the tactic. Since field tactics are built upon ring tactics, all mofifiers of the Add Ring apply. There is only one specific modifier:

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. termis a proof of forall x y, [x] == [y] -> x?=!y = true, which is the completeness of equality on coefficients w.r.t. the field equality.

23.9  Legacy implementation

Warning: This tactic is the 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.

23.9.1  legacy ring term₁ … term_n

This tactic, written by Samuel Boutin and Patrick Loiseleur, applies associative commutative rewriting on every ring. The tactic must be loaded by Require Import LegacyRing. The ring must be declared in the Add Ring command. The ring of booleans is predefined; if one wants to use the tactic on nat one must first require the module LegacyArithRing; for Z, do Require Import LegacyZArithRing; for N, do Require Import LegacyNArithRing.

The terms term₁, …, term_n must be subterms of the goal conclusion. The tactic ring normalizes these terms w.r.t. associativity and commutativity and replace them by their normal form.

Variants:

1. legacy ring When the goal is an equality t₁=t₂, it acts like ring_simplify t₁ t₂ and then solves the equality by reflexivity.
2. ring_nat is a tactic macro for repeat rewrite S_to_plus_one; ring. The theorem S_to_plus_one is a proof that forall (n:nat), S n = plus (S O) n.

You can have a look at the files LegacyRing.v, ArithRing.v, ZArithRing.v to see examples of the Add Ring command.

23.9.2  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 Legacy 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:

1. Add Legacy 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).

2. Add Legacy 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.

3. Add Legacy Abstract Semi Ring A Aplus Amult Aone Azero Aeq T.

Error messages:

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

23.9.3  legacy field

This tactic written by David Delahaye and Micaela Mayero solves equalities using commutative field theory. Denominators have to be non equal to zero and, as this is not decidable in general, this tactic may generate side conditions requiring some expressions to be non equal to zero. This tactic must be loaded by Require Import LegacyField. Field theories are declared (as for legacy ring) with the Add Legacy Field command.

23.9.4  Add Legacy Field

This vernacular command adds a commutative field theory to the database for the tactic field. You must provide this theory as follows:

where A is a term of type Type, 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, Aopp is a term of type A->A, Aeq is a term of type A->bool, Ainv is a term of type A->A, Rth is a term of type (Ring_Theory A Aplus Amult Aone Azero Ainv Aeq), and Tinvl is a term of type forall n:A, ~(n=Azero)->(Amult (Ainv n) n)=Aone. To build a ring theory, refer to Chapter 23 for more details.

This command adds also an entry in the ring theory table if this theory is not already declared. So, it is useless to keep, for a given type, the Add Ring command if you declare a theory with Add Field, except if you plan to use specific features of ring (see Chapter 23). However, the module ring is not loaded by Add Field and you have to make a Require Import Ring if you want to call the ring tactic.

Variants:

1. Add Legacy Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
       with minus:=Aminus

   Adds also the term Aminus which must be a constant expressed by means of Aopp.

2. Add Legacy Field A Aplus Amult Aone Azero Aopp Aeq Ainv Rth Tinvl
       with div:=Adiv

   Adds also the term Adiv which must be a constant expressed by means of Ainv.

See also: [42] for more details regarding the implementation of legacy field.

23.10  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:

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 [18]). Later, the stuff was rewritten by Patrick Loiseleur: the new tactic does not any more require ACDSimpl to compile and it makes use of βδι-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see 23.11). 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.

23.11  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 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 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 can check in Coq that the trace has the expected semantic by applying the correction lemma.

1

based on previous work from Patrick Loiseleur and Samuel Boutin

• webmaster
• xhtml valid
• CSS valid