The ring and field tactic families¶
- Author
Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry 1
This chapter presents the tactics dedicated to dealing with ring and field equations.
What does this tactic do?¶
ring
does associative-commutative rewriting in ring and semiring
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 polynomial is an expression built on
variables \(V_0\), \(V_1\), \(\dots\) and constants by application
of \(\oplus\) and \(\otimes\).
Let an ordered product be a product of variables \(V_{i_1} \otimes \dots
\otimes V_{i_n}\) verifying \(i_1 ≤ i_2 ≤ \dots ≤ 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 the ring
tactic do? It normalizes polynomials over
any ring or semiring 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.
Example
- In the ring of integers, the normal form of
\(x (3 + yx + 25(1 − z)) + zx\)
- is
\(28x + (−24)xz + xxy\).
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\).
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, consider this expression
in the semiring nat
:
(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:
0 |
\(\mapsto\) |
if b then (4) else (f (3)) |
1 |
\(\mapsto\) |
(f (5)) |
2 |
\(\mapsto\) |
x |
Then normalize the “abstract” polynomial \(((V_1 \otimes V_2 ) \oplus V_2) \oplus (V_0 \otimes 2)\) In our example the normal form is: \((2 \otimes V_0 ) \oplus (V_1 \otimes V_2) \oplus (V_2 \otimes V_2 )\). 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)))
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.
Concrete usage in Coq¶
-
ring
The ring
tactic solves equations upon polynomial expressions of a ring
(or semiring) structure. It proceeds by normalizing both sides
of the equation (w.r.t. associativity, commutativity and
distributivity, constant propagation, rewriting of monomials) and
comparing syntactically the results.
-
ring_simplify
ring_simplify
applies the normalization procedure described above to
the given terms. 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
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
- Require Import ZArith.
- [Loading ML file z_syntax_plugin.cmxs ... done] [Loading ML file quote_plugin.cmxs ... done] [Loading ML file newring_plugin.cmxs ... done] [Loading ML file omega_plugin.cmxs ... done]
- 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.
- 1 subgoal ============================ forall a b c : Z, (a + b + c) ^ 2 = a * a + b ^ 2 + c * c + 2 * a * b + 2 * a * c + 2 * b * c
- intros; ring.
- No more subgoals.
- Abort.
- Goal forall a b:Z, 2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30.
- 1 subgoal ============================ forall a b : Z, 2 * a * b = 30 -> (a + b) ^ 2 = a ^ 2 + b ^ 2 + 30
- intros a b H; ring [H].
- No more subgoals.
- Abort.
-
Variant
ring [term*]
decides the equality of two terms modulo ring operations and
the equalities defined by the term
s.
Each term
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.
performs the simplification in the hypothesis named ident
.
注釈
-
ring_simplify term1; ring_simplify term2
is not equivalent to
-
ring_simplify term1 term2
In the latter case the variables map
is shared between the two terms, and common subterm t of term1
and term2
will have the same associated variable number. So the first
alternative should be avoided for terms belonging to the same ring
theory.
Error messages:
-
Error
Not a valid ring equation.
¶ The conclusion of the goal is not provable in the corresponding ring theory.
-
Error
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.
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
Tactics enabled on user provided relations).
The definitions of ring and semiring (see module Ring_theory
) are:
- 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 }.
- Toplevel input, characters 70-71: > 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 }. > ^ Error: Syntax error: [constr:operconstr] expected after '=' (in [constr:operconstr]).
- 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 }.
- Toplevel input, characters 76-77: > 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 }. > ^ Error: Syntax error: [constr:operconstr] expected after '=' (in [constr:operconstr]).
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] }.
- Toplevel input, characters 52-53: > 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] }. > ^ Error: Syntax error: [constr:lconstr] expected after [vernac:of_type_with_opt_coercion] (in [record_binder_body]).
- 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] }.
- Toplevel input, characters 51-52: > 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] }. > ^ Error: Syntax error: [constr:lconstr] expected after [vernac:of_type_with_opt_coercion] (in [record_binder_body]).
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 semiring), 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
(orN
for semirings).- 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.
- Cpow is declared
- Variable Cp_phi : N -> Cpow.
- Cp_phi is declared
- Variable rpow : R -> Cpow -> R.
- Toplevel input, characters 29-30: > Variable rpow : R -> Cpow -> R. > ^ Error: The reference R was not found in the current environment.
- Record power_theory : Prop := mkpow_th { rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) }.
- Toplevel input, characters 70-73: > Record power_theory : Prop := mkpow_th { rpow_pow_N : forall r n, req (rpow r (Cp_phi n)) (pow_N rI rmul r n) }. > ^^^ Error: The reference req was not found in the current environment.
- End POWER.
The syntax for adding a new ring is
The ident
is not relevant. It is used just for error messages. The
term
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:
ring_mod ::= abstract | decidableterm
| morphismterm
| setoidterm
term
| constants [ltac
] | preprocess [ltac
] | postprocess [ltac
] | power_tacterm
[ltac
] | signterm
| divterm
- 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 hould be evaluable). Its type should be of the formforall 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 (seeRing_theory.ring_morph
andRing_theory.semi_morph
).- setoid
term
term
forces the use of given setoid. The first
term
is a proof that the equality is indeed a setoid (seeSetoid.Setoid_Theory
), and the secondterm
a proof that the ring operations are morphisms (seeRing_theory.ring_eq_ext
andRing_theory.sring_eq_ext
). This modifier needs not be used if the setoid and morphisms have been declared.- constants [
ltac
] specifies a tactic expression
ltac
that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returnsInitialRing.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.- preprocess [
ltac
] specifies a tactic
ltac
that is applied as a preliminary step forring
andring_simplify
. It can be used to transform a goal so that it is better recognized. For instance,S n
can be changed toplus 1 n
.- postprocess [
ltac
] specifies a tactic
ltac
that is applied as a final step forring_simplify
. For instance, it can be used to undo modifications of the preprocessor.- power_tac
term
[ltac
] allows
ring
andring_simplify
to recognize power expressions with a constant positive integer exponent (example: :\(x^2\) ). The termterm
is a proof that a given power function satisfies the specification of a power function (term has to be a proof ofRing_theory.power_theory
) andltac
specifies a tactic expression that, given a term, “abstracts” it into an object of typeN
whose interpretation viaCp_phi
(the evaluation function of power coefficient) is the original term, or returnsInitialRing.NotConstant
if not a constant coefficient (i.e. Ltac is the inverse function ofCp_phi
). See filesplugins/setoid_ring/ZArithRing.v
andplugins/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 outputting its normal form, i.e writingx − y
instead ofx + (− y)
. The term :n:`@term is a proof that a given sign function indicates expressions that are signed (term has to be a proof ofRing_theory.get_sign
). Seeplugins/setoid_ring/InitialRing.v
for examples of sign function.- div
term
allows
ring
andring_simplify
to use monomials with coefficients other than 1 in the rewriting. The termterm
is a proof that a given division function satisfies the specification of an euclidean division function (term
has to be a proof ofRing_theory.div_theory
). For example, this function is called when trying to rewrite \(7x\) by \(2x = z\) to tell that \(7 = 3 \times 2 + 1\). Seeplugins/setoid_ring/InitialRing.v
for examples of div function.
Error messages:
-
Error
Bad ring structure.
¶ The proof of the ring structure provided is not of the expected type.
-
Error
Bad lemma for decidability of equality.
¶ The equality function provided in the case of a computational ring has not the expected type.
-
Error
Ring operation should be declared as a morphism.
¶ A setoid associated to the carrier of the ring structure has been found, but the ring operation should be declared as morphism. See Tactics enabled on user provided relations.
How does it work?¶
The code of ring
is a good example of a tactic written using reflection.
What is reflection? Basically, using it means that a part of a tactic is written
in Gallina, Coq's language of terms, rather than Ltac or OCaml. From the
philosophical point of view, reflection 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 its 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.
- Toplevel input, characters 36-37: > 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. > ^ Error: The reference C was not found in the current environment.
Polynomials in normal form are defined as:
- Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol | PX : Pol -> positive -> Pol -> Pol.
- Toplevel input, characters 33-34: > Inductive Pol : Type := | Pc : C -> Pol | Pinj : positive -> Pol -> Pol | PX : Pol -> positive -> Pol -> Pol. > ^ Error: The reference C was not found in the current environment.
where Pinj n P
denotes P
in which \(V_i\) is replaced by \(V_{i+n}\) ,
and PX P n Q
denotes \(P \otimes V_1^n \oplus Q'\), Q' being Q where \(V_i\) is replaced by \(V_{i+1}\).
Variable maps are represented by lists 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 := [...].
- Toplevel input, characters 44-45: > Definition PEeval : list R -> PExpr -> R := [...]. > ^ Error: Syntax error: [reduce] expected after ':=' (in [vernac:def_body]).
- Definition Pphi_dev : list R -> Pol -> R := [...].
- Toplevel input, characters 44-45: > Definition Pphi_dev : list R -> Pol -> R := [...]. > ^ Error: Syntax error: [reduce] expected after ':=' (in [vernac:def_body]).
A function to normalize polynomials is defined, and the big theorem is its correctness w.r.t interpretation, that is:
- Definition norm : PExpr -> Pol := [...].
- Toplevel input, characters 34-35: > Definition norm : PExpr -> Pol := [...]. > ^ Error: Syntax error: [reduce] expected after ':=' (in [vernac:def_body]).
- Lemma Pphi_dev_ok : forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe.
- Toplevel input, characters 70-71: > Lemma Pphi_dev_ok : forall l pe npe, norm pe = npe -> PEeval l pe == Pphi_dev l npe. > ^ Error: Syntax error: [constr:operconstr] expected after '=' (in [constr:operconstr]).
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 \(\beta\delta\iota\)-
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:
p |
\(\rightarrow_{\beta\delta\iota}\) |
|
=(by the main correctness theorem) |
||
p’ |
\(\leftarrow_{\beta\delta\iota}\) |
|
The user does not see the right part of the diagram. From outside, the tactic behaves like a \(\beta\delta\iota\) simplification extended with rewriting rules for associativity and commutativity. Basically, the proof is only the application of the main correctness theorem to well-chosen arguments.
Dealing with fields¶
-
field
The field
tactic is an extension of the ring
tactic that deals with rational
expressions. 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 ring to solve
\(N = 0\).
Note that field
also generates nonzero 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. Nonzero
conditions are 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 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 plugins/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 the module Qcanon
.
Example
- Require Import Reals.
- [Loading ML file r_syntax_plugin.cmxs ... done] [Loading ML file fourier_plugin.cmxs ... done] [Loading ML file micromega_plugin.cmxs ... done]
- Open Scope R_scope.
- Goal forall x, x <> 0 -> (1 - 1 / x) * x - x + 1 = 0.
- 1 subgoal ============================ forall x : R, x <> 0 -> (1 - 1 / x) * x - x + 1 = 0
- intros; field; auto.
- No more subgoals.
- Abort.
- Goal forall x y, y <> 0 -> y = x -> x / y = 1.
- 1 subgoal ============================ forall x y : R, y <> 0 -> y = x -> x / y = 1
- intros x y H H1; field [H1]; auto.
- No more subgoals.
- Abort.
-
Variant
field [term*]
decides the equality of two terms modulo field operations and the equalities defined by the
term
s. Eachterm
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.
注釈
rewriting works with the equality m =
p only if p is a polynomial since
rewriting is handled by the underlying ring tactic.
-
Variant
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 fraction simplification. This yields smaller expressions when reducing to the same denominator since common factors can be canceled.
-
Variant
field_simplify [term*]
performs the simplification in the conclusion of the goal using the equalities defined by the
term
s.
-
Variant
field_simplify [term*] term*
performs the simplification in the terms
terms
of the conclusion of the goal using the equalities defined byterm
s inside the brackets.
-
Variant
field_simplify [term*] in ident
performs the simplification in the assumption
ident
using the equalities defined by theterm
s.
-
Variant
field_simplify [term*] term* in ident
performs the simplification in the
term
s of the assumptionident
using the equalities defined by theterm
s inside the brackets.
-
Variant
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\).
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 Tactics enabled on user provided relations). The definition of
fields and semifields 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 }.
- Toplevel input, characters 111-112: > 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 }. > ^ Error: Syntax error: [constr:operconstr] expected after '=' (in [constr:operconstr]).
- 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 }.
- Toplevel input, characters 115-116: > 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 }. > ^ Error: Syntax error: [constr:operconstr] expected after '=' (in [constr:operconstr]).
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) }.
- Toplevel input, characters 44-49: > Record linear : Type := mk_linear { num : PExpr C; denum : PExpr C; condition : list (PExpr C) }. > ^^^^^ Error: The reference PExpr was not found in the current environment.
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
The ident
is not relevant. It is used just for error
messages. term
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.
field_mod ::=ring_mod
| completenessterm
Since field tactics are built upon ring
tactics, all modifiers of the Add Ring
apply. There is only one
specific modifier:
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:
- Require Import ZArith.
- Open Scope Z_scope.
- 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
- intros; rewrite (Zmult_comm y z); reflexivity.
- No more subgoals.
- Save foo.
- foo is defined
- Print foo.
- foo = fun x y z : Z => eq_ind_r (fun z0 : Z => x + 3 + y + z0 = x + 3 + y + z * y) eq_refl (Z.mul_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 [Bou97]). Later, it
was rewritten by Patrick Loiseleur: the new tactic does not any
more require 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 Discussion). He also wrote
some ML code for the Add Ring
command that allows registering new rings dynamically.
Proofs terms generated by 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.
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_0 \oplus V_1 \otimes (V_2 \ominus 1) \oplus V_3\),
with the variables mapping
\(\{V_0 \mapsto 34; V_1 \mapsto 2; V_2 \mapsto x; V_3 \mapsto 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 the old one: by using
reflection, we get for free the integration of computation and reasoning
that would be very difficult to implement without it.
Is it the ultimate way to write tactics? The answer is: yes and no.
The ring
tactic intensively uses the conversion rules of the Calculus of
Inductive Constructions, i.e. it replaces proofs by computations as much as possible.
It can be useful in all situations where a classical tactic generates huge proof
terms, like symbolic processing and tautologies. 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 correctness theorem that states that replaying traces is safe with respect to 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 semantics by applying the correctness theorem.
Footnotes
- 1
based on previous work from Patrick Loiseleur and Samuel Boutin