Claudio Sacerdoti Coen1
This chapter presents the extension of several equality related tactics to work over user-defined structures (called setoids) that are equipped with ad-hoc equivalence relations meant to behave as equalities. Actually, the tactics have also been generalized to relations weaker then equivalences (e.g. rewriting systems).
The work generalizes, and is partially based on, a previous implementation of the setoid_replace tactic by Clément Renard.
A parametric relation R is any term of type forall (x1:T1) …(xn:Tn), relationust be a constant expreariable 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:
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).
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.
Error messages:
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.
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.
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 20 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 20). 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:
Adds also the term Aminus which must be a constant expressed by means of Aopp.
Adds also the term Adiv which must be a constant expressed by means of Ainv.
See also: [38] for more details regarding the implementation of legacy field.
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 [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 βδι-reduction not only to replace the rewriting steps, but also to achieve the interleaving of computation and reasoning (see 20.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.
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 V0 + V1 × (V2 ⊖ 1) + V3, with the variables mapping {V0 ↦ 34; V1 ↦ 2; V2 ↦ x; V3 ↦ 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.