Introduction

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 ∀xy : R, x 2 + xy = 0, y 2 + xy = 0 ⇒ x + y = 0, or ∀x : R, x 2 = 1 ⇒ x = 1.

This tactic uses external efficient programs that compute Gröbner bases, and their result to produce a proof and a certificate.

We wrote such a tactic several years ago [9], but using only the gbcoq program, which were rather slow. So the tactic remained experimental and was not included in the Coq system. There are also similar tactics in other proof systems: in hol-light, John Harrison wrote a program that computes Gröbner bases to prove polynomial equalities, specially in arithmetics [7]. This program was adapted in Isabelle by Amine Chaieb and Makarius Wenzel for the same task [2]. We show on examples that our tactic is faster.

This paper is organized as follow. In section 2 we explain the mathematical method we use to reduce the problem to Grö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 Grö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 [6] . Section 8 contains the conclusion and perpectives of this work.

Rudnicki P, Sutcliffe G., Konev B., Schmidt R., Schulz S. (eds.); Proceedings of the Combined KEAPPA -IWIL Workshops, pp. 67-76 1 downloadable at http://www-sop.inria.fr/marelle/Loic.Pottier/gb-keappa.tgz

Pottier

Hilbert Nullstellensatz

Hilbert Nullstellensatz shows how to reduce proofs of equalities on polynomials to algebraic computations (see for example [3] for the notions introduced in this section).

It is easy to see that if a polynomial P in K[X 1 , . . . , X n ] verifies P r = ∑ s i=1 Q i P i , with r a positive integer, Q i and P i also in K[X 1 , . . . , X n ], then P is zero whenever polynomials P 1 , ..., P s are zero.

Then we can reduce the proof of P 1 = 0, . . . , P s = 0 ⇒ P = 0 to find Q 1 , . . . , Q s and r such that

P r = ∑ i Q i P i .

The converse is also true when K is algebraically closed: this is the Hilbert Nullstellensatz. In this case, the method is complete.

Finding P r = ∑ i Q i P i can be done using Grö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 ∈ I whenever a ∈ I . The ideal generated by a family of polynomials is the set of all linear combinations of these polynomials (with polynomial coefficients).

A Grö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 Grö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 α − Q we write P = aX α S + T where T contains no monomial that is multiple of X α . 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 Gröbner basis, this remainder is unique (this is a characteristic property of Gröbner basis).

Method 1: how to findQ 1 , . . . , Q s such that 1 = ∑ i Q i P i

Compute a Gröbner base of the polynomials {tP i − e i , e i e j , e i t} i, j (where t, e 1 , . . . , e s are new variables) with an order such that t > X i > e i .

Suppose that, in this basis, there is a polynomial of the form t − ∑ i Q i e i . This polynomial is then in the ideal generated by {tP i − e i , e i e j , e i t} i, j , so is a linear combination of these polynomials: t − ∑ i Q i e i = ∑ i h i (tP i − e i ) + ∑ i j g i j e i e j + ∑ i k i e i t e i are formal variables, so we can substitute formally e i with tP i , and we obtain t(1

− ∑ i Q i P i ) = 0 + t 2 ( ∑ i j g i j P i P j + ∑ i k i P i ).

Then the coefficient of t in this equation must be zero: 1 − ∑ i Q i P i = 0, and we are done. Note that the polynomials {e i t, e i e j } are not necessary, but their presence much speed up the computation of the Gröbner basis2 .

2.2 Method 2: how to find Q 1 , . . . , Q s and r such that P r = ∑ i Q i P i Use the standard trick: search to write 1 = ∑ i h i P i + 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 h i .

Substitute formally z with 1/P, and multiply the equation (*) by P r . Then we obtain P r = ∑ i Q i P i , as required, where

Q i = P r h i [z ← 1/P]

Connecting Gröbner bases programs with Coq Pottier

Completness

It is easy to see that methods 1 and 2 are complete in the sense that if P r = ∑ i Q i P i holds, there will find such an equation:

• method 1: suppose 1 − ∑ i Q i P i = 0. Then t = ∑ i Q i tP i , and t − ∑ i Q i e i = ∑ i Q i (tP i − e i ).

Hence t − ∑ i Q i e i belongs to the ideal of which we have computed a Gröbner basis. Because of the order we have choosen on variables, this implies that there is a polynomial t − ∑ i h i e i in the Gröbner basis.

• method 2: suppose P r = ∑ i Q i P i . We have 1 − z r P r = (1 + zP + . . .

+ z r−1 P r−1 )(1 − zP). Replacing P r with ∑ i Q i P i we obtain 1 = z r (∑ i Q i P i ) + (1 + zP + . . . + z r−1 P r−1 )(1 − zP).

Example

Take p = x + y, p 1 = x 2 + xy, p 2 = y 2 + xy. With the previous method, the Gröbner basis is: we obtain r = 2,

t − zye 0 − zxe 0 − z 2 e 1 − z 2 e 2 −Q 1 = 1, Q 2 = 1, and then (x + y) 2 = 1 × (x 2 + xy) + 1 × (y 2 + xy). Which proves that x 2 + xy = 0, y 2 + xy = 0 ⇒ x + y = 0.

Proof in Coq

Coq [11] is a proof assistant based on type theory, where we can interactively build proofs of goals, which are logical assertions of the form ∀H 1 : T 1 , . . . , ∀H n : T n ,C(H1, . . . , H n ). Using tactics, we can simplify the goal, while the system builds the corresponding piece of proof.

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, Gröbner basis computation, and building the proof from the Nullstellensatz equation.

Syntaxification

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:

Building the proof from the Nullstellensatz equation

After interpreting the polynomials q 1 and q 2 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.

Connecting F4, GB, and gbcoq to Coq

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 Grö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 Grö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. Faugè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 Grö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 Grö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 Faugère, which are free but not opensource.

The gbR and gbZ tactics in Coq

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 cp d = ∑ i q i p i , where c is an integer, and the q i have integer coefficients. We can allow negations of equations in the conclusion. For example xy = 1 ⇒ x = 0. The trick is to replace x = 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 x 2 = 1 ⇒ x = 1. This can be done by introducing new variables, remarking that p = 0 ⇔ ∃t, p * t = 1.

Pottier

Algebra

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 X 3 + a * X Last example takes less than 1s with F4 and GB, and gbcoq. With hol-light, it takes 1s.

Geometry

Desargues theorem is too complicated to be proved with Gröbner bases. But Pappus theorem can. We formalize in Coq the set of points in the real plane: Open Scope R_scope. Record point:Type:={ X:R; Y:R}.

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

Pottier

Unix.time()-.t1;;

The general case of Pappus theorem is too complicated to compute.

Arithmetics

Following the idea of [7], we can prove statements about coprimality, gcd and divisions. We have to do some work for that, because the tactic gbZ is not sufficient. But the problem is again an ideal membership one, then solvable by Gröbner basis computation. We have written a tactic doing that, called gbarith. 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.

Computation times, comparison with hol-light

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 Gröbner basis.

Conclusion

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 Grö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.