Check-ins Using Download Hex

Artifact c0350237e912d5d1d16cbc1473ffe03d666106698f3625d401b685186df1eb7b:

\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
REDUCE Historical
[ REDUCE Sourceforge Project | Historical SVN Repository | GitHub Mirror | SourceHut Mirror | NotABug Mirror | Chisel Mirror | Chisel RSS ]