|
|
%auto-ignore
#PLANE GEOMETRY: AN ELEMENTARY SCHOOL TEXTBOOK (ca. 2050 AD)
#By Shalosh B. Ekhad, XIV
##Downloaded from the Future by Doron Zeilberger (zeilberg@math.temple.edu)
#INTRODUCTION:
#Dear Children,
#Do you know that until fifty years ago most of mathematics was
#done by humans? Even more strangely, they used human language
#to state and prove mathematical theorems. Even when they started
#to use computers to prove theorems, they always translated the
#proof into the imprecise human language,because, ironically, computer-
#proofs were considered of questionable rigor!
##
##Only thirty years ago, when more and more mathematics was getting
#done by computer, people realized how silly it is to go back-and-forth
#from the precise programming-language to the imprecise humanese.
#At the historical ICM 2022, the IMS (International Math Standards)
#were introduced, and Maple was chosen the official language for mathematical
#communication. They also realized that once a theorem is stated precisely,
#in Maple, the proof-process can be started right away, by running the
#program-statement of the theorem.
##
#All the theorems that were known to our grandparents, and most of what they
#called conjectures, can now be proved in a few nano-seconds on any PC.
#As you probably known, computers have since discovered much deeper theorems
#for which we only have semi-rigorous proofs, since a complete proof would
#take too long.
##
#All the theorems in this textbook were automatically discovered (and
#of course proved) by computer. The discovery program started with 3
#generic points in the plane, and iteratively constructed new points, lines,
#and circles using a few primitives. Whenever a new point (or line, or circle,
#or whatever) coincided with an old one, a "theorem" was born. Then a search
#in Eric's Math Treasure Trove, version 1998, was performed, to see which of
#the theorems that were discovered by the Discovery Program were anticipated
#by humans, the program then automatically attached the human names
#to the theorems. Not surprisingly, all the theorems that turned out to
#be anticipated by humans, and that are presented in this very elementary
#textbook, were of very low complexity and depth.
#
##HOW TO USE THIS TEXTBOOK:
#
#You don't have to read it cover-to-cover. Pick any theorem
#in Part I, and then look up, in Part II, the definitions used in the
#statement-program of that theorem.
#These definitions, in turn, may involve other definitions, etc.
#Don't worry, none of the definitions are circular.
##
##Example: Look up Napoleon's Theorem. It involves two definitions:
#ItIsEqui and CET. Look up ItIsEqui. It involves DeSq. DeSq is
#primitive. Now look up CET. It uses Circumcenter. Circumcenter involves
#the primitive definitions Ce and Center. Hence to understand the statement
#of Napoleon's theorem you only need to look up the definitions: Ce, Center,
#CET, Circumcenter, DeSq and ItIsEqui, and get a completely self-contained
#statement of the so-called Napoleon theorem. To actually prove it, get into
#Maple by typing: "maple<CR>" (without the quotes), then, once inside maple,
#type: "read text;<CR>" (without the quotes), and then "Napoleon();<CR>"
#(without the quotes). You should immediately get the response of the
#computer: true.
##
##
##Note: A point is represented as a list of length 2. Lines are
##represented as a*x+b*y+c.
##WARNING: x and y are global variables!
###
###Note From the Downloader (DZ):
##IMPORTANT: THIS TEXTBOOK IS ALSO AVAILABLE ON-LINE AS A MAPLE PACKAGE
##CALLED "RENE", FROM http://www.math.temple.edu/~zeilberg/
##(click on "Maple programs and packages", then click on "RENE").
##This textbook was tested for Maple V, ver. 5 and previous versions.
##Unfortunately, every year or so, Maple comes out with a new version
##(bigger but not always better, and often buggier,)
##that is not fully compatible with code written for previous versions.
##The package RENE will be constantly updated to conform to future
##versions, but let's hope that Maple will start to become upward-compatible.
##RENE will also be continuously enlarged to include new proofs, in particular
##of Monthly problems and IMO problems (it already has a few now).
##########################Part I: THEOREMS############
AreaFormula:=proc() local A,B,C:
ItIsZero(DeSq(A,B)*DeSq(C,Ft(C,Le(A,B)))/4-AREA(A,B,C)^2):end:
Brianchon:=proc() local Li,t,i,c,d,P:
for i from 0 to 5 do Li[i]:=TangentToEllipse(c,d,t[i]): od:
for i from 0 to 5 do P[i]:=Pt(Li[i],Li[i+1 mod 6]): od:
Concurrent(Le(P[0],P[3]),Le(P[1],P[4]),Le(P[2],P[5])):end:
Butterfly:=proc() local P,t,i,R,Li,M,X,Y:for i from 1 to 4 do
P[i]:=ParamCircle([0,0],R,t[i]) od:M:=Pt(Le(P[1],P[3]),Le(P[2],P[4])):
Li:=PerpPQ([0,0],M):X:=Pt(Le(P[1],P[4]),Li):Y:=Pt(Le(P[2],P[3]),Li):
ItIsZero(DeSq(M,X)-DeSq(M,Y)):end:
CentroidExists:=proc() local A,B,C:
Concurrent(Le(MidPt(A,B),C),Le(MidPt(A,C),B),Le(MidPt(B,C),A)):end:
Ceva:=proc() local A,B,C,O,D,E,F: A:=[0,0]: B:=[1,0]:
D:=Pt(Le(B,C),Le(A,O)):E:=Pt(Le(A,C),Le(B,O)):F:=Pt(Le(A,B),Le(C,O)):ItIsZero(
DeSq(B,D)*DeSq(C,E)*DeSq(A,F)-DeSq(D,C)*DeSq(E,A)*DeSq(F,B)): end:
Desargues:=proc() local A,B,i,m,t,s: for i from 1 to 3 do
A[i]:=ParamLine(m[i],0,t[i]): B[i]:=ParamLine(m[i],0,s[i]):od:
Colinear(Pt(Le(A[1],A[2]),Le(B[1],B[2])),Pt(Le(A[1],A[3]),Le(B[1],B[3])),
Pt(Le(A[2],A[3]),Le(B[2],B[3]))):end:
EulerLineExists:=proc() local A,B,C:
Colinear(Orthocenter(A,B,C),Circumcenter(A,B,C),Centroid(A,B,C)):end:
EulerTetrahedronVolumeFormula:=proc() local P1,P2,P3,P4,P,Q,R,A,B,C,Vol,
p31,p32,p41,p42,p43: with(linalg):P1:=[0,0,0]: P2:=[1,0,0]:P3:=[p31,p32,0]:
P4:=[p41,p42,p43]:P:=DeSqG(P1,P4,3):Q:=DeSqG(P2,P4,3):R:=DeSqG(P3,P4,3):
A:=DeSqG(P2,P3,3):B:=DeSqG(P3,P1,3):C:=DeSqG(P1,P2,3):
Vol:=AREA([p31,p32],[1,0],[0,0])*p43/3:evalb(normal(det(array([[0,P,Q,R,1],
[P,0,C,B,1],[Q,C,0,A,1],[R,B,A,0,1],[1,1,1,1,0]]))/Vol^2/288)=1):end:
EulerTriangleFormula:=proc() local T,m,n,A,B,C,d,R,r,O,I1:
T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n):
I1:=Circumcenter(A,B,C):r:=Inradius(m,n):R:=Circumradius(A,B,C):
d:=sqrt(DeSq(O,I1)): ItIsZero((d^2-R^2)^2-4*r^2*R^2):end:
Feuerbach:=proc() local m,n:TouchCe(NinePointCircle(Te(m,n)),Incircle(m,n)):end:
FoxTalbot:=proc() local q,L,i,a,b,c,j,M: L[1]:=x: for i from 2 to 5 do L[i]:=
a[i]*x+b[i]*y+c[i]: od: for i from 1 to 5 do
q:=Quad(seq(L[j],j=1..i-1),seq(L[j],j=i+1..5)):M[i]:=Le(MidPt(q[1],q[3]),
MidPt(q[2],q[4])):od: Concurrent(seq(M[i],i=1..5)):end:
Herron:=proc() local q,a,b,c,s,A,B,C,b1,a2,b2,Area:A:=[0,0]:B:=[0,b1]:
C:=[a2,b2]:a:=sqrt(DeSq(B,C)):b:=sqrt(DeSq(A,C)):c:=sqrt(DeSq(A,B)):
s:=(a+b+c)/2: ItIsZero(AREA(A,B,C)^2-s*(s-a)*(s-b)*(s-c)):end:
IncenterExists:=proc() local m,n,A,B,C,T:T:=Te(m,n):A:=T[1]:B:=T[2]:
C:=T[3]:Concurrent(y-m*x,y+n*x-n,y-C[2]-(x-C[1])*TS(m,1/n)):end:
Johnson:=proc() local C,t,i,R,P: for i from 0 to 2 do C[i]:=ParamCircle(
[0,0],R,t[i]): od: for i from 0 to 2 do P[i]:=MirRefOf0(C[i],C[i+1 mod 3]) :
od: ItIsZero(Radius(Ce(P[0],P[1],P[2]))^2-R^2): end:
Lehmus:=proc() local N,M,m,n:N:=Pt(y-TS(m,m)*x,y+n*(x-1)):
M:=Pt(y-m*x,y+TS(n,n)*(x-1)):factor(DeSq([1,0],N)-DeSq([0,0],M)):end:
Menelaus:=proc() local A,B,C,X,Y,Z,L,m,b: L:=y-m*x-b: X:=Pt(Le(B,C),L):
Y:=Pt(Le(A,C),L):Z:=Pt(Le(A,B),L):ItIsZero(
DeSq(B,X)*DeSq(C,Y)*DeSq(A,Z)-DeSq(C,X)*DeSq(A,Y)*DeSq(B,Z)): end:
Morley:=proc() local m,n,A,B,C,D,E,F:A:=[0,0]:B:=[1,0]:
C:=Pt(y-TS(m,m,m)*x,y+TS(n,n,n)*(x-1)):D:=Pt(y-m*x,y+n*x-n):
E:=Pt(y-TS(m,m)*x,y-C[2]-(x-C[1])*TS(m,m,-n,sqrt(3))):
F:=Pt(y+TS(n,n)*(x-1),y-C[2]+(x-C[1])*TS(n,n,-m,sqrt(3))):ItIsEqui(D,E,F):end:
Napoleon:=proc() local A,B,C: ItIsEqui(CET(A,B),CET(B,C),CET(C,A)): end:
NinePointCircleExists:=proc() local A,B,C,O,D,E,F,G,H,I,K,L,M:
D:=Ft(A,Le(B,C)):E:=Ft(B,Le(A,C)):F:=Ft(C,Le(A,B)):
G:=MidPt(A,B):H:=MidPt(A,C):I:=MidPt(B,C):O:=Orthocenter(A,B,C):
K:=MidPt(O,A):L:=MidPt(O,B):M:=MidPt(O,C):Concyclic(D,E,F,G,H,I,K,L,M):end:
OrthocenterExists:=proc() local A,B,C:
Concurrent(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)),Altitude(C,Le(A,B))):end:
Pappus:=proc() local t,s,m,b,m1,b1,i,P,Q:
for i from 1 to 3 do P[i]:=ParamLine(m,b,t[i]): Q[i]:=ParamLine(m1,b1,s[i]): od:
Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])),Pt(Le(P[1],Q[3]),Le(P[3],Q[1])),
Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end:
Pascal:=proc() local c,d,s,t,i,P,Q: for i from 1 to 3 do P[i]:=ParEllipse(
c,d,t[i]):Q[i]:=ParEllipse(c,d,s[i]):od:Colinear(Pt(Le(P[1],Q[2]),Le(P[2],Q[1])),
Pt(Le(P[1],Q[3]),Le(P[3],Q[1])),Pt(Le(P[2],Q[3]),Le(P[3],Q[2]))):end:
Ptolemy:=proc() local P,i,t,R: for i from 1 to 4 do
P[i]:=ParamCircle([0,0],R,t[i]): od: Sqabc(DeSq(P[1],P[2])*DeSq(P[3],P[4]),
DeSq(P[2],P[3])*DeSq(P[4],P[1]),DeSq(P[1],P[3])*DeSq(P[2],P[4])):end:
Simson:=proc() local t,i,P,R:for i from 1 to 4 do
P[i]:=ParamCircle([0,0],R,t[i]): od: Colinear(Ft(P[4],Le(P[1],P[2])),
Ft(P[4],Le(P[2],P[3])),Ft(P[4],Le(P[3],P[1]))):end:
Soddy:=proc() local q,e1,e2,e3,e4,c,d,e,TC,R,r,s,t,p:with(grobner):
R:=1:TC:=TcCesOut:c:=[r+R,0]:q:=gbasis({TC(c,r,d,s),TC(c,r,e,t),TC(d,s,e,t),
TC([0,0],R,c,r),TC([0,0],R,d,s),TC([0,0],R,e,t)},[d[1],e[1],d[2],e[2],r,s,t],
tdeg):e4:=1/R:e1:=1/r:e2:=1/s:e3:=1/t:
p:=-2*(e1^2+e2^2+e3^2+e4^2)+(e1+e2+e3+e4)^2:p:=numer(normal(p)):
ItIsZero(normalf(p,q,[d[1],e[1],d[2],e[2],r,s,t],tdeg)):end:
########################PART II:DEFINITIONS##########################
#Def (The perpendicular to line Le1 that passes through point Pt1
Altitude:=proc(Pt1,Le1): expand(coeff(expand(Le1),x,1)*(y-Pt1[2])-
coeff(expand(Le1),y,1)*(x-Pt1[1])): end:
#Def(Area of triangle ABC)
AREA:=proc(A,B,C):normal(expand((B[1]*C[2]-B[2]*C[1]-A[1]*C[2]+A[2]*C[1]
-B[1]*A[2]+B[2]*A[1])/2)):end:
#Def (The Circumcircle of the inputed Points)
Ce:=proc() local eq,a,b,c,i,q:eq:=x^2+y^2+a*x+b*y+c:q:=solve({seq(subs(
{x=args[i][1],y=args[i][2]},eq),i=1..nargs)} ,{a,b,c}):expand(subs(q,eq)):end:
#Def(The Center of a Circle Circ)
Center:=proc(Circ):[-coeff(expand(Circ),x,1)/2,-coeff(expand(Circ),y,1)/2]:end:
#Def (The intersection of the three medians)
Centroid:=proc(A,B,C):Concurrency(Le(MidPt(A,B),C),Le(MidPt(A,C),B),
Le(MidPt(B,C),A)):end:
#Def(Circumcenter of the equilateral triangle two of whose vertices are A and B)
CET:=proc(A,B):Circumcenter(A, B, [(B[1]+A[1])/2-(A[2]-B[2])*3^(1/2)/2,
B[2]/2+(A[1]-B[1])*3^(1/2)/2+A[2]/2]):end:
#Def (The Circumcenter of the triangle ABC)
Circumcenter:=proc(A,B,C):Center(Ce(A,B,C)):end:
#Def (Circumradius of the triangle ABC)
Circumradius:=proc(A,B,C):Radius(Ce(A,B,C)):end:
#Def (The inputed points all on the same line?)
Colinear:=proc() local i:
if nargs<2 then ERROR(`Need at least two Pts`): fi: for i from 3 to nargs do
if AREA(args[1],args[2],args[i])<>0 then RETURN(false):fi:od:true:end:
#Def (The common point of the inputed lines)
Concurrency:=proc() local q: q:=solve({args},{x,y}):[subs(q,x),subs(q,y)]: end:
#Def (Are the inputed lines concurrent?)
Concurrent:=proc(): not evalb(solve({args},{x,y})=NULL): end:
#Def (Are the inputed points all on the same circle?)
Concyclic:=proc() local i,C1:C1:=Ce(args[1],args[2],args[3]):
for i from 4 to nargs do
if C1<>Ce(args[1],args[2],args[i]) then RETURN(false): fi: od: true: end:
#Def (Square of Distance of point P to line L)
DePtLeSq:=proc(P,L):DeSq(Pt(Altitude(P,L),L),P):end:
#Def (The square of the distance of points A and B)
DeSq:=proc(A,B):(A[1]-B[1])^2+(A[2]-B[2])^2: end:
#Def (The square of the distance of points A and B, in dim-dimensional space)
DeSqG:=proc(A,B,dim) local i :sum((A[i]-B[i])^2,i=1..dim): end:
#Def (The line through Circumcenter, Orthocenter, and Centroid)
EulerLine:=proc(A,B,C):Le(Orthocenter(A,B,C),Circumcenter(A,B,C)):end:
#Def (Projection of point Pt1 on line Le1)
Ft:=proc(Pt1,Le1) :Pt(Altitude(Pt1,Le1),Le1):end:
#Def(The incenter of the triangle whose vertices are A(0,0), B(1,0),
#and the slopes of AB and BC are TS(m,m),TS(n,n),resp.)
Incenter:=proc(m,n) local C: C:=Te(m,n)[3]: if m=n then [1/2,m/2] :else
Concurrency(y-m*x,y+n*x-n,y-C[2]-expand((x-C[1])*TS(m,1/n))) fi:end:
#Def: The eq. of the incircle through the standard triangle
Incircle:=proc(m,n) local C,R:R:=Inradius(m,n):C:=Incenter(m,n):
expand((x-C[1])^2+(y-C[2])^2-R^2):end:
#Def(The inradius of the standard triangle )
Inradius:=proc(m,n) local A,B,C,T,O:
T:=Te(m,n):A:=T[1]:B:=T[2]:C:=T[3]:O:=Incenter(m,n):sqrt(normal(
{DePtLeSq(O,Le(A,B)),DePtLeSq(O,Le(A,C)),DePtLeSq(O,Le(B,C))})[1]):end:
#Def(Is the triangle ABC equilateral?)
ItIsEqui:=proc(A,B,C):evalb(normal
({DeSq(A,B)-DeSq(A,C),DeSq(B,C)-DeSq(C,A)})={0}):end:
#Def(Is it zero?)
ItIsZero:=proc(a):evalb(normal(a)=0):end:
#Def (The eq. of the line joining A and B)
Le:=proc(A,B) AREA(A,B,[x,y]):end:
#Def (The midpoint between A and B)
MidPt:=proc(A,B):[(A[1]+B[1])/2,(A[2]+B[2])/2]:end:
#Def (Mirror reflection of the origin w.r.t. to the line AB)
MirRefOf0:=proc(A,B) local q: q:=Ft([0,0],Le(A,B)): [2*q[1],2*q[2]]:end:
#Def (Mirror reflection of the origin w.r.t. to the line AB)
MirRefPtLe:=proc(P,l) local q:
q:=Ft([0,0],subs({x=x+P[1],y=y+P[2]},l)): [2*q[1]+P[1],2*q[2]+P[2]]:end:
#Def (Euler's Nine-point circle for triangle ABC)
NinePointCircle:=proc(A,B,C): Ce(MidPt(A,B),MidPt(A,C),MidPt(B,C)):end:
#Def (The intersection of the three perpendicular projections)
Orthocenter:=proc(A,B,C):Concurrency(Altitude(A,Le(B,C)),Altitude(B,Le(A,C)),
Altitude(C,Le(A,B))):end:
#Def (Generic point on a Parametric circle center [c[1],c[2]] and radius R)
ParamCircle:=proc(c,R,t):[c[1]+R*(t+1/t)/2,c[2]+R*(t-1/t)/2/I]:end:
#Def (Generic point on a Parametric ellipse, center [c[1],c[2]])
ParEllipse:=proc(c,d,t):[c[1]+d[1]*(t+1/t)/2,c[2]+d[2]*(t-1/t)/2/I]:end:
#Def (Generic point on a parametric line)
ParamLine:=proc(m,b,t):[t,m*t+b]:end:
#Def(Line through Midpoint of PQ perpendicular to PQ)
PerpMid:=proc(P,Q):PerpPQ(P,MidPt(P,Q)):end:
#Def(Line through Q perpendicular to PQ)
PerpPQ:=proc(P,Q):expand((y-Q[2])*(P[2]-Q[2])+(x-Q[1])*(P[1]-Q[1])):end:
#Def (The point of intersection of lines Le1 and Le2)
Pt:=proc(Le1,Le2) local q:q:=solve(
{numer(normal(Le1)),numer(normal(Le2))},{x,y}):
[normal(simplify(subs(q,x))),normal(simplify(subs(q,y)))]:end:
#Def(Quadrilateral through four lines L1,L2,L3,L4)
Quad:=proc(L1,L2,L3,L4):Pt(L1,L2),Pt(L2,L3),Pt(L3,L4),Pt(L4,L1):end:
#Def(The Radius of a circle Circ)
Radius:=proc(Circ) local q:
q:=Center(Circ):sqrt(normal(subs({x=q[1],y=q[2]},-Circ))):end:
#Def (The slope of the line joining points A and B)
Slope:=proc(A,B):normal((B[2]-A[2])/(B[1]-A[1])):end:
#Def( Is it true that sqrt(a)+sqrt(b)=sqrt(c) ?)
Sqabc:=proc(a,b,c):ItIsZero((c-a-b)^2-4*a*b):end:
#Tangent(Ce1,Pt1): Given a circle Ce1, and a point Pt1
#on it, finds the equation of the tangent
Tangent:=proc(Ce1,Pt1) local A,x0,y0: A:=coeff(Ce1,x,2):x0:=Pt1[1]: y0:=Pt1[2]:
numer(normal((y-y0)*(2*A*y0+coeff(Ce1,y,1))+(x-x0)*(2*A*x0+coeff(Ce1,x,1)))):
end:
#Def(Tangent to the parametric ellipse at the parametric point
TangentToEllipse:=proc(c,d,t) local P: P:=ParEllipse(c,d,t):
diff(P[1],t)*(y-P[2])-(x-P[1])*diff(P[2],t):end:
#Def: The condition that two circles, with given centers and radii touch
TcCesOut:=
proc(C1,R1,C2,R2):expand((R1+R2)^2-(C1[1]-C2[1])^2-(C1[2]-C2[2])^2):end:
#Def(Standard Triangle whose vertices are A(0,0),B(1,0) and angles
#CAB and CAB are 2*arctan(m) and 2*arctan(-n) resp.
Te:=proc(m,n):[0,0],[1,0],Pt(y-TS(m,m)*x,y+TS(n,n)*(x-1)):end:
#Def(Given two circles C1,C2, decides whether they touch)
TouchCe:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)):
ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2):
end:
#Def(The expression whose vanishing guarantess that the symbolic
#circles touch)
TouchCe1:=proc(C1,C2) local gu: gu:=expand(subs(y=solve(C1-C2,y),C1)):
numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)):
end:
#Def(Given a circle C1, and a line L1, decides whether they touch)
TouchCeLe:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)):
ItIsZero(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2):
end:
#Def(The expression whose vanishing guarantess that the symbolic
#circle C1 and Line L1 touch)
TouchCeLe1:=proc(C1,L1) local gu: gu:=expand(subs(y=solve(L1,y),C1)):
numer(normal(4*coeff(gu,x,2)*coeff(gu,x,0)-coeff(gu,x,1)^2)):
end:
#Def:tan(a_1+a_2+...) expressed in terms li[1]:=tan(a_1), li[2]:=tan(a_2) ..
TS:=proc(li) local i,t:if nargs=1 then RETURN(args[1]) else
t:=TS(seq(args[i],i=2..nargs)): RETURN((args[1]+t)/(1-t*args[1])):fi:end:
|
|
