We describe how we connected three programs that compute Gro¨bner bases [1] to Coq [11], to do automated proofs on algebraic, geometrical and arithmetical expressions. The result is a set of Coq tactics and a certificate mechanism 1. The programs are: F4 [5], GB [4], and gbcoq [10]. F4 and GB are the fastest (up to our knowledge) available programs that compute Gro¨bner bases. Gbcoq is slow in general but is proved to be correct (in Coq), and we adapted it to our specific problem to be efficient. The automated proofs concern equalities and non-equalities on polynomials with coefficients and indeterminates in R or Z, and are done by reducing to Gro¨bner computation, via Hilbert's Nullstellensatz. We adapted also the results of [7], to allow to prove some theorems about modular arithmetics. The connection between Coq and the programs that compute Gro¨bner bases is done using the ”external” tactic of Coq that allows to call arbitrary programs accepting xml inputs and outputs. We also produce certificates in order to make the proof scripts independant from the external programs.
Proof assistants contain now more and more automatic procedures that generate proofs in specific domains. In the Coq system, several tactics exist, for example the omega tactic which proves inequalities between linear expressions with integer variables, the fourier tactic which does the same thing with real numbers, the ring and field tactic, which proves equalities between expressions in a ring or a field, the sos tactic which proves some inequalities on real polynomials. We describe here a new tactic, called gb, which proves (non-)equalities in rings using other (non-)equalities as hypotheses. For example 8xy : R; x2 + xy = 0; y2 + xy = 0 ) x + y = 0, or 8x : R; x2 6= 1 ) x 6= 1.
This tactic uses external efficient programs that compute Gro¨bner bases, and their result to produce a proof and a certificate.
We wrote such a tactic several years ago [
This paper is organized as follow. In section 2 we explain the mathematical method we use to reduce
the problem to Gro¨bner bases computations. In section 3 we detail the tactic and the way it builds a
proof in Coq. In section 4 we show how we connected Coq to the specialized programs that computes
Gro¨bner bases. Section 5 details the complete tactics that proves also non-equalities, and section 6 shows
how to produce certificates and then save time in the proof script. In section 7 we give some examples
of utilisations of the tactic in algebra, geometry and arithmetics, with comparisons with hol-light[
Hilbert Nullstellensatz shows how to reduce proofs of equalities on polynomials to algebraic
computations (see for example [
It is easy to see that if a polynomial P in K[X1; : : : ; Xn] verifies Pr = åi=1 QiPi, with r a positive integer, Qi and Pi also in K[X1; : : : ; Xn], then P is zero whenever polynomials P1; :::; Ps are zero.
Then we can reduce the proof of P1 = 0; : : : ; Ps = 0 ) P = 0 to find Q1; : : : ; Qs and r such that Pr = åi QiPi.
The converse is also true when K is algebraically closed: this is the Hilbert Nullstellensatz. In this case, the method is complete.
Finding Pr = åi QiPi can be done using Gro¨bner bases, as we will explain now.
Recall that an ideal I of a ring is an additive sub-group of the ring such that ax 2 I whenever a 2 I . The ideal generated by a family of polynomials is the set of all linear combinations of these polynomials (with polynomial coefficients).
A Gro¨bner basis of an ideal is a set of polynomials of the ideal such that their head monomials (relative to a choosen order on monomials, e.g. lexicographic order, or degree order) generates the ideal of head monomials of all polynomials in the ideal. The main property of a Gro¨bner basis is that it provides a test for the membership to the ideal: a polynomial is in the ideal iff its euclidian division by the polynomials of the basis gives a zero remainder. The division process is a generalisation of the division of polynomials in one variable: to divide a polynomial P by a polynomial aX a Q we write P = aX a S + T where T contains no monomial that is multiple of X a . Then change P with QS + T and repeat divison. The last non zero T is the remainder of the division. To divide a polynomial by a family of polynomials, we repeat this process with each polynomial of the family. In general, the remainder depends on the order we use the polynomials of the family. But with a Gro¨bner basis, this remainder is unique (this is a characteristic property of Gro¨bner basis). 2.1
Method 1: how to find Q1; : : : ; Qs such that 1 = åi QiPi Compute a Gro¨bner base of the polynomials ftPi ei; eie j; eitgi; j (where t; e1; : : : ; es are new variables) with an order such that t > Xi > ei.
Suppose that, in this basis, there is a polynomial of the form t åi Qiei. This polynomial is then in the ideal generated by ftPi ei; eie j; eitgi; j, so is a linear combination of these polynomials: t åi Qiei = åi hi(tPi ei) + åi j gi jeie j + åi kieit ei are formal variables, so we can substitute formally ei with tPi, and we obtain t(1 åi QiPi) = 0 + t2( åi j gi jPiPj + åi kiPi).
Then the coefficient of t in this equation must be zero: 1 åi QiPi = 0, and we are done.
Note that the polynomials feit; eie jg are not necessary, but their presence much speed up the computation of the Gro¨bner basis2. 2.2
Method 2: how to find Q1; : : : ; Qs and r such that Pr = åi QiPi Use the standard trick: search to write 1 = åi hiPi + h(1 zP) ( ), where z is a new variable. This can be done with the previous method. Suppose we succeed. Let r be the max degree in z of polynomials hi.
Substitute formally z with 1=P, and multiply the equation (*) by Pr. Then we obtain Pr = åi QiPi, as required, where Qi = Prhi[z 1=P]
2.3
It is easy to see that methods 1 and 2 are complete in the sense that if Pr = åi QiPi holds, there will find such an equation: method 1: suppose 1 åi QiPi = 0. Then t = åi QitPi, and t åi Qiei = åi Qi(tPi ei). Hence t åi Qiei belongs to the ideal of which we have computed a Gro¨bner basis. Because of the order we have choosen on variables, this implies that there is a polynomial t åi hiei in the Gro¨bner basis. method 2: suppose Pr = åi QiPi. We have 1 zrPr = (1 + zP + : : : + zr 1Pr 1)(1 zP). Replacing Pr with åi QiPi we obtain 1 = zr(åi QiPi) + (1 + zP + : : : + zr 1Pr 1)(1 zP). 2.4
Take p = x + y; p1 = x2 + xy; p2 = y2 + xy. With the previous method, the Gro¨bner basis is: t zye0 zxe0 z2e1 z2e2 y2e0 x2e0 + zye1 zxe2 yxe0 + x2e0 + zye2 + zxe2 e20 xe1 ye2 e0e1; e12; e0e2; e1e2; e22 we obtain r = 2; Q1 = 1; Q2 = 1, and then (x + y)2 = 1 that x2 + xy = 0; y2 + xy = 0 ) x + y = 0. 3
(x2 + xy) + 1
(y2 + xy). Which proves
Coq [
Typically we will treate goals of the form: x : Z y : Z H : x ^ 2 + x * y = 0 H0 : y ^ 2 + x * y = 0 ============================ x + y = 0 Here hypotheses are variables belonging in a ring or a field, and equalities between polynomials.
We explain now how to compute and use the Nullstellensatz equation to build a proof of this goal in Coq. The steps are: syntaxification, Gro¨bner basis computation, and building the proof from the Nullstellensatz equation. 3.1
We begin by building polynomials from the three equations in this goal. This is done in the tactic language of Coq (LTAC, which is a meta-language for computing tactics and executing them) by first computing the list of variables:
and the list of polynomials: lp = (cons (Add (Pow (Var 2) 2) (Mul (Var 2) (Var 1))) (cons (Add (Pow (Var 1) 2) (Mul (Var 2) (Var 1))) (cons (Sub (Add (Var 2) (Var 1)) (Const 0 1))
nil)))
Variables are represented by their rank in the list of variables. Polynomials are elements of an inductive type, and we can recover the equations by interpreting them in Z with the list of variables. For example, (interpret (Add (Pow (Var 2) 2) (Mul (Var 2) (Var 1)))
lv) evaluates in x^2 + x * y.
We used parts of the code of the sos[
We call the external program gb (see section 4) with the list of polynomials; here we choose the program F4 to compute Gro¨bner basis: external "./gb" "jcf2" lp
The result is the term: (cons (Pow (Add (Add Zero (Mul (Add (Add Zero (Mul (Const 0 1) (Const 1 1)))
(Mul (Const 1 1) (Pow (Var 1) 1))) (Const 1 1))) (Mul (Const 1 1) (Pow (Var 2) 1))) 2) (cons (Const 1 1) (cons(Const 1 1) (cons (Const 1 1) nil))))
which has the structure (cons (Pow p d) (cons c lq)) such that the Nullstellensatz equation holds: Here, we have lq = q1; q2, q1 = q2 = 1 cpd = å qi pi qi2lq 3.3
After interpreting the polynomials q1 and q2 in Z using the original list of variables, we get and prove easily the goal 1 * (x + y)^2 = 1 * (x ^ 2 + x * y) + 1 * (y ^ 2 + x * y) by the ring tactic.
To prove the original goal, it is now sufficient to rewrite x^2 + x * y and y^2 + x * y by 0, getting 1 * (x + y)^2 = 0, and, using a simple lemma, we get x + y = 0 and we are done. 4
Coq allows to call arbitrary external programs via a function called ”external”. It sends Coq terms in xml format (i.e. as tree) to the standard output of the external program, and gets its standard output (also in xml format) as a resulting Coq term. We use this function to compute a Gro¨bner basis of a list of polynomials, via a single interface to three specialized programs: F4, GB, and gbcoq. This interface, called ”gb” is written in ocaml. It translates the list of polynomials given as standard input in xml format in the format of the choosen program (F4, GB or gbcoq), call it with the good arguments, get its result (a Gro¨bner basis, if no error occured), selects its useful information, translates it in xml and sends it as result to standard output. More precisely:
F4 is a C library, and has only an interface for Maple. We wrote a simple parser of polynomials to use it on command line, helped by J.C. Fauge`re.
GB is also written in C and has a command line interface, or accept inputs in a file; with a Maplelike syntax for polynomials.
Gbcoq is written in ocaml, so is integrated to gb. This program uses an Buchberger-like algorithm which has been extracted from Coq. So it is proven to be correct. We added recently an optimisation which reduces drastically the time to compute Nullstellensatz equations: each time we add a new polynomial during the completion via the reduction of critical pairs, we divide the polynomial that we want to test if it is in the ideal, by the current family of polynomials. If this gives zero, then we stop:, and return the Nullstellensatz coefficients, deduced from the divisions we made. More we also try its powers (up to a parametrized limit). Then, when we have computed the whole Gro¨bner basis, we can compute the Nullstellensatz coefficients, without having to verify that the remaining critical pairs reduce to zero. More, this is often the case that the polynomial reduces to zero with a partial Gro¨bner basis! The time is sometimes divided by 1000 with such a technique, and always much reduced. Note that such an improvement cannot be made in a blackbox program such as the programs of JC Fauge`re, which are free but not opensource. 5
We wrote two tactics: gbR for real numbers, gbZ for integers. The set of integer is not a field, but we can simulate computations in the field of rational numbers using only integers. In this case, the Nullstellensatz equation become cpd = åi qi pi, where c is an integer, and the qi have integer coefficients.
We can allow negations of equations in the conclusion. For example xy = 1 ) x 6= 0. The trick is to replace x 6= 0 with x = 0 ) 1 = 0, which is equivalent to add a new equation in hypotheses, and replace the equation to prove with 1 = 0.
In the case of real numbers, we can allow also negations of equations in hypotheses. For example x2 6= 1 ) x 6= 1. This can be done by introducing new variables, remarking that p 6= 0 , 9t; p t = 1. In the example, this gives t(x2 1) = 1 ) x 6= 1. The negation in conclusion can be removed and leads to t(x2 1) = 1; x 1 = 0 ) 1 = 0, which is proven using the Nullstellensatz equation 1 = 1 (t(x2 1) 1) + (t + tx) (x 1)
Finally, the tactics use first the program F4. If it fails (for memory limits), then the tactics try GB. If it fails too, then the tactics uses gbcoq. We have also specialised tactics, allowing the user to choose which program to use, between F4, GB, and gbcoq. Indeed, experiments show that no one is better than others.
Once the Nullstellensatz equation is computed, we can change the proof script, replacing the tactic gb with a similar tactic, called ”check gb” which will not call external programs, but instead it will take as arguments all the components of the Nullstellensatz equation. So, next time we will execute the proof script, for compilation for example, it will not need external Gro¨bner computation3. Let us give an example. Suppose we want to prove:
Goal forall x y z:R, x^2+x*y=0 -> y^2+x*y=0 -> x+y=0.
we execute the tactic gbR, which proves the goal, and prints these lines in the standard output of Coq: (* with JC.Faugere algorithm F4 *) gbR_begin; check_gbR (x + y - 0) (List.cons (x * (x * 1) + x * y) (List.cons (y * (y * 1) + x * y) List.nil)) (List.cons y (List.cons x List.nil)) (lceq (Pow (Add (Add Zero (Mul (Add (Add Zero (Mul (Const 0 1) (Const 1 1)))
(Mul (Const 1 1) (Pow (Var 1) 1))) (Const 1 1))) (Mul (Const 1 1) (Pow (Var 2) 1))) 2) (lceq (Const 1 1) (lceq (Const 1 1) (lceq (Const 1 1) lnil)))) .
Then, we can replace the line calling gbR with these tactics lines, which contains no more than the components of the needed Nullstellensatz equation (x + y)2 = 1 (x2 + xy) + 1 (y2 + xy), and then need much less time to evaluate, because it doesn’t need Gro¨bner basis computation.
In this section we give several examples of use of the tactics gbR and gbR.
The following examples uses the symetric expressions of coefficients with roots of a polynomial.
First in degree 3: if x; y; z are the three complex roots of X3 + a X2 + b X + c then we have a = (x + y + z), b = x y + y z + z x, and c = x y z. And then we can prove that x + y + z = 0 ) x y + y z + z x = 0 ) x y z = 0 ) x = 0, because then the polynomial becomes X3, and has only 0 as a root.
Require gbZ.
Goal forall x y z:Z,
x+y+z=0 -> x*y+y*z+z*x=0 -> x*y*z=0 -> x=0. gbZ.
Qed.
Goal forall x y z u:Z, x+y+z+u=0 -> x*y+y*z+z*u+u*x+x*z+u*y=0 -> x*y*z+y*z*u+z*u*x+u*x*y=0 -> x*y*z*u=0 -> x=0. gbZ.
Qed.
Goal forall x y z u v:Z, x+y+z+u+v=0 -> x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0-> x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0-> x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 -> x*y*z*u*v=0 -> x^5=0. gbZ.
Qed.
Last example takes less than 1s with F4 and GB, and gbcoq. With hol-light, it takes 1s.
Open Scope R_scope.
Record point:Type:={
X:R;
Y:R}.
Desargues theorem is too complicated to be proved with Gro¨bner bases. But Pappus theorem can. We formalize in Coq the set of points in the real plane:
Then we give two definitions of colinearity of three points (the theorem is false if we use only the second definition, because of degenerated configurations): Definition colinear(C A B:point):=
exists a:R, (X C)=a*(X A)+(1-a)*(X B) /\ (Y C)=a*(Y A)+(1-a)*(Y B).
Definition colinear2(A B C:point):= (X A)*(Y B)+(X B)*(Y C)+(X C)*(Y A) =(Y B)*(X C)+(Y C)*(X A)+(Y A)*(X B).
Then we state and prove the Pappus theorem, in a specialized (but without lost of generality) configuration: Lemma pappus: forall A B C A' B' C' D E F:point, (X A')=0 -> (X B')=0-> (X C')=0 -> (Y A)=0 -> (Y B)=0 -> (Y C) = 0 -> colinear D A B' -> colinear D A' B -> colinear E A C' -> colinear E A' C -> colinear F B C' -> colinear F B' C -> colinear2 D E F. ... gbR_choice 2.
Qed.
In this example, F4 fails, GB takes 9s, and gbcoq takes 3s. We also tried hol-light with this example, which takes 77s: ./hol prioritize_int();; let t1 = Unix.time();; int_ideal_cofactors [`XD -( x4 * XA )`; `YD -((&1 - x4) * YB1)`; `XD -( (&1 - x3) * XB)`; `YD - (x3 * YA1)`; ` XE - x2 * XA`; `YE - (&1 - x2) * YC1`; ` XE - (&1 - x1) * XC`; ` YE - x1 * YA1`; ` XF - x0 * XB`; ` YF - (&1 - x0) * YC1`; ` XF - (&1 - x) * XC`; ` YF - x * YB1`] ` XD * YE + XE * YF + XF * YD -(YE * XF + YF * XD + YD * XE)`;; Unix.time()-.t1;; 7.3
The general case of Pappus theorem is too complicated to compute.
Following the idea of [
Definition modulo(a b p:Z):= exists k:Z, a - b = k*p.
Definition ideal(x a b:Z):= exists u:Z, exists v:Z, x = u*a+v*b.
Definition gcd(g a b:Z):= divides g a /\ divides g b /\ ideal g a b.
Definition coprime(a b:Z):= exists u:Z, exists v:Z, 1 = u*a+v*b.
Goal forall a b c:Z, divides a (b*c) -> coprime a b -> divides a c. gbarith.
Qed.
Goal forall m n r:Z, divides m r -> divides n r -> coprime m n -> divides (m*n) r. gbarith.
Qed.
Goal forall x y a n:Z, modulo (x^2) a n -> modulo (y^2) a n -> divides n ((x+y)*(x-y)). gbarith.
Qed. 7.4
Previous examples, and more we made, show that no one among F4, GB, gbcoq and is better than others. hol-light is sometimes better than F4 and GB, but gbcoq is much better than hol-light. The reason is simple: we often stop computations before obtaining a Gro¨bner basis. 8
The ”external” tactic of Coq is a very good tool to use efficient programs to produce proofs in specific domains. We have shown how to use efficient Gro¨bner bases computations in this context. The use of certificates should be developped to reduce time of re-verification of proofs. The certificate can be written explicitely in the proof script, as we have shown here, but it could be stored in a cache. We have shown the interest of using external programs, but also their limits, as soon as it is impossible or difficult to adapt them to specific use of proof systems. We plan to investigate other decisions procedures, for example polynomial system solving, to produce new tactics in the same spirit.
Acknowledgements: we thank anonymous referees for their suggestions on the redaction of this paper and bibliographical completions. Connecting Gro¨ bner bases programs with Coq