Connecting Gröbner bases programs with Coq to do proofs in algebra, geometry and arithmetics Loı̈c Pottier INRIA Sophia Antipolis Abstract We describe how we connected three programs that compute Grö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 Grö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 Grö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 Grö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. 1 Introduction Proof assistants contain now more and more automatic procedures that generate proofs in specific do- mains. 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, x2 + xy = 0, y2 + xy = 0 ⇒ x + y = 0, or ∀x : R, x2 6= 1 ⇒ x 6= 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 67 Connecting Gröbner bases programs with Coq Pottier 2 Hilbert Nullstellensatz Hilbert Nullstellensatz shows how to reduce proofs of equalities on polynomials to algebraic computa- tions (see for example [3] for the notions introduced in this section). It is easy to see that if a polynomial P in K[X1 , . . . , Xn ] verifies Pr = ∑si=1 Qi Pi , 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 r P = ∑i Qi Pi . 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 Qi Pi 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). 2.1 Method 1: how to find Q1 , . . . , Qs such that 1 = ∑i Qi Pi Compute a Gröbner base of the polynomials {tPi − ei , ei e j , eit}i, 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 Qi ei . This polynomial is then in the ideal generated by {tPi − ei , ei e j , eit}i, j , so is a linear combination of these polynomials: t − ∑i Qi ei = ∑i hi (tPi − ei ) + ∑i j gi j ei e j + ∑i ki eit ei are formal variables, so we can substitute formally ei with tPi , and we obtain t(1 − ∑i Qi Pi ) = 0 + t 2 ( ∑i j gi j Pi Pj + ∑i ki Pi ). Then the coefficient of t in this equation must be zero: 1 − ∑i Qi Pi = 0, and we are done. Note that the polynomials {eit, ei e j } are not necessary, but their presence much speed up the com- putation of the Gröbner basis2 . 2.2 Method 2: how to find Q1 , . . . , Qs and r such that Pr = ∑i Qi Pi Use the standard trick: search to write 1 = ∑i hi Pi + 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 Qi Pi , as required, where Qi = Pr hi [z ← 1/P] 2 thanks to Bernard Mourrain for this trick 68 Connecting Gröbner bases programs with Coq Pottier 2.3 Completness It is easy to see that methods 1 and 2 are complete in the sense that if Pr = ∑i Qi Pi holds, there will find such an equation: • method 1: suppose 1 − ∑i Qi Pi = 0. Then t = ∑i QitPi , and t − ∑i Qi ei = ∑i Qi (tPi − ei ). Hence t − ∑i Qi ei 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 hi ei in the Gröbner basis. • method 2: suppose Pr = ∑i Qi Pi . We have 1 − zr Pr = (1 + zP + . . . + zr−1 Pr−1 )(1 − zP). Replacing Pr with ∑i Qi Pi we obtain 1 = zr (∑i Qi Pi ) + (1 + zP + . . . + zr−1 Pr−1 )(1 − zP). 2.4 Example Take p = x + y, p1 = x2 + xy, p2 = y2 + xy. With the previous method, the Gröbner basis is: t − zye0 − zxe0 − z2 e1 − z2 e2 − e0 y2 e0 − x2 e0 + zye1 − zxe2 − e1 + e2 yxe0 + x2 e0 + zye2 + zxe2 − e2 e20 xe1 − ye2 e0 e1 , e21 , e0 e2 , e1 e2 , e22 we obtain r = 2, Q1 = 1, Q2 = 1, and then (x + y)2 = 1 × (x2 + xy) + 1 × (y2 + xy). Which proves that x2 + xy = 0, y2 + xy = 0 ⇒ x + y = 0. 3 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 ∀H1 : T1 , . . . , ∀Hn : Tn ,C(H1, . . . , Hn ). 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. 3.1 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: 69 Connecting Gröbner bases programs with Coq Pottier lv = (cons y (cons x nil)) 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 in- ductive 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[8] tactic, written by Laurent Théry. 3.2 Calling Gröbner basis computation We call the external program gb (see section 4) with the list of polynomials; here we choose the program F4 to compute Grö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: cpd = ∑ qi pi qi ∈lq Here, we have lq = q1 , q2 , q1 = q2 = 1 70 Connecting Gröbner bases programs with Coq Pottier 3.3 Building the proof from the Nullstellensatz equation 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 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 Maple- like 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 optimisa- tion 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. 5 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 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 2 x 6= 1 ⇒ x 6= 1. This can be done by introducing new variables, remarking that p 6= 0 ⇔ ∃t, p ∗ t = 1. 71 Connecting Gröbner bases programs with Coq Pottier 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. 6 Certificates 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 Grö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 Gröbner basis computation. 7 Examples In this section we give several examples of use of the tactics gbR and gbR. 3 thanks to Julien Narboux for this suggestion 72 Connecting Gröbner bases programs with Coq Pottier 7.1 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 2 + 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 X 3 , 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. More complicated, the same thing in degrees 4 and 5: 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. 7.2 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): 73 Connecting Gröbner bases programs with Coq Pottier 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) config- uration: 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)‘;; 74 Connecting Gröbner bases programs with Coq Pottier Unix.time()-.t1;; The general case of Pappus theorem is too complicated to compute. 7.3 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. Here are examples of its use in Coq: Definition divides(a b:Z):= exists c:Z, b=c*a. 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 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. 8 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. Acknowledgements: we thank anonymous referees for their suggestions on the redaction of this paper and bibliographical completions. 75 Connecting Gröbner bases programs with Coq Pottier References [1] Bruno Buchberger. Bruno buchberger’s phd thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. Journal of Symbolic ComputationVolume 41, Issues 3-4, Logic, Mathematics and Computer Science: Interactions in honor of Bruno Buchberger (60th birthday),, 2006. [2] Amine Chaieb and Makarius Wenzel. Context aware calculation and deduction. In Manuel Kauers, Manfred Kerber, Robert Miner, and Wolfgang Windsteiger, editors, Calculemus/MKM, volume 4573 of Lecture Notes in Computer Science, pages 27–39. Springer, 2007. [3] David Eisenbud. Commutative algebra with a view toward algebraic geometry. Graduate Texts in Mathemat- ics 150. Springer-Verlag, 1999. [4] Jean-Charles Faugère. Gb. http://fgbrs.lip6.fr/jcf/Software/Gb/index.html. [5] Jean-Charles Faugère. A new efficient algorithm for computing grobner bases (f4). volume 139, issues 1-3 of Journal of Pure and Applied Algebra, pages 61–88, 1999. [6] John Harrison. Towards self-verification of hol light. In Ulrich Furbach and Natarajan Shankar, editors, Proceedings of the third International Joint Conference, IJCAR 2006, volume 4130 of Lecture Notes in Computer Science, pages 177–191, Seattle, WA, 2006. Springer-Verlag. [7] John Harrison. Automating elementary number-theoretic proofs using gröbner bases. In Frank Pfenning, editor, Proceedings of the 21st International Conference on Automated Deduction, CADE 21, volume 4603 of Lecture Notes in Computer Science, pages 51–66, Bremen, Germany, 2007. Springer-Verlag. [8] John Harrison. Verifying nonlinear real formulas via sums of squares. In Klaus Schneider and Jens Brandt, editors, Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007, volume 4732 of Lecture Notes in Computer Science, pages 102–118, Kaiserslautern, Ger- many, 2007. Springer-Verlag. [9] Loı̈c Pottier Jérôme Créci. Gb: une procédure de décision pour le système coq. Journées Francaises des Langages Applicatifs, Sainte-Marie-de-Ré, pages http://jfla.inria.fr/2004/actes/actes–jfla–2004.tar.gz, 2004. [10] Loı̈c Pottier Laurent Théry. gbcoq, 1998. http://www-sop.inria.fr/croap/CFC/Gbcoq.html. [11] The Coq Development Team. The coq proof assistant, 2008. http://coq.inria.fr/V8.1pl3/refman/ index.html. 76