\chapter[GEOMETRY: Plane geometry]%
{GEOMETRY: Mechanized (Plane) Geometry Manipulations}
\label{GEOMETRY}
\typeout{{GEOMETRY: Mechanized (Plane) Geometry Manipulations}}
\newcommand{\xxyy}[2] {\noindent{\f{#1}} \\\hspace*{1cm}
\parbox[t]{9cm}{#2} \\[6pt]}
\newcommand{\geo}{{\sc Geometry}}
\newenvironment{code}{\tt \begin{tabbing}
\hspace*{1cm}\=\hspace*{1cm}\=\hspace*{1cm}\=
\hspace*{1cm}\=\hspace*{1cm}\=\kill}{\end{tabbing}}
{\footnotesize
\begin{center}
Hans-Gert Gr\"abe \\
Universit\"at Leipzig, Germany \\
e-mail: graebe@informatik.uni-leipzig.de \\
\end{center}
}
\ttindex{GEOMETRY}
%\markboth{CHAPTER \ref{GEOMETRY}. GEOMETRY: (PLANE) GEOMETRY MANIPULATIONS}{}
%\thispagestyle{myheadings}
\section{Introduction}
This package provides tools for formulation and mechanized proofs of
geometry statements in the spirit of the ``Chinese Prover'' of
W.-T. Wu \cite{Wu:94} and the fundamental book \cite{Chou:88} of
S.-C. Chou who proved 512 geometry theorems with this mechanized
method, see also \cite{Chou:84}, \cite{Chou:90}, \cite{Wu:84a},
\cite{Wu:84b}.
The general idea behind this approach is an algebraic reformulation of
geometric conditions using generic coordinates. A (mathematically
strong) proof of the geometry statement then may be obtained from
appropriate manipulations of these algebraic expressions. A CAS as,
e.g., Reduce is well suited to mechanize these manipulations.
For a more detailed introduction to the topic see the accompanying
file {\tt geometry.tex} in \$REDUCEPATH/packages/geometry/.
\section{Basic Data Types and Constructors}
The basic data types in this package are {\tt Scalar, Point, Line, Circle1
and Circle}. \\
The function \f{POINT($a,b$)} creates a {\tt Point} in the plane with
the $(x,y)$-coordinates $(a,b)$.
A {\tt Line} is created with the function \f{LINE($a,b,c$)} and
fulfills the equation $ ax + by + c = 0$.
For circles there are two constructors. You can use
\f{CIRCLE($c_1,c_2,c_3,c_4$)} to create a {\tt Circle} where
the scalar variables solve the equation $c_1(x^2+y^2) + c_2x + c_3y + c_4 = 0$.
Note that lines are a subset of the circles with $c_1=0$. The other way
to create a {\tt Circle} is the function \f{CIRCLE1($M,s$)}.
The variable $M$ here denotes a {\tt Point} and $s$ the squared
radius. Please note that this package mostly uses the squared distances and
radiuses.
There are various functions whose return type is {\tt Scalar}.
Booleans are represented as extended booleans, i.e.\ the
procedure returns a {\tt Scalar} that is zero iff the condition is fulfilled.
For example, the function call \f{POINT\_ON\_CIRCLE(P,c)} returns zero if
the {\tt Point} $P$ is on the circle, otherwise $P$ is not on the circle.
In some cases also a non zero result has a geometric meaning. For example,
\f{COLLINEAR(A,B,C)} returns the signed area of the corresponding
parallelogram.
\section{Procedures}
This section contains a short description of all procedures available
in \geo. Per convention distances and radiuses of circles are squared.
\bigskip
\xxyy{ANGLE\_SUM(a,b:Scalar):Scalar \ttindex{ANGLE\_SUM}}
{Returns $\tan(\alpha+\beta)$, if $a=\tan(\alpha), b=\tan(\beta)$.}
\xxyy{ALTITUDE(A,B,C:Point):Line \ttindex{ALTITUDE}}
{The altitude from $A$ onto $g(BC)$. }
\xxyy{C1\_CIRCLE(M:Point,sqr:Scalar):Circle \ttindex{C1\_CIRCLE}}
{The circle with given center and sqradius.}
\xxyy{CC\_TANGENT(c1,c2:Circle):Scalar \ttindex{CC\_TANGENT}}
{Zero iff $c_1$ and $c_2$ are tangent.}
\xxyy{CHOOSE\_PC(M:Point,r,u):Point \ttindex{CHOOSE\_PC}}
{Chooses a point on the circle around $M$ with radius $r$ using its rational
parametrization with parameter $u$.}
\xxyy{CHOOSE\_PL(a:Line,u):Point \ttindex{CHOOSE\_PL}}
{Chooses a point on $a$ using parameter $u$.}
\xxyy{CIRCLE(c1,c2,c3,c4:Scalar):Circle \ttindex{CIRCLE}}
{The {\tt Circle} constructor.}
\xxyy{CIRCLE1(M:Point,sqr:Scalar):Circle1 \ttindex{CIRCLE1}}
{The {\tt Circle1} constructor. }
\xxyy{CIRCLE\_CENTER(c:Circle):Point \ttindex{CIRCLE\_CENTER}}
{The center of $c$.}
\xxyy{CIRCLE\_SQRADIUS(c:Circle):Scalar \ttindex{CIRCLE\_SQRADIUS}}
{The sqradius of $c$.}
\xxyy{CL\_TANGENT(c:Circle,l:Line):Scalar \ttindex{CL\_TANGENT}}
{Zero iff $l$ is tangent to $c$.}
\xxyy{COLLINEAR(A,B,C:Point):Scalar \ttindex{COLLINEAR}}
{Zero iff $A,B,C$ are on a common line. In general the signed area of the
parallelogram spanned by $\vec{AB}$ and $\vec{AC}$. }
\xxyy{CONCURRENT(a,b,c:Line):Scalar \ttindex{CONCURRENT}}
{Zero iff $a,b,c$ have a common point.}
\xxyy{INTERSECTION\_POINT(a,b:Line):Point \ttindex{INTERSECTION\_POINT}}
{The intersection point of the lines $a,b$. }
\xxyy{L2\_ANGLE(a,b:Line):Scalar \ttindex{L2\_ANGLE}}
{Tangens of the angle between $a$ and $b$. }
\xxyy{LINE(a,b,c:Scalar):Line \ttindex{LINE}}
{The {\tt Line} constructor.}
\xxyy{LOT(P:Point,a:Line):Line \ttindex{LOT}}
{The perpendicular from $P$ onto $a$.}
\xxyy{MEDIAN(A,B,C:Point):Line \ttindex{MEDIAN}}
{The median line from $A$ to $BC$.}
\xxyy{MIDPOINT(A,B:Point):Point \ttindex{MIDPOINT}}
{The midpoint of $AB$. }
\xxyy{MP(B,C:Point):Line \ttindex{MP}}
{The midpoint perpendicular of $BC$.}
\xxyy{ORTHOGONAL(a,b:Line):Scalar \ttindex{ORTHOGONAL}}
{zero iff the lines $a,b$ are orthogonal. }
\xxyy{OTHER\_CC\_POINT(P:Point,c1,c2:Circle):Point \ttindex{OTHER\_CC\_POINT}}
{ $c_1$ and $c_2$ intersect at $P$. The procedure returns the second
intersection point. }
\xxyy{OTHER\_CL\_POINT(P:Point,c:Circle,l:Line):Point \ttindex{OTHER\_CL\_POINT}}
{$c$ and $l$ intersect at $P$. The procedure returns the second intersection
point.}
\xxyy{P3\_ANGLE(A,B,C:Point):Scalar \ttindex{P3\_ANGLE}}
{Tangens of the angle between $\vec{BA}$ and $\vec{BC}$. }
\xxyy{P3\_CIRCLE(A,B,C:Point):Circle\ \ttindex{P3\_CIRCLE} {\rm or\ }\\
P3\_CIRCLE1(A,B,C:Point):Circle1\ttindex{P3\_CIRCLE1} }
{The circle through 3 given points. }
\xxyy{P4\_CIRCLE(A,B,C,D:Point):Scalar \ttindex{P4\_CIRCLE}}
{Zero iff four given points are on a common circle. }
\xxyy{PAR(P:Point,a:Line):Line \ttindex{PAR}}
{The line through $P$ parallel to $a$. }
\xxyy{PARALLEL(a,b:Line):Scalar \ttindex{PARALLEL}}
{Zero iff the lines $a,b$ are parallel. }
\xxyy{PEDALPOINT(P:Point,a:Line):Point \ttindex{PEDALPOINT}}
{The pedal point of the perpendicular from $P$ onto $a$.}
\xxyy{POINT(a,b:Scalar):Point \ttindex{POINT}}
{The {\tt Point} constructor.}
\xxyy{POINT\_ON\_BISECTOR(P,A,B,C:Point):Scalar \ttindex{POINT\_ON\_BISECTOR}}
{Zero iff $P$ is a point on the (inner or outer) bisector of the
angle $\angle\,ABC$.}
\xxyy{POINT\_ON\_CIRCLE(P:Point,c:Circle):Scalar\ \ttindex{POINT\_ON\_CIRCLE}
{\rm or\ }\\
POINT\_ON\_CIRCLE1(P:Point,c:Circle1):Scalar \ttindex{POINT\_ON\_CIRCLE1}}
{Zero iff $P$ is on the circle $c$.}
\xxyy{POINT\_ON\_LINE(P:Point,a:Line):Scalar \ttindex{POINT\_ON\_LINE}}
{Zero iff $P$ is on the line $a$. }
\xxyy{PP\_LINE(A,B:Point):Line \ttindex{PP\_LINE}}
{The line through $A$ and $B$.}
\xxyy{SQRDIST(A,B:Point):Scalar \ttindex{SQRDIST}}
{Square of the distance between $A$ and $B$.}
\xxyy{SYMPOINT(P:Point,l:Line):Point \ttindex{SYMPOINT}}
{The point symmetric to $P$ wrt.\ the line $l$.}
\xxyy{SYMLINE(a:Line,l:Line):Line \ttindex{SYMLINE}}
{The line symmetric to $a$ wrt.\ the line $l$.}
\xxyy{VARPOINT(A,B:Point,u):Point \ttindex{VARPOINT}}
{The point $D=u\cdot A+(1-u)\cdot B$. }
\noindent \geo \ supplies as additional tools the functions
\bigskip
\xxyy{EXTRACTMAT(polys,vars) \ttindex{EXTRACTMAT}}
{Returns the coefficient matrix of the list of equations $polys$ that are
linear in the variables $vars$. }
\xxyy{RED\_HOM\_COORDS(u:\{Line,Circle\}) \ttindex{RED\_HOM\_COORDS}}
{Returns the reduced homogeneous coordinates of $u$, i.e., divides out the
content. }
\newpage
\section{Examples}
\example
Create three points as the vertices of a generic triangle. \\
{\tt A:=Point(a1,a2); B:=Point(b1,b2); C:=Point(c1,c2);} \\
\noindent The midpoint perpendiculars of $\Delta\,ABC$ pass through
a common point since
\begin{code}\+\>
concurrent(mp(A,B),mp(B,C),mp(C,A));
\end{code}
simplifies to zero.
\medskip
\example
\noindent The intersection point of the midpoint perpendiculars
\begin{code}\+\>
M:=intersection\_point(mp(A,B),mp(B,C));
\end{code}
is the center of the circumscribed circle since
\begin{code}\+\>
sqrdist(M,A) - sqrdist(M,B);
\end{code}
simplifies to zero.
\medskip
\example
\noindent {\em Euler's line}:
\begin{quote}
The center $M$ of the circumscribed circle, the orthocenter $H$ and
the barycenter $S$ are collinear and $S$ divides $MH$ with ratio 1:2.
\end{quote}
Compute the coordinates of the corresponding points
\begin{code}\+\>
M:=intersection\_point(mp(a,b,c),mp(b,c,a));\\
H:=intersection\_point(altitude(a,b,c),altitude(b,c,a));\\
S:=intersection\_point(median(a,b,c),median(b,c,a));
\end{code}
and then prove that
\begin{code}\+\>
collinear(M,H,S);\\
sqrdist(S,varpoint(M,H,2/3));
\end{code}
both simplify to zero.
\medskip