Needs["GeoProver`"]

GeoProver`gbasis[polys_,vars_]:=
  (* compute a lex Groebner basis of polys in k[vars] *)
  GroebnerBasis[polys,vars,CoefficientDomain -> RationalFunctions]

GeoProver`normalf[p_List,poly_,vars_]:=
	GeoProver`normalf[#,polys,vars]& /@ p

GeoProver`normalf[p_,polys_,vars_]:=
  (* compute the normal form of p wrt. polys in k[vars] *)
  Together[PolynomialReduce[p,polys,vars,
           CoefficientDomain -> RationalFunctions][[2]]]

Demo for the GeoProver package 
version 1.3 

Author: Hans-Gert Gräbe
Univ. Leipzig, Inst. f. Informatik,
D-04109 Leipzig,Germany

finished at January 20, 2003

Some one line proofs

Very elementary statements

Consider a generic triangle ABC

a=point[a1,a2] 
b=point[b1,b2]
c=point[c1,c2]

Its  perpendicular bisectors have a point in common since

isconcurrent[pbisector[a,b],pbisector[b,c],pbisector[c,a]]

simplifies to zero. This point

m=intersectionpoint[pbisector[a,b],pbisector[b,c]]

is the center of the circumscribed circle

eqdist[m,a,m,b]

The altitutes intersection theorem may be proved in the same way

isconcurrent[altitude[a,b,c],altitude[b,c,a],altitude[c,a,b]]

And the median intersection theorem also

isconcurrent[median[a,b,c],median[b,c,a],median[c,a,b]]

Euler's line

The theorem about Euler's line states that 

	the circumcenter M, the orthocenter H and the barycenter S are on a common line. 

To prove this statement we compute the corresponding generic coordinates:

m=intersectionpoint[pbisector[a,b],pbisector[b,c]]

h=intersectionpoint[altitude[a,b,c],altitude[b,c,a]]

s=intersectionpoint[median[a,b,c],median[b,c,a]]

They are all on a common line since

iscollinear[m,h,s]

Moreover, S divides MH with ratio 2:1. Indeed

sqrdist[s,varpoint[m,h,1/3]]

Feuerbach's circle

To prove this statement we choose a special coordinate system

a=point[0,0]
b=point[u1,0]
c=point[u2,u3]

compute coordinates of M, H, and the midpoint N of MH

m=intersectionpoint[pbisector[a,b],pbisector[b,c]]

h=intersectionpoint[altitude[a,b,c],altitude[b,c,a]]

n=midpoint[m,h]

and show that N is the center of the nine point circle passing through the midpoints of the sides of ABC

cc=pccircle[n,midpoint[a,b]]
{oncircle[midpoint[b,c],cc], oncircle[midpoint[a,c],cc]}

through the midpoints of the upper altitudes' parts

{oncircle[midpoint[a,h],cc], oncircle[midpoint[b,h],cc], oncircle[midpoint[c,h],cc]}

and the pedal points

{ oncircle[pedalpoint[a,ppline[b,c]],cc], oncircle[pedalpoint[b,ppline[a,c]],cc], oncircle[pedalpoint[c,ppline[a,b]],cc]}

clearndg[];

Non-linear Geometric Objects

The bisector intersection theorem

For the bisector intersection theorem take special coordinates

a=point[0,0]
b=point[1,0]
c=point[u1,u2]

The bisector intersection point can't be addressed directly, since unordered geometry cannot distinguish between inner and outer bisectors. Hence there are four intersection points of the three pairs of angle bisectors. The coordinates of each such point P

p=point[x1,x2]

satisfy three polynomial relations, one for each bisector pair,

polys={ onbisector[p,a,b,c]==0,
        onbisector[p,b,c,a]==0,
        onbisector[p,c,a,b]==0}

To prove the theorem we have to show the consistency of these equations. We may try to solve the equations

vars={x1,x2}
sol=Solve[polys,vars];

(be patient; we suppress the long output !) Since (Subscript[x, 2])is the distance from P to AB we may even check that P is the center of one of the tangent circles: Compute the other distances and compare them with (Subscript[x, 2])

con1=(sqrdistpl[p,ppline[a,c]]-sqrdistpl[p,ppline[a,b]])//Together//Numerator
con2=(sqrdistpl[p,ppline[b,c]]-sqrdistpl[p,ppline[a,b]])//Together//Numerator

con1 /. sol // Together

con2 /. sol  // Together

(again be patient). A more clever way uses Groebner bases (see supp.m for details) to prove these statements:

gb=gbasis[polys,vars]

normalf[{con1,con2},gb,vars]

Here is a constructive proof of the bisector intersection theorem. Take A,B, and P,

a=point[0,0]
b=point[1,0] 
p=point[u1,u2]

construct the lines l1 symmetric  to AB wrt.AP and l2 symmetric to AB  wrt. BP. They intersect in C and CP must bisect the  third angle:

l1=ppline[a,b]
l2=symline[l1,ppline[a,p]]
l3=symline[l1,ppline[b,p]]

onbisector[p,a,b,intersectionpoint[l2,l3]]

clearndg[];

Miquel's theorem

For a triangle ABC choose points P on AB, Q on BC, and R on AC. Then the circles through A,P,R, through B,P,Q, and through C,Q,R pass through a common point.

To prove this statement we choose A,B,C,P,Q,R

a=point[0,0]
b=point[1,0]
c=point[c1,c2]

p=lineslider[ppline[a,b],u1]
q=lineslider[ppline[b,c],u2]
r=lineslider[ppline[a,c],u3]

compute the coordinates of the intersection point X of the circles through A,P,R and B,P,Q other than P

x=otherccpoint[p,p3circle[a,p,r],p3circle[b,p,q]]

and finally show that it also belongs to the third circle

oncircle[x,p3circle[c,q,r]]

clearndg[];

Theorems of linear type

Pappus' theorem

Let A,B,C and P,Q,R be collinear. Then the intersection points AQ^PB, AR^PC and BR^QC are collinear. 

To prove this statement choose coordinates where the x-axis is AB.

a=point[0,0]
b=point[0,1]
c=point[0,u5]
p=point[u6,u7]
q=point[u8,u9]
r=point[u0,x2]

There is a single condition on P,Q,R that allows to be solved for (Subscript[x, 2])

polys = iscollinear[p, q, r]

The conclusion may be formulated as

con=iscollinear[
intersectionpoint[ppline[a,q],ppline[p,b]],
intersectionpoint[ppline[a,r],ppline[p,c]],
intersectionpoint[ppline[b,r],ppline[q,c]]]

Now solve the equation for (Subscript[x, 2]), substitute the solution into the conlusion and simplify.

sol = Solve[polys == 0, x2]

con/.sol//Together

Again there is a constructive solution

a=point[0,0]
b=point[0,1]
p=point[u6,u7]
q=point[u8,u9]

c=lineslider[ppline[a,b],u5]
r=lineslider[ppline[p,q],u0]

con=iscollinear[
	intersectionpoint[ppline[a,q],ppline[p,b]],
	intersectionpoint[ppline[a,r],ppline[p,c]],
	intersectionpoint[ppline[b,r],ppline[q,c]]]

clearndg[];

Theorems of non linear type

Fermat point

Let ABC be a triangle and ABP, BCQ, ACR equilateral triangles to the same side. Then AP, BQ and CR pass through a common point.

Choose coordinates

a=point[0,0]
b=point[0,2]
c=point[u1,u2]
p=point[x1,x2]
q=point[x3,x4]
r=point[x5,x6]

The coordinates are related by the polynomial conditions

polys={
	eqdist[p,b,b,c]==0, eqdist[p,c,b,c]==0, 
	eqdist[q,a,a,c]==0, eqdist[q,c,a,c]==0,
	eqdist[r,b,a,b]==0, eqdist[r,a,a,b]==0}

The conclusion reads as

con=isconcurrent[ppline[a,p], ppline[b,q], ppline[c,r]]

The statement is difficult to prove since there are auxiliary components (corresponding to triangles on the "wrong" sides). If we solve the polynomial conditions for the dependent variables

vars={x1,x2,x3,x4,x5,x6}

sol=Solve[polys,vars]

and substitute these solutions into the conclusion

con/.sol//Together

we observe that the theorem holds only for two of the 8 branches (this are exactly the solutions where the three equilateal triangles are on the "same" sides wrt. ABC).

To avoid this peculiarity we may use oriented angles and determine the outer triangles as isoceles with equal base angles.

polys2={
	eqdist[p,b,p,c]==0, 
	eqdist[q,a,q,c]==0,  
	eqdist[r,a,r,b]==0, 
	eqangle[r,a,b,p,b,c]==0, 
	eqangle[q,c,a,p,b,c]==0}

sol=Solve[polys2,{x1,x2,x3,x4,x6}]

Together[con/.sol]

Note that we proved a more general theorem than stated above: The theorem remains true for isoceles triangles with equal base angles.

clearndg[];

Desargue's theorem

The affine version of Desargue's theorem states: For triangles ABC and RST in similarity position AR, BS and CT pass through a common point.
Here is a constructive proof. Choose A,B,C,R arbitrary

a=point[a1,a2]
b=point[b1,b2]
c=point[c1,c2]
r=point[d1,d2]

S and T may be defined as

s=lineslider[parline[r,ppline[a,b]],u]
t=intersectionpoint[parline[r,ppline[a,c]],parline[s,ppline[b,c]]]

and the conclusion reads as

con=isconcurrent[ppline[a,r],ppline[b,s],ppline[c,t]]

Desargue's theorem as theorem of linear type. Take points

a=point[u1,u2]
b=point[u3,u4]
c=point[u5,u6]
r=point[u7,u8]
s=point[u9,x1]
t=point[x2,x3]

The similarity of ABC and RST may be expressed through 3 (linear in the dependent variables) equations

polys={
	isparallel[ppline[r,s],ppline[a,b]]==0,
	isparallel[ppline[s,t],ppline[b,c]]==0,
	isparallel[ppline[r,t],ppline[a,c]]==0}

The conclusion reads as

con=isconcurrent[ppline[a,r],ppline[b,s],ppline[c,t]]

We prove it solving the polynomial conditions for the dependent variables and substitute the solution into the conclusion.

sol=Solve[polys,{x1,x2,x3}]

con/.sol//Together

The general theorem of Desargue states that for triangles ABC and RST with AB^RS, AC^RT and BC^ST collinear the lines AR, BS and CT pass through a common point (or are parallel). 
For a proof choose coordinates

a=point[0,0]
b=point[0,1]
c=point[u5,u6]
r=point[u7,u8]
s=point[u9,u1]
t=point[u2,x1]

The assumption and conclusion read as

con1=iscollinear[
	intersectionpoint[ppline[r,s],ppline[a,b]],
	intersectionpoint[ppline[s,t],ppline[b,c]],
	intersectionpoint[ppline[r,t],ppline[a,c]]]

con2=isconcurrent[ppline[a,r],ppline[b,s],ppline[c,t]]

Factor[Numerator[con1]]

We see immediately that con2 is a factor of the assumption polynomial. Note that the second factor is exactly

iscollinear[r, s, t]

i.e., the inverse of the theorem holds, too.

clearndg[];

Brocard points

Let ABC be a triangle. The circle through A,B tangent to AC, the circle through B,C tangent to AB and the circle through A,C tangent to BC pass through a common point, the Brocard point of the triangle.
For a proof choose a generic triangle

a=point[0,0]
b=point[1,0]
c=point[u1,u2]

and centers for the circles

m1 = point[x1, x2]
m2 = point[x3, x4]
m3 = point[x5, x6]
c1 = pccircle[m1, a]
c2 = pccircle[m2, b]
c3 = pccircle[m3, c]

These coordinates are determined by the conditions

polys={
	iscltangent[c1,ppline[a,c]]==0, 
	oncircle[b,c1]==0, 
	iscltangent[c2,ppline[a,b]]==0, 
	oncircle[c,c2]==0, 
	iscltangent[c3,ppline[b,c]]==0, 
	oncircle[a,c3]==0}

This is a non-linear system of equations, but yields a single (and rational) solution

vars={x1,x2,x3,x4,x5,x6,x7,x8,x9}

sol=Solve[polys,vars]

(Mathematica returns 9 times the same solution, only the first of which is considered)

sol=sol[[1]]

Let P be the intersection point of two of the circles

p=otherccpoint[b,c1/.sol,c2/.sol]

This point also belongs to the third circle

con=oncircle[p,c3/.sol]

clearndg[];

Simson's theorem

Let ABC a triangle and P a point on the circumcircle of ABC. Then the perpfoots from P onto the sides of the triangle (or their prolongations) are collinear.

Here is a constructive proof. Choose a circle and four points on its circumference

m=point[0,0]
a=point[u1,0]
b=circleslider[m,a,u2]
c=circleslider[m,a,u3]
p=circleslider[m,a,u4]

Then compute the coordinates of the pedal points

x=pedalpoint[p,ppline[a,b]];
y=pedalpoint[p,ppline[b,c]];
z=pedalpoint[p,ppline[a,c]];

and prove that they are collinear

iscollinear[x,y,z]

clearndg[];

A pure equational proof goes as follows. Take points A, B, C, P, X, Y, Z with independent and dependent coordinates

a=point[0,0]
b=point[1,0]
c=point[u1,u2]
p=point[u3,x1]
x=varpoint[a,b,x2] 
y=varpoint[b,c,x3]
z=varpoint[a,c,x4]

The dependent variables are related by the polynomial conditions

polys={
	isorthogonal[ppline[a,c],ppline[p,z]]==0,
	isorthogonal[ppline[b,c],ppline[p,y]]==0,
	isorthogonal[ppline[a,b],ppline[p,x]]==0,      			
	isconcyclic[a,b,c,p]==0}

and the conclusion is

con=iscollinear[x,y,z]

Solving the polynomial equations we get two solutions

vars={x2,x3,x4,x1}
sol=Solve[polys,vars]

con /. sol // Together

Let's prove the same result with a Groebner basis computations:

gb=gbasis[polys,vars]

normalf[con,gb,vars]

For the inverse theorem,  the polynomial conditions are

polys={
	isorthogonal[ppline[a,c],ppline[p,z]]==0,
	isorthogonal[ppline[b,c],ppline[p,y]]==0,
	isorthogonal[ppline[a,b],ppline[p,x]]==0,
    iscollinear[x,y,z]==0}

The conclusion is

con=isconcyclic[a,b,c,p]

Solving the polynomial equations we get again two solutions

sol = Solve[polys, vars]

con /. sol // Together

Here is an approach through Groebner bases

gb=gbasis[polys,vars]

normalf[con,gb,vars]

clearndg[];

The butterfly theorem

Let A, B, C, D be four points on a circle with center O. AC and BD intersect at P. The line through P perpendicular to OP intersects AD in E and BC in F. Then P is the midpoint of EF.

For an equational proof choose the following coordinates

p=point[0,0]
o=point[u1,0]
a=point[u2,u3]
b=point[u4,x1]
c=point[x2,x3]
d=point[x4,x5]
e=point[0,x6]
f=point[0,x7]
cc=pccircle[o,a]

Due to the special choice of the coordinate system EF is already perpendicular to OP and the dependent variables are related through the polynomials

polys={
	oncircle[b,cc]==0, 
	oncircle[c,cc]==0, 
	oncircle[d,cc]==0,
	online[p,ppline[a,c]]==0,
	online[p,ppline[b,d]]==0,
	online[e,ppline[a,d]]==0,
	online[f,ppline[b,c]]==0}

The conclusion may be formulated as

con=Numerator[sqrdist[p,midpoint[e,f]]]

Let's try to solve the polynomial system with Solve

vars={x6,x7,x5,x4,x2,x3,x1}
sol=Solve[polys,vars];

(long output suppressed; be patient or abort the computation) 

The solution contains degenerate components with B=D or A=C that should be removed

sol1 = 
        Select[sol, ! SameQ[sqrdist[a, c] /. # // Together, 
                0]  &];
sol2 = 
      Select[sol1, ! SameQ[sqrdist[b, d] /. # // Together, 
              0]  &]

con /. sol2 // Together

The Butterfly theorem may also be proved in a constructive way

o=point[0,0]
a=point[1,0]
b=circleslider[o,a,u1]
c=circleslider[o,a,u2]
d=circleslider[o,a,u3]

p=intersectionpoint[ppline[a,c],ppline[b,d]]

h=ortholine[p,ppline[o,p]]

e=intersectionpoint[h,ppline[a,d]]

f=intersectionpoint[h,ppline[b,c]]

con=sqrdist[p,midpoint[e,f]]

clearndg[];

Tangency of Feuerbach's circle

The Feuerbach circle has another interesting property; it is tangent to the in- and the excircles, i.e., to the four tangent circles of the triangle ABC. 

To prove this statement we choose the following coordinates

a=point[0,0]
b=point[2,0]
c=point[u1,u2]

m=intersectionpoint[pbisector[a,b],pbisector[b,c]]
h=intersectionpoint[altitude[a,b,c],altitude[b,c,a]]
n=midpoint[m,h]

fc=pccircle[n,midpoint[a,b]] (* Feuerbach's circle *)

This is Feuerbach's circle. Let P be the center of one of the tangent circles pc

p=point[x1,x2]
pc=pccircle[p,pedalpoint[p,ppline[a,b]]]

(hence  (Subscript[x, 2]) is the radius of the tangent circle). The coordinates of P are related by the polynomials

polys={
	onbisector[p,a,b,c]==0,
	onbisector[p,b,c,a]==0}

whereas the conclusion translates as

con=iscctangent[pc,fc]

The standard approach through Solve yields very complicated radical expressions that are usually hard to simplify. Let's apply Groebner bases instead

vars={x1,x2}
gb=gbasis[polys,vars]

normalf[con,gb,vars]

clearndg[];

Time used for evaluation

TimeUsed[]