This note is based on Cox et al.², which gives a method for proving geometric theorems using Groebner basis. The theorem is first translated to a statement where one set of equations implies another equation. This statement is then verified in Singular by calculating the Groebner basis of the equation set. It is also shown how to use the Groebner basis to solve a set of equations.

Notation

Points are denoted by capital letters, as in C. A point is determined by its coordinates. For example, A = (1,2) says that the point A is at position x = 1, y = 2, if we let x and y span the plane as normal. A line segment is denoted by two capital letters marking the start and the stop of the line segment, as in AB. AB can also denote the length of this line segment if it appears in an equation. We also need to talk about vectors, which will be denoted by AB when the vector is defined by the two points A and B, or by A if the vector is defined by a single point, or by (1,2) if the vector is defined by the value of a point. We have

AB = B - A = (1-3,2-4) = (-2,-2)

if the point A is (1,2) and the point B is (3,4).

The theorem of Apollonius

The theorem which we shall prove is the following.
 
Theorem. Let ABC be a right triangle in the plane, with a right angle at A. The midpoint of the three sides and the foot of the altitude drawn from A to the line BC lie on a circle.
 

Finding the equations

We first find the equations that represent the theorem. Place A at (0,0), B at (a,0). Since the angle at A is a right angle, we have C = (0,b). The three midpoints have coordinates K = (s,0), L = (0,t), and M = (u,v). Note that we use the naming convention so that a, b are arbitrary, whereas s,…,z are determined by the values of a, b. K is a midpoint if the segments 2AK = AB, that is 2s = a, which gives us the first polynomial equation

F1: 2s - a = 0

L as a midpoint gives us

F2: 2t - b = 0

and M is a midpoint if BM = BC, that is,

2 [(u,v)-(a,0)] = (0,b) - (a,0)

which gives

F3: 2u - a = 0

F4: 2v - b = 0

Next we shall construct the point H = (w,x). AH is at right angles to BC if the inner product of these is zero. The inner product between two arbitrary vectors is (d,e) o (f,g) = df + ge, where "o" denotes the inner product. We get

AH o BC = (w,x) o (-a,b) = -wa + xb

which gives us

F5: wa - xb = 0

Further^{1 (theorem III)}, since

wb(a,0) - ab(w,x) + xa(0,b) = (0,0),

then B,H,C are on the same line if

wb + xa - ab = 0

and this gives us the sixth equation

F6: wb + xa - ab = 0

Finally we must consider the statement that K, L, M, H lie on a circle. A general collection of four points do not lie on a circle, but a collection of three points do. Thus, our conclusion can be restated as follows: if we construct the circle through K, L, and M, then H must lie on this circle also. To check this we need to construct the centre of the circle O = (y,z). K, L, and M  is on the same circle if KO = LO and KO = MO. A general circle is given by

 (X - a)² + (Y - b)² = R²

where (X,Y) is some point on the curve, (a,b) is the centre of the circle, and R is the radius. Equating the radiuses KO and LO gives

(s - y)² + (0 - z)² = (-y)² + (t - z)²

F7: (s - y)² + z² - y² - (t - z)² = 0

Equating KO and MO gives

F8: (s - y)² + z² - (u - y)² - (v - z)² = 0

Our conclusion is KO = HO which in the same manner gives us the last equation

G: (s - y)² + z² - (w - y)² - (x - z)² = 0

We have now translated the theorem of Apollonius into the statement that G follows from F1 - F8. We are now ready to complete the proof in Singular.

Completing the proof in Singular

From Proposition 8 and Corollary 9 in Cox et al.^{2 (pp. 295-6)} we form the following statement.

Statement. G follows generically from F1,…,F8 if {1} is the Groebner basis of (the ideal generated by) {F1,…,F8,1- pG} where p is a variable.

The following paragraph gives a more technical discussion of the above statement. You may skip it without consequence for the rest of this note. When we calculate a Groebner basis we must specify the ring of the coefficients. Here we have variables s,...,z and our ring is the real numbers with a,b as parameters. This makes a,b invertible and therefore different from zero which prevent a degenerate triangle. In general when performing automated theorem proving one must watch out not to include degenerated cases of the theorem to be proven. Let rad(Q) be the radical of the ideal generated by F1,...,F8 in R(a,b)[s,...,z]. If the polynomial G follows from F1,...,F8 we must have that Z(Q) is in Z(G) and so G = I(Z(G)) is in I(Z(Q)) = rad(Q) (Nullstellensatz). Z() denotes the zero set and I(X) are the functions X as zero set.

We are now ready to prove the theorem and do this simply by defining the polynomials and calculating the Groebner basis in Singular. The code is listed below:

ring R = (0,a,b),(p,s,t,u,v,w,x,y,z),lp;
poly F1 = 2s - a;
poly F2 = 2t - b;
poly F3 = 2u - a;
poly F4 = 2v - b;
poly F5 = aw - bx;
poly F6 = bw + ax - a*b;
poly F7 = (s-y)^2 + z2 - y2 - (z-t)^2;      //note that z2 is an abbreviation for z^2
poly F8 = (s-y)^2 + z2 - (u-y)^2 - (v-z)^2;
poly G = (w - y)^2 + (x-z)^2 - (s-y)^2 - z2;
poly G2 = 1 - p*G;
ideal i = F1,F2,F3,F4,F5,F6,F7,F8,G2;
std(Q);  //Groebner basis

The ring R is defined to have characteristic 0 (as the real numbers), parameters a,b , variables p,s,...,z , and a lexicographic ordering (lp). The resulting output is {1} as expected.

Exercise

Other geometric theorems can also be proved using this method. If you want, you can try to prove the following theorem of Pappus in the same manner. Remember to let coordinates which has arbitrary values be parameters with names a,b,... and coordinates which values are fixed by the parameters be variables with names s,t,... (or any other two easily distinguishable sets of characters). When you simulate in Singular place the a,b,... in the first bracket in the line that defines the ring and the s,t,... in the second.

Theorem (Pappus). A,B,C and A',B',C' are two groups of three points lying on two lines. If P,Q,R are constructed as in the figure these points are co-linear.

Solving systems of equations with Singular

Lets see how we can use the Groebner basis to solve equations. Assume we want to draw the circle of Apollonius (as I had to in this note). We draw the triangle and choose for example B = (10,0) and C = (0,5). To find the centre of the circle we need to solve 8 equations, F1 to F8, two of which are quadratic. Does this semm like a lot of work? Not if we calculate the Groebner basis first. Usually, as in this case, when we want to solve a set of equations, we are only interested in the values of only a few of the variables - here we want y and z. It is a surprising fact that the Groebner basis produce polynomials in which the variables are successively eliminated. Lets calculate the Groebner basis of F1 to F8 in Singular:

ring R = 0,(s,t,u,v,w,x,y,z),lp;
poly F1 = 2s - 10;
poly F2 = 2t - 5;
poly F3 = 2u - 10;
poly F4 = 2v - 5;
poly F5 = 10w - 5x;
poly F6 = 5w + 10x - 10*5;
poly F7 = (s-y)^2 + z2 - y2 - (z-t)^2;
poly F8 = (s-y)^2 + z2 - (u-y)^2 - (v-z)^2;
ideal i = F1,F2,F3,F4,F5,F6,F7,F8;
std(i);

The result is the following polynomials:

4z - 5
8y - 4z - 15
x -4
w + 2x - 10
2v - 5
2t - 5
s - 5

As we can see, the two first polynomials of the result equal to zero give us y = 2.5 and z = 1.25 - the centre of the circle. The elimination of variables is easier to observe in more complicated examples.

Obtaining and using Singular

The Singular package, including manuals and libraries, can be obtained gratis from
ftp://www.mathematik.uni-kl.de/pub/Math/Singular. Singular consists essentially of one main executable that is started in the command window. You then get the Singular prompt, ">", and can start giving commands. Use "<filename" if you want to read in the above commands from a file (to avoid typing).

References

1. D. Pedoe, Geometry: A Comprehensive Course, 1988.

2. D. Cox, J. Little, D. O'Shea, Ideals, varieties, and algorithms, Springer, 1997.

3. http://alamos.math.arizona.edu/~rychlik/577-notes.html (technical paper on the same subject of this note).