1\documentclass{article} 2 3\title{\geo\ : A Small Package for Mechanized (Plane) Geometry 4Manipulations\\[20pt] Version 1.1} 5 6\author{Hans-Gert Gr\"abe, Univ. Leipzig, Germany} 7 8\date{September 7, 1998} 9 10\newenvironment{code}{\tt \begin{tabbing} 11\hspace*{1cm}\=\hspace*{1cm}\=\hspace*{1cm}\= 12\hspace*{1cm}\=\hspace*{1cm}\=\kill 13}{\end{tabbing}} 14\newcommand{\formel}[1]{\[\begin{array}{l} #1\end{array}\]} 15\newcommand{\iks}{{\bf x}} 16\newcommand{\uhh}{{\bf u}} 17\newcommand{\vau}{{\bf v}} 18\newcommand{\geo}{{\sc Geometry}} 19\newcommand{\gr}{{Gr\"obner}} 20\newcommand{\xxyy}[2] {\noindent{\tt #1} \\\hspace*{1cm} 21\parbox[t]{9cm}{#2} \\[6pt]} 22 23\begin{document} 24 25\maketitle 26 27\section{Introduction} 28 29Geometry is not only a part of mathematics with ancient roots but also 30a vivid area of modern research. Especially the field of geometry, 31called by some negligence ``elementary'', continues to attract the 32attention also of the great community of leisure mathematicians. This 33is probably due to the small set of prerequisites necessary to 34formulate the problems posed in this area and the erudition and non 35formal approaches ubiquitously needed to solve them. Examples from 36this area are also an indispensable component of high school 37mathematical competitions of different levels upto the International 38Mathematics Olympiad (IMO) \cite{IMO}. 39\medskip 40 41The great range of ideas involved in elementary geometry theorem 42proving inspired mathematicians to search for a common toolbox that 43allows to discover such geometric statements or, at least, to prove 44them in a more unified way. These attempts again may be traced back 45until ancient times, e.g., to Euclid and his axiomatic approach to 46geometry. 47 48Axiomatic approaches are mainly directed towards the introduction of 49coordinates that allow to quantify geometric statements and to use the 50full power of algebraic and even analytic arguments to prove geometry 51theorems. Different ways of axiomatization lead to different, even 52non-commutative, {\em rings of scalars}, the basic domain of 53coordinate values, see \cite{Wu:94}. 54 55Taking rational, real or even complex coordinates for granted (as we 56will do in the following) it turns out that geometry theorems may be 57classified due to their symmetry group as statements in, e.g., 58projective, affine or Euclidean (Cartesian) geometry. Below such a 59distinction will be important for the freedom to choose appropriate 60coordinate systems. 61\medskip 62 63It may be surprising that tedious but mostly straightforward 64manipulations of the algebraic counterparts of geometric statements 65allow to prove many theorems in geometry with even ingenious ``true 66geometric'' proofs. With the help of a Computer Algebra System 67supporting algebraic manipulations this approach obtains new power. 68The method is not automatic, since one often needs a good feeling how 69to encode a problem efficiently, but mechanized in the sense that one 70can develop a tool box to support this encoding and some very standard 71tools to derive a (mathematically strong~!) proof from these encoded 72data. 73 74The attempts to algorithmize this part of mathematics found their 75culmination in the 80's in the work of W.-T. Wu \cite{Wu:94} on ``the 76Chinese Prover'' and the fundamental book \cite{Chou:88} of S.-C. Chou 77who proved 512 geometry theorems with this mechanized method, see also 78\cite{Chou:84}, \cite{Chou:90}, \cite{Wu:84a}, \cite{Wu:84b}. 79 80Since the geometric interpretation of algebraic expressions depends 81heavily on the properties of the field of scalars, we get another 82classification of geometry theorems: Those with coordinate version 83valid over the algebraically closed field ${\bf C}$ and those with 84coordinate version valid (or may be even formulated) only over ${\bf 85R}$. The latter statements include {\em ordered geometry}, that uses 86the distinction between ``inside'' and ``outside'', since ${\bf C}$ 87doesn't admit monotone orderings. 88\medskip 89 90This package \geo, written in the algebraic mode of Reduce, should 91provide the casual user with a couple of procedures that allow him/her 92to mechanize his/her own geometry proofs. Together with the Reduce 93built-in simplifier for rational functions, the {\tt solve} function, 94and the \gr\ utilities\footnote{Unfortunately, the built in \gr\ 95package of Reduce doesn't admit enough flexibility for our purposes.} 96of the author's package CALI \cite{CALI} (part of the Reduce library) 97it allows for proving a wide range of theorems of unordered geometry, 98see the examples below and in the test file {\tt geometry.tst}. 99 100This package grew up from a course of lectures for students of 101computer science on this topic held by the author at the Univ. of 102Leipzig in fall 1996 and was updated after a similar lecture in spring 1031998. 104 105\section{Mechanizing Geometry Proving} 106 107Most geometric statements are of the following form: 108\begin{quote} 109Given certain (more or less) arbitrarily chosen points and/or lines we 110construct certain derived points and lines from them. Then the 111(relative) position of these geometric objects is of a certain 112specific kind regardless of the (absolute) position of the chosen 113data. 114\end{quote} 115 116To obtain evidence for such a statement (recommended before attempting 117to prove it~!) one makes usually one or several drawings, choosing the 118independent data appropriately and constructing the dependent ones out 119of them (best with ruler and compass, if possible). A computer may be 120helpful in such a task, since the constructions are purely algorithmic 121and computers are best suited for algorithmic tasks. Given appropriate 122data structures such construction steps may be encoded into {\em 123functions} that afterwards need only to be called with appropriate 124parameters. 125 126Even more general statements may be transformed into such a form and 127must be transformed to create drawings. This may sometimes involve 128constructions that can't be executed with ruler and compass as, e.g., 129angle trisection in Morley's theorem or construction of a conic in 130Pascal's theorem. 131 132\subsection{Algorithmization of (plane) geometry} 133 134The representation of geometric objects through coordinates is best 135suited for both compact (finite) data encoding and regeometrization of 136derived objects, e.g., through graphic output. Note that the target 137language for realization of these ideas on a computer can be almost 138every computer language and is not restricted to those supporting 139symbolic computations. Different geometric objects may be collected 140into a {\em scene}. Rapid graphic output of such a scene with 141different parameters may be collected into animations or even 142interactive drag-and-move pictures if supported by the programming 143system. (All this is not (yet) supported by \geo.) 144\medskip 145 146We will demonstrate this approach on geometric objects, containing 147points and lines, represented as pairs {\tt P:Point=$(p_{1},p_{2})$} 148or tripels {\tt g:Line=$(g_{1}, g_{2}, g_{3})$} of a certain basic 149type {\tt Scalar}, e.g., floating point reals. Here $g$ represents the 150homogeneous coordinates of the line $\{(x,y)\, :\, g_{1}x + g_{2}y + 151g_{3}=0\}$. In this setting geometric constructions may be understood 152as functions constructing new geometric objects from given ones. 153Implementing such functions variables occur in a natural way as formal 154parameters that are assigned with special values of the correct type 155during execution. 156\medskip 157 1581) For example, the equation 159\[(x-p_{1})(q_{2}-p_{2}) - (y-p_{2})(q_{1}-p_{1})=0\] 160 of the line through two given points $P=(p_{1},p_{2}),\, 161Q=(q_{1},q_{2})$ yields the function 162\begin{code} 163pp\_line(P,Q:Point):Line == 164 $(q_{2}-p_{2},p_{1}-q_{1},p_{2}q_{1}-p_{1}q_{2})$ 165\end{code} 166that returns the (representation of the) line through these two 167points. In this function $P$ and $Q$ are neither special nor general 168points but formal parameters of type {\tt Point}. 169 1702) The (coordinates of the) intersection point of two lines may be 171computed solving the corresponding system of linear equations. We get 172a partially defined function, since there is no or a not uniquely 173defined intersection point, if the two lines are parallel. In this 174case our function terminates with an error message. 175\begin{code} 176intersection\_point(a,b:Line):Point == \+\\ 177d:=$a_{1}b_{2}-a_{2}b_{1}$;\\ 178if $d=0$ then error ``Lines are parallel''\\ 179else return $((a_{2}b_{3}-a_{3}b_{2})/d,(a_{3}b_{1}-a_{1}b_{3})/d)$ 180\end{code} 181Again $a$ and $b$ are formal parameters, here of the type {\tt Line}. 182 1833) In the same way we may define a line $l$ through a given point $P$ 184perpendicular to a second line $a$ as 185\begin{code} 186lot(P:Point,a:Line):Line == $(a_{2},-a_{1},a_{1}p_{2}-a_{2}p_{1})$ 187\end{code} 188and a line through $P$ parallel to $a$ as 189\begin{code} 190par(P:Point,a:Line):Line == $(a_{1},a_{2},-a_{1}p_{1}-a_{2}p_{2})$ 191\end{code} 192 1934) All functions so far returned objects with coordinates being 194rational expressions in the input parameters, thus especially well 195suited for algebraic manipulations. To keep this nice property we 196introduce only the {\em squared Euclidean distance} 197\begin{code} 198sqrdist(P,Q:Point):Scalar == $(p_{1}-q_{1})^{2}+(p_{2}-q_{2})^{2}$ 199\end{code} 200 2015) Due to the relative nature of geometric statements some of the 202points and lines may be chosen arbitrarily or with certain 203restrictions. Hence we need appropriate constructors for points and 204lines given by their coordinates 205\begin{code} 206Point(a,b:Scalar):Point == $(a,b)$\\ 207Line(a,b,c::Scalar):Line == $(a,b,c)$ 208\end{code} 209and also for a point on a given line. For this purpose we provide two 210different functions 211\begin{code} 212choose\_Point(a:Line,u:Scalar):Point == \+\\ 213if $a_{2}=0$ then\+\\ 214if $a_{1}=0$ then error ``a is not a line''\\ 215else return $(-a_{3}/a_{1},u)$\-\\ 216else return $(u,-(a_{3}+a_1\,u)/a_{2})$ 217\end{code} 218that chooses a point on a line $a$ and 219\begin{code} 220varPoint(P,Q:Point,u:Scalar):Point == 221$(u\,a_{1}+(1-u)\,b_{1},u\,a_{2}+(1-u)\,b_{2})$ 222\end{code} 223that chooses a point on the line through two given points. The main 224reason to have also the second definition is that $u$ has a well 225defined geometric meaning in this case. For example, the midpoint of 226$PQ$ corresponds to $u={1\over 2}$: 227\begin{code} 228midPoint(P,Q:Point):Point == varPoint(P,Q,1/2) 229\end{code} 230 2316) One can compose these functions to get more complicated geometric 232objects as, e.g., the pedal point of a perpendicular 233\begin{code} 234pedalPoint(P:Point,a:Line):Point == intersection\_point(lot(P,a),a), 235\end{code} 236the midpoint perpendicular of $BC$ 237\begin{code} 238mp(B,C:Point):Line == lot(midPoint(B,C),line(B,C)), 239\end{code} 240the altitude to $BC$ in the triangle $\Delta\,ABC$ 241\begin{code} 242altitude(A,B,C:Point):Line == lot(A,line(B,C)) 243\end{code} 244and the median line 245\begin{code} 246median(A,B,C:Point):Line == line(A,midPoint(B,C)) 247\end{code} 248 2497) We can also test geometric conditions to be fulfilled, e.g., whether 250two lines $a$ and $b$ are parallel or orthogonal 251\begin{code} 252parallel(a,b:Line):Boolean == $(a_{1}b_{2}-a_{2}b_{1}=0)$ 253\end{code} 254resp. 255\begin{code} 256orthogonal(a,b:Line):Boolean == $(a_{1}b_{1}+a_{2}b_{2}=0)$ 257\end{code} 258or whether a given point is on a given line 259\begin{code} 260point\_on\_line(P:Point,a:Line):Boolean == 261$(a_{1}p_{1}+a_{2}p_{2}+a_{3}=0)$ 262\end{code} 263The corresponding procedures implemented in the package return the 264value of the expression to be equated to zero instead of a boolean. 265 266Even more complicated conditions may be checked as, e.g., whether 267three lines have a point in common or whether three points are on a 268common line. For a complete collection of the available procedures we 269refer to the section \ref{description}. 270\medskip 271 272Note that due to the linearity of points and lines all procedures 273considered so far return data with coordinates that are rational in 274the input parameters. One can easily enlarge the ideas presented in 275this section to handle also non linear objects as circles and angles, 276compute intersection points of circles, tangent lines etc., if the 277basic domain {\tt Scalar} admits to solve non-linear (mainly 278quadratic) equations. Since non-linear equations usually have more 279than one solution, branching ideas should be incorporated, too. For 280example, intersecting a circle and a line the program should consider 281both intersection points. 282 283\subsection{Mechanized evidence of geometric statements} 284 285With a computer and these prerequisites at hand one may obtain 286evidence of geometric statements not only from plots but also 287computationally, converting the statement to be checked into a 288function depending on the variable coordinates as parameters and 289plugging in different values for them. 290 291For example, the following function tests whether the three midpoint 292perpendiculars in a triangle given by the coordinates of its vertices 293$A,B,C$ pass through a common point 294\begin{code} 295test(A,B,C:Point):Boolean ==\\\>\>\> 296concurrent(mp(A,B,C),mp(B,C,A),mp(C,A,B)) 297\end{code} 298Plugging in different values for $A,B,C$ we can verify the theorem for 299many different special geometric configurations. Of course this is 300not yet a {\bf proof}. 301\medskip 302 303Lets add another remark: {\tt Point} and {\tt Line} are not only the 304basic data types of our geometry, but data type functions parametrized 305by the data type {\tt Scalar}. To have the full functionality of our 306procedures {\tt Scalar} must be a field with effective zero test. 307 308\section{Geometry Theorems of Constructive Type} 309 310Implementing the functions described above in a system, that admits 311also symbolic computations, we can execute the same computations also 312with symbolic values, i.e. taking a pure transcendental extension of 313${\bf Q}$ as scalars. The procedures then return (simplified) symbolic 314expressions that specialize under (almost all) substitutions of 315``real'' values for these symbolic ones to the same values as if they 316were computed by the original procedures with the specialized input. 317This leads to the notion of {\em generic geometric configurations}. A 318geometric statement holds in this generic configuration, i.e., the 319corresponding symbolic expression simplifies to zero, if and only if 320it is ``generically true'', i.e., holds for all special coordinate 321values except degenerate ones. 322 323\subsection{Geometric configurations of constructive type} 324 325This approach is especially powerful, if all geometric objects 326involved into a configuration may be constructed step by step and have 327{\em rational} expressions in the algebraically independent variables 328as symbolic coordinates. 329\medskip 330 331{\sc Definition: } We say that a geometric configuration is of {\em 332constructive type}\footnote{This notion is different from 333\cite{Chou:88}.}, if its generic configuration may be constructed step 334by step in such a way, that the coordinates of each successive 335geometric object may be expressed as rational functions of the 336coordinates of objects already available or algebraically independent 337variables, and the conclusion may be expressed as vanishing of a 338rational function in the coordinates of the available geometric 339objects. 340\medskip 341 342Substituting the corresponding rational expressions of the coordinates 343of the involved geometric objects into the coordinate slots of newly 344constructed objects and finally into the conclusion expression, we 345obtain successively rational expressions in the given algebraically 346independent variables. 347\begin{quote}\it 348A geometry theorem of constructive type is generically true if and 349only if (its configuration is not contradictory and) the conclusion 350expression simplifies to zero. 351\end{quote} 352 353Indeed, if this expression simplifies to zero, the algebraic version 354of the theorem will be satisfied for all ``admissible'' values of the 355parameters. If the expression doesn't simplify to zero, the theorem 356fails for almost all such parameters. 357 358Note that due to cancelation of denominators the domain of definition 359of the simplified expression may be greater than the (common) domain 360of definition of the different parts of the unsimplified 361expression. The correct non degeneracy conditions describing 362``admissibility'' may be collected during the computation. Collecting 363up the zero expression indicates, that the geometric configuration is 364contradictory. Hence the statement, that a certain geometric 365configuration of constructive type is contradictory, is of 366constructive type, too. 367 368The package \geo\ provides procedures {\tt clear\_ndg(), print\_ndg()} 369to manage and print these non degeneracy conditions and also a 370procedure {\tt add\_ndg(d)} as a hook for their user driven 371management. 372 373\subsection{Some one line proofs} 374 375Take independent variables $a_1,a_2,b_1,b_2,c_1,c_2$ and 376\begin{code} 377A:=Point(a1,a2);\ B:=Point(b1,b2);\ C:=Point(c1,c2); 378\end{code} 379as the vertices of a generic triangle. We can prove the following 380geometric statements about triangles computing the corresponding 381(compound) symbolic expressions and proving that they simplify to 382zero. Note that Reduce does simplification automatically. 383\medskip 384 385\noindent 1) The midpoint perpendiculars of $\Delta\,ABC$ pass through 386a common point since 387\begin{code}\+\> 388concurrent(mp(A,B),mp(B,C),mp(C,A)); 389\end{code} 390simplifies to zero. 391\medskip 392 393\noindent 2) The intersection point of the midpoint perpendiculars 394\begin{code}\+\> 395M:=intersection\_point(mp(A,B),mp(B,C)); 396\end{code} 397is the center of the circumscribed circle since 398\begin{code}\+\> 399sqrdist(M,A) - sqrdist(M,B); 400\end{code} 401simplifies to zero. 402\medskip 403 404\noindent 3) {\em Euler's line}: 405\begin{quote} 406The center $M$ of the circumscribed circle, the orthocenter $H$ and 407the barycenter $S$ are collinear and $S$ divides $MH$ with ratio 1:2. 408\end{quote} 409Compute the coordinates of the corresponding points 410\begin{code}\+\> 411M:=intersection\_point(mp(a,b,c),mp(b,c,a));\\ 412H:=intersection\_point(altitude(a,b,c),altitude(b,c,a));\\ 413S:=intersection\_point(median(a,b,c),median(b,c,a)); 414\end{code} 415and then prove that 416\begin{code}\+\> 417 collinear(M,H,S);\\ 418 sqrdist(S,varpoint(M,H,2/3)); 419\end{code} 420both simplify to zero. 421\medskip 422 423\noindent 4) {\em Feuerbach's circle}: 424\begin{quote} 425The midpoint $N$ of $MH$ is the center of a circle that passes through 426nine special points, the three pedal points of the altitudes, the 427midpoints of the sides of the triangle and the midpoints of the upper 428parts of the three altitudes. 429\end{quote} 430\begin{code}\+\> 431 N:=midpoint(M,H);\\[8pt] 432 433 sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(B,C));\\ 434 sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(H,C));\\[8pt] 435 436 D:=intersection\_point(pp\_line(A,B),pp\_line(H,C));\\ 437 sqrdist(N,midpoint(A,B))-sqrdist(N,D); 438\end{code} 439Again the last expression simplifies to zero thus proving the theorem. 440 441\section{Non-linear Geometric Objects} 442 443\geo\ provides several functions to handle angles and circles as 444non-linear geometric objects. 445 446\subsection{Angles and bisectors} 447 448(Oriented) angles between two given lines are presented as tangens of 449the difference of the corresponding slopes. Since 450\[\tan(\alpha-\beta) = \frac{\tan(\alpha)-\tan(\beta)}{1+ 451\tan(\alpha)\, \tan(\beta)}\] 452we get for the angle between two lines $g,h$ 453\begin{code}\> 454l2\_angle(g,h:Line):Scalar == $\frac{g_2h_1-g_1h_2}{g_1h_1+g_2h_2}$ 455\end{code} 456 457Note that in unordered geometry we can't distinguish between inner and 458outer angles. Hence we cannot describe (rationally) the parameters of 459the angle bisector of a triangle. For a point $P$ the equation 460\begin{code}\> 461l2\_angle(pp\_line(A,B),pp\_line(P,B)) =\\\>\>\> 462 l2\_angle(pp\_line(P,B),pp\_line(C,B)) 463\end{code} 464i.e., $\angle\,ABP=\angle\,PBC$, describes the condition to be located 465on either the inner or outer bisector of $\angle\,ABC$. Clearing 466denominators yields a procedure 467\begin{code}\> 468point\_on\_bisector(P,A,B,C) 469\end{code} 470that returns on generic input a polynomial of (total) degree 4 and 471quadratic in the coordinates of $P$ that describes the condition for 472$P$ to be on (either the inner or the outer) bisector of 473$\angle\,ABC$. 474\medskip 475 476With some more effort one can also employ such indirect geometric 477descriptions. For example, we can prove the following unordered 478version of the bisector intersection theorem. 479\medskip 480 481\noindent 5) There are four common points on the three bisector pairs 482of a given triangle $\Delta\,ABC$. Indeed, due to Cartesian symmetry 483we may choose a special coordinate system with origin $A$ and (after 484scaling) $x$-axes unit point $B$. The remaining point $C$ is 485arbitrary. Then the corresponding generic geometric configuration is 486described with two independent parameters $u_1,u_2$ -- the coordinates 487of $C$: 488\begin{code}\> 489A:=Point(0,0); B:=Point(1,0); C:=Point(u1,u2); 490\end{code} 491A point {\tt P:=Point(x1,x2)} is an intersection point of three 492bisectors iff it is a common zero of the polynomial system 493\begin{code} 494polys:=\{\>\>\+\+ point\_on\_bisector(P,A,B,C),\\ 495point\_on\_bisector(P,B,C,A),\\ 496point\_on\_bisector(P,C,A,B)\}, 497\end{code} 498i.e., of the polynomial system 499\begin{quote} 500$\hspace*{-2ex}\{\ {x_1}^{2}\,u_2 -2\,x_1\,x_2\,u_1 +2\,x_1\,x_2 501-2\,x_1\,u_2 -{x_2}^{2}\,u_2 +2\,x_2\,u_1 -2 \,x_2 +u_2,\\ 5022\,{x_1}^{2}\,u_1\,u_2 -{x_1}^{2}\,u_2 -2\,x_1\,x_2\,{u_1}^{2} 503+2\,x_1\,x_2\,u_1 +2\,x_1\,x_2\,{u_2}^{2} -2\,x_1\,{u_1}^{2}\,u_2 504-2\,x_1\,{u_2}^{3} -2\,{x_2}^{2}\,u_1\, u_2 +{x_2}^{2}\,u_2 505+2\,x_2\,{u_1}^{3} -2\,x_2\,{u_1}^{2} +2\,x_2\,u_1\,{u_2}^{2} -2\,x_2 506\,{u_2}^{2} +{u_1}^{2}\,u_2 +{u_2}^{3},\\ {x_1}^{2}\,u_2 507-2\,x_1\,x_2\,u_1 -{x_2}^{2}\,u_2\}$ 508\end{quote} 509with indeterminates $x_1,x_2$ over the coefficient field ${\bf 510Q}(u_1,u_2)$. A \gr\ basis computation with CALI 511\begin{code}\>\+ 512load cali;\\ 513setring(\{$x_1,x_2$\},\{\},lex);\\ 514setideal(polys,polys);\\ 515gbasis polys; 516\end{code} 517yields the following equivalent system: 518\begin{quote} 519$\hspace*{-2ex}\{\ 4\,{x_2}^{4}\,u_2 -8\,{x_2}^{3}\,{u_1}^{2} 520+8\,{x_2}^{3}\,u_1 -8\,{x_2}^{3}\,{u_2}^{2 } 521+4\,{x_2}^{2}\,{u_1}^{2}\,u_2 -4\,{x_2}^{2}\,u_1\,u_2 522+4\,{x_2}^{2}\,{u_2}^{3} -4\,{ x_2}^{2}\,u_2 +4\,x_2\,{u_2}^{2} 523-{u_2}^{3},\\ 2\,x_1\,u_1\,{u_2}^{2} -x_1\,{u_2}^{2} +2\,{ 524x_2}^{3}\,u_2 -4\,{x_2}^{2}\,{u_1}^{2} +4\,{x_2}^{2}\,u_1 525-2\,{x_2}^{2}\,{u_2}^{2} -2\, x_2\,{u_1}^{2}\,u_2 +2\,x_2\,u_1\,u_2 526-2\,x_2\,u_2 -u_1\,{u_2}^{2} +{u_2}^{2}\} $ 527\end{quote} 528The first equation has 4 solutions in $x_2$ and each of them may be 529completed with a single value for $x_1$ determined from the second 530equation. Hence the system $polys$ has four generic solutions 531corresponding to the four expected intersection points. The solutions 532have algebraic coordinates of degree 4 over the generic field of 533scalars ${\bf Q}(u_1,u_2)$ and specialize to the correct ``special'' 534intersection points for almost all values for the parameters $u_1$ and 535$u_2$. 536 537Although it is hard to give an explicit description through radicals 538of these symbolic values, one can compute with them knowing their 539minimal polynomials. Since in this situation $x_2$ is the distance 540from $P$ to the line $AB$, we can prove that each of the four points 541has equal distance to each of the 3 lines through two vertices of 542$\Delta\,ABC$, i.e., that these points are the centers of its incircle 543and the three excircles. First we compute the differences of the 544corresponding squared distances 545\begin{code}\>\+ 546con1:=sqrdist(P,pedalpoint(p,pp\_line(A,C)))-x2\^{}2;\\ 547con2:=sqrdist(p,pedalpoint(p,pp\_line(B,C)))-x2\^{}2; 548\end{code} 549The numerator of each of these two expressions should simplify to zero 550under the special algebraic values of $x_1,x_2$. This may be verified 551computing their normal forms with respect to the above \gr\ basis: 552\begin{code}\>\+ 553con1 mod gbasis polys;\\ 554con2 mod gbasis polys; 555\end{code} 556Note that \cite{Wu:94} proposes also a constructive proof for the 557bisector intersection theorem: 558 559Start with $A,B$ and the intersection point $P$ of the bisectors 560through $A$ and $B$. Then $g(AC)$ and $g(BC)$ are symmetric to $g(AB)$ 561wrt.\ $g(AP)$ and $g(BP)$ and $P$ must be on their bisector: 562\begin{code}\>\+ 563A:=Point(0,0); B:=Point(1,0); P:=Point(u1,u2);\\ 564l1:=pp\_line(A,B);\\ 565l2:=symline(l1,pp\_line(A,P));\\ 566l3:=symline(l1,pp\_line(B,P));\\[6pt] 567 568point\_on\_bisector(P,A,B,intersection\_point(l2,l3)); 569\end{code} 570As desired the last expression simplifies to zero. 571 572 573\subsection{Circles} 574 575The package \geo\ supplies two different types for encoding circles. 576The first type is {\tt Circle1} that stores the pair $(M,s)$, the 577center and the squared radius of the circle. The implementation of 578{\tt point\_on\_circle1(P,c)} and \linebreak {\tt p3\_circle1(A,B,C)} 579is almost straightforward. The latter function finds the circle 580through 3 given points, computing its center as the intersection point 581of two midpoint perpendiculars. 582 583For purposes of analytic geometry it is often better to work with the 584representation {\tt Circle} derived from the description of the circle 585as the set of points $(x,y)$ for which the expression 586\[(x-m_1)^2+(y-m_2)^2-r^2 = (x^2+y^2) -2\,m_1\,x -2\,m_2\,y 587+m_1^2+m_2^2-r^2 \] 588vanishes. We use homogeneous coordinates {\tt k:Circle} 589$=(k_1,k_2,k_3,k_4)$ for the circle 590\[k:=\{\,(x,y)\ :\ k_1*(x^2+y^2)+k_2*x+k_3*y+k_4 = 0\}\] 591since they admit denominator free computations and include also lines 592as special circles with infinite radius: The line $g=(g_1,g_2,g_3)$ is 593the circle $(0,g_1,g_2,g_3)$. 594 595Its easy to derive formulas {\tt circle\_center(k)} for the center of 596the circle $k$ and {\tt circle\_sqradius(k)} for its squared radius. 597It is also straightforward to test {\tt point\_on\_circle(P,k)}. The 598parameters of the circle {\tt p3\_circle(A,B,C)} through 3 given 599points 600\begin{code}\> 601A:=Point($a_1,a_2$); B:=Point($b_1,b_2$); C=Point($c_1,c_2$); 602\end{code} 603may be obtained from a nontrivial solution of the corresponding 604homogeneous linear system with coefficient matrix 605\[\left(\begin{array}{cccc} 606a_1^2+a_2^2 & a_1 & a_2 & 1 \\ b_1^2+b_2^2 & b_1 & b_2 & 1 \\ 607c_1^2+c_2^2 & c_1 & c_2 & 1 \\ 608\end{array}\right) 609\] 610The condition that 4 points are on a common circle then may be 611expressed as 612\begin{code}\> 613p4\_circle(A,B,C,D) == point\_on\_circle(D,p3\_circle(A,B,C)); 614\end{code} 615For generic points $A,B,C,D$ this yields a polynomial $p_4$ of degree 6164 in their coordinates. 617 618Note that this condition is equivalent to the circular angle theorem: 619For generic points $A,B,C,D$ 620\begin{code}\+\> 621 u:=angle(pp\_line(A,D),pp\_line(B,D));\\ 622 v:=angle(pp\_line(A,C),pp\_line(B,C));\\ 623 (num(u)*den(v)-den(u)*num(v)); 624\end{code} 625yields the same condition $p_4$. The common denominator {\tt 626den(u)*den(v)} corresponds to the degeneracy condition that either 627$A,B,C$ or $A,B,D$ are collinear. 628\medskip 629 630This condition is also equivalent to {\em Ptolemy's theorem}: 631\begin{quote} 632For points $A,B,C,D$ are (in that order) on a circle iff 633\[l(AB)*l(CD)+l(AD)*l(BC) = l(AC)*l(BD),\] 634i.e., the sum of the products of the lengths of opposite sides of the 635cyclic quadrilateral $ABCD$ equals the product of the lengths of its 636diagonals. 637\end{quote} 638For an elementary proof see \cite[2.61]{Coxeter:67}. To get a 639mechanized proof with the tools developed so far we are faced with 640several problems. First the theorem invokes distances and not their 641squares. Second the theorem uses the order of the given points. 642Unordered geometry can't even distinguish between sides and diagonals 643of a quadrilateral. 644 645The fist problem may be solved by repeated squaring. Denoting the 646lengths appropriately we get step by step 647\[\begin{array}{c} 648p\cdot r + q\cdot s = t\cdot u\\ 649(p\,r)^2+(q\,s)^2-(t\,u)^2 = -(2\,p\,q\,r\,s)\\ 650((p\,r)^2+(q\,s)^2-(t\,u)^2)^2 - (2\,p\,q\,r\,s)^2 = 0 651\end{array}\] 652arriving at an expression that contains only squared distances. This 653expression 654\[{\tt poly:= }\ p^4\,r^4 - 2\,p^2\,q^2\,r^2\,s^2 - 6552\,p^2\,r^2\,t^2\,u^2 + q^4\,s^4 - 2\,q^2\, s ^2\,t^2\,u^2 + t^4\,u^4 656\] 657is symmetric in pairs of opposite sides thus solving also the second 658problem. Substituting the corresponding squared distances of generic 659points $A,B,C,D$ we obtain exactly the square of the condition $p_4$. 660\medskip 661 662As for bisector coordinates the coordinates of intersection points of 663a circle and a line generally can't be expressed rationally in terms 664of the coordinates of the circles. For a generic circle {\tt c:= 665Circle($c_1,c_2,c_3,c_4$)} and a generic line {\tt 666d:=Line($d_1,d_2,d_3$)} we may solve the line equation for $y$ and 667substitute the result into the circle equation to get a single 668polynomial $q(x)$ of degree 2 with zeroes being the $x$-coordinate of 669the two intersection points of {\tt c} and {\tt d}: 670\begin{code}\>\+ 671vars:=\{x,y\};\\ 672polys:=\{c1*(x\^{}2+y\^{}2)+c2*x+c3*y+c4, d1*x+d2*y+d3\};\\ 673s:=solve(second polys,y);\\ 674q:=num sub(s,first polys); 675\end{code} 676$q:={x}^{2}\,c_1\,({d_1}^{2} +{d_2}^{2}) +x\,(2\,c_1\,d_1\,d_3 + 677c_2\,{d_2}^{2} -c_3\,d_1\,d_2 ) +(c_1\,{d_3}^{2} -c_3\,d_2\,d_3 678+c_4\,{d_2}^{2})$ 679\medskip 680 681In many cases {\tt d} is the line through a specified point {\tt P:= 682Point($p_1,p_2$)} on the circle. Fixing these coordinates as generic 683ones we get the algebraic relations 684\begin{code}\> 685polys:=\{point\_on\_line(P,d), point\_on\_circle(P,c)\}; 686\end{code} 687\formel{\{d_1\,p_1 +d_2\,p_2 +d_3, c_1\,{p_1}^{2} +c_1\,{p_2}^{2} 688 +c_2\,p_1 +c_3\,p_2 +c_4\}} 689between the coordinates of $c, d$ and $P$. This dependency may be 690removed solving these equations for $d_3$ and $c_4$. In the new 691coordinates the polynomial $q(x)$ factors 692\begin{code}\>\+ 693s:=solve(polys,\{d3,c4\});\\ 694factorize sub(s,q); 695\end{code} 696into $x-p_1$ and a second factor that is linear in $x$. This yields 697the coordinates for the intersection point of {\tt c} and {\tt d} 698different from {\tt P} that are saved into a function {\tt 699other\_cl\_point(P,c,d)}. Similarly we computed the coordinates of the 700second intersection point of two circles $c_1$ and $c_2$ passing 701through a common point {\tt P} and saved into a function {\tt 702other\_cc\_point(P,c1,c2)}. 703 704Also conditions on the coordinates of a circle and a line resp.\ two 705circles to be tangent may be derived in a similar way. 706\medskip 707 708\noindent 6) These functions admit a constructive proof of {\em 709Miquels theorem}: 710\begin{quote} Let $\Delta\,ABC$ be a triangle. Fix arbitrary points 711$P,Q,R$ on the sides $AB, BC, AC$. Then the three circles through each 712vertex and the chosen points on adjacent sides pass through a common 713point. 714\end{quote} 715Take as above 716\begin{code}\> 717A:=Point(0,0); B:=Point(1,0); C:=Point(c1,c2); 718\end{code} 719Generic points on the sides may be introduced with three auxiliary 720indeterminates: 721\begin{code}\>\+ 722P:=choose\_pl(pp\_line(A,B),u1);\\ 723Q:=choose\_pl(pp\_line(B,C),u2);\\ 724R:=choose\_pl(pp\_line(A,C),u3); 725\end{code} 726Then 727\begin{code}\> 728X:=other\_cc\_point(P,p3\_circle(A,P,R),p3\_circle(B,P,Q)); 729\end{code} 730is the intersection point of two of the circles different from {\tt P} 731(its generic coordinates contain 182 terms) and since 732\begin{code}\> 733point\_on\_circle(X,p3\_circle(C,Q,R)); 734\end{code} 735simplifies to zero the third circle also passes through {\tt X}. 736 737\section{Geometry Theorems of Equational Type} 738 739As already seen in the last section non-linear geometric conditions 740are best given through implicit polynomial dependency conditions on 741the coordinates of the geometric objects. In this more general setting 742a geometric statement may be translated into a {\em generic geometric 743configuration}, involving different geometric objects with coordinates 744depending on (algebraically independent) variables $\vau = (v_1, 745\ldots, v_n)$, a system of {\em polynomial conditions} $F= \{f_1, 746\ldots, f_r\}$ expressing the implicit geometric conditions and a 747polynomial $g$ encoding the geometric conclusion, such that, for a 748certain polynomial non degeneracy condition $h$, the following holds: 749\begin{quote}\it 750The geometric statement is true iff for all non degenerate correct 751special geometric configurations, i.e., with coordinates, obtained 752from the generic ones by specialization $v_i\mapsto c_i$ in such a 753way, that $f({\bf c})=0$ for all $f\in F$ but $h({\bf c})\neq 0$, the 754conclusion holds, i.e., $g({\bf c})$ vanishes. 755\end{quote} 756Denoting by $Z(F)$ the set of zeroes of the polynomial system $F$ and 757writing $Z(h)=Z(\{h\})$ for short, we arrive at {\em geometry theorems 758of equational type}, that may be shortly stated in the form 759\[Z(F)\setminus Z(h) \subseteq Z(g).\] 760Over an algebraically closed field, e.g. ${\bf C}$, this is equivalent 761to the ideal membership problem 762\[g\cdot h\in rad\ I(F),\] 763where $rad\ I(F)$ is the radical of the ideal generated by $F$. Even 764if $h$ is unknown a detailed analysis of the different components of 765the ideal $I(F)$ allows to obtain more insight into the geometric 766problem. 767\medskip 768 769Note the symmetry between $g$ and $h$ in the latter formulation of 770geometry theorems. This allows to derive {\em non degeneracy 771conditions} for a given geometry theorem of equational type from the 772stable ideal quotient 773\[h\in rad\ I(F):g^\infty.\] 774Since every element of this ideal may serve as non degeneracy 775condition there is no weakest condition among them, if the ideal is 776not principal. 777 778\subsection{Dependent and independent variables} 779 780Let $S=R[v_1,\ldots,v_n]$ be the polynomial ring in the given 781variables over the field of scalars $R$. The polynomial system $F$ 782describes algebraic dependency relations between these variables in 783such a way that the values of some of the variables may be chosen 784(almost) arbitrarily whereas the remaining variables are determined 785upto a finite number of values by these choices. 786\medskip 787 788A set of variables $\uhh\subset\vau$ is called {\em independent} wrt.\ 789the ideal $I=I(F)$ iff $I\cap R[\uhh]=(0)$, i.e., the variables are 790algebraically independent modulo $I$. If $\uhh$ is a maximal subset 791with this property the remaining variables $\iks=\vau\setminus\uhh$ 792are called {\em dependent}. 793 794Although a maximal set of independent variables may be read off from a 795\gr\ basis of $I$ there is often a natural choice of dependent and 796independent variables induced from the geometric problem. $\uhh$ is a 797maximal independent set of variables iff $F$ has a finite number of 798solutions as polynomial system in $\iks$ over the generic scalar field 799$R(\uhh)$. In many cases this may be proved with less effort than 800computing a \gr\ basis of $I$ over $S$. 801 802If $F$ has an infinite number of solutions then $\uhh$ was independent 803but not maximal. If $F$ has no solution then $\uhh$ was not 804independent. 805 806\subsection{Geometry theorems of linear type} 807 808We arrive at a particularly nice situation in the case when $F$ is a 809non degenerate quadratic linear system of equations in $\iks$ over 810$R(\uhh)$. Such geometry theorems are called {\em of linear type}. 811 812In this case there is a unique (rational) solution $\iks = \iks(\uhh)$ 813that may be substituted for the dependent variables into the geometric 814conclusion $g=g(\iks,\uhh)$. We obtain as for geometry theorems of 815constructive type a rational expression in $\uhh$ and 816\begin{quote}\it 817the geometry theorem holds (under the non degeneracy condition 818$h=det(F)\in R[\uhh]$, where $det(F)$ is the determinant of the linear 819system $F$) iff this expression simplifies to zero. 820\end{quote} 821 822 823\noindent 7) As an example consider the {\em theorem of Pappus}: 824\begin{quote} 825Let $A,B,C$ and $P,Q,R$ be two triples of collinear points. Then the 826intersection points $g(AQ)\wedge g(BP), g(AR)\wedge g(CP)$ and 827$g(BR)\wedge g(CQ)$ are collinear. 828\end{quote} 829The geometric conditions put no restrictions on $A,B,P,Q$ and one 830restriction on each $C$ and $R$. Hence we may take as generic 831coordinates 832\begin{code}\>\+ 833A:=Point(u1,u2); B:=Point(u3,u4); C:=Point(x1,u5);\\ 834P:=Point(u6,u7); Q:=Point(u8,u9); R:=Point(u0,x2); 835\end{code} 836with $u_0,\ldots,u_9$ independent and $x_1,x_2$ dependent, as 837polynomial conditions 838\begin{code}\> 839F:=\{collinear(A,B,C), collinear(P,Q,R)\}; 840\end{code} 841and as conclusion 842\begin{code}\+\+ 843con:=collinear(\\ 844 intersection\_point(pp\_line(A,Q),pp\_line(P,B)),\\ 845 intersection\_point(pp\_line(A,R),pp\_line(P,C)),\\ 846 intersection\_point(pp\_line(B,R),pp\_line(Q,C))); 847\end{code} 848a rational expression with 462 terms. The polynomial conditions are 849linear in $x_1,x_2$ and already separated. Hence 850\begin{code}\>\+ 851sol:=solve(polys,\{x1,x2\});\\ 852sub(sol,con); 853\end{code} 854proves the theorem since the expression obtained from $con$ 855substituting the dependent variables by their rational expressions in 856$\uhh$ simplifies to zero. 857\medskip 858 859As for most theorems of linear type the linear system may be solved 860``geometrically'' and the whole theorem may be translated into a 861constructive geometric statement: 862\begin{code}\>\+ 863A:=Point(u1,u2); B:=Point(u3,u4);\\ 864P:=Point(u6,u7); Q:=Point(u8,u9);\\[6pt] 865 866C:=choose\_pl(pp\_line(A,B),u5);\\ 867R:=choose\_pl(pp\_line(P,Q),u0);\\[6pt] 868 869con:=collinear(\+\\ 870 intersection\_point(pp\_line(A,Q),pp\_line(P,B)),\\ 871 intersection\_point(pp\_line(A,R),pp\_line(P,C)),\\ 872 intersection\_point(pp\_line(B,R),pp\_line(Q,C))); 873\end{code} 874 875\subsection{Geometry theorems of non-linear type} 876 877Lets return to the general situation of a polynomial system $F\subset 878S$ that describes algebraic dependency relations, a subdivision 879$\vau=\iks\cup\uhh$ of the variables into dependent and independent 880ones, and the conclusion polynomial $g(\iks,\uhh)\in S$. The set of 881zeros $Z(F)$ may be decomposed into irreducible components that 882correspond to prime components $P_\alpha$ of the ideal $I=I(F)$ 883generated by $F$ over the ring $S=R[\iks,\uhh]$. 884 885Since $P_\alpha\supset I$ the variables $\uhh$ may become dependent 886wrt.\ $P_\alpha$. Prime components where $\uhh$ remains independent 887are called {\em generic}, the other components are called {\em 888special}. Note that each special component contains a non zero 889polynomial in $R[\uhh]$. Multiplying them all together yields a non 890degeneracy condition $h=h(\uhh)\in R[\uhh]$ on the independent 891variables such that a zero $P\in Z(F)$ with $h(P)\neq 0$ necessarily 892belongs to one of the generic components. Hence they are the 893``essential'' components and we say that the geometry theorem is {\em 894generically true}, when the conclusion polynomial $g$ vanishes on all 895these generic components. 896\medskip 897 898If we compute in the ring $S'=R(\uhh)[\iks]$, i.e., consider the 899independent variables as parameters, exactly the generic components 900remain visible. Indeed, this corresponds to a localization of $S$ by 901the multiplicative set $R[\uhh]\setminus\{0\}$. Hence the geometry 902theorem is generically true iff $g\in rad(I)\cdot S'$, i.e. $g$ 903belongs to the radical of the ideal $I$ in this special extension of 904$S$. A sufficient condition can be derived from a \gr\ basis $G$ of 905$F$ with the $\uhh$ variables as parameters: Test whether $g\ mod\ G 906=0$, i.e., the normal form vanishes. More subtle examples may be 907analyzed with the \gr\ factorizer or more advanced techniques from the 908authors package CALI, \cite{CALI}. 909\medskip 910 911\noindent 8) As an application we consider the following nice theorem 912from \cite[ch. 4, \S\ 2]{Coxeter:67} about Napoleon triangles: 913\begin{quote} 914Let $\Delta\,ABC$ be an arbitrary triangle and $P,Q$ and $R$ the third 915vertex of equilateral triangles erected externally on the sides $BC, 916AC$ and $AB$ of the triangle. Then the lines $g(AP), g(BQ)$ and 917$g(CR)$ pass through a common point, the {\em Fermat point} of the 918triangle $\Delta\,ABC$. 919\end{quote} 920 921A mechanized proof again will be faced with the difficulty that 922unordered geometry can't distinguish between different sides wrt.\ a 923line. A straightforward formulation of the geometric conditions starts 924with independent coordinates for $A,B,C$ and dependent coordinates for 925$P,Q,R$. W.l.o.g. we may fix the coordinates in the following way: 926\begin{code}\+\> 927A:=Point(0,0); B:=Point(0,2); C:=Point(u1,u2);\\ 928P:=Point(x1,x2); Q:=Point(x3,x4); R:=Point(x5,x6); 929\end{code} 930There are 6 geometric conditions for the 6 dependent variables. 931\begin{code}\+\+ 932polys:=\{\>\>sqrdist(P,B)-sqrdist(B,C), sqrdist(P,C)-sqrdist(B,C),\\ 933 sqrdist(Q,A)-sqrdist(A,C), sqrdist(Q,C)-sqrdist(A,C),\\ 934 sqrdist(R,B)-sqrdist(A,B), sqrdist(R,A)-sqrdist(A,B)\}; 935\end{code} 936\formel{ 937{x_1}^{2} +{x_2}^{2} -4\,x_2 -{u_1}^{2} -{u_2}^{2} +4\,u_2\\ 938{x_1}^{2} -2\,x_1\,u_1 +{ x_2}^{2} -2\,x_2\,u_2 +4\,u_2 -4\\ 939{x_3}^{2} +{x_4}^{2} -{u_1}^{2} -{u_2}^{2}\\ 940{x_3}^{2} -2\,x_3\,u_1 +{x_4}^{2} -2\,x_4\,u_2\\ 941{x_5}^{2} +{x_6}^{2} -4\,x_6\\ 942{x_5}^{2} +{x_6}^{2} -4} 943These equations may be divided into three groups of two quadratic 944relations for the coordinates of each of the points $P,Q,R$. Each of 945this pairs has (only) two solutions, the inner and the outer triangle 946vertex, since it may easily be reduced to a quadratic and a linear 947equation, the line equation of the corresponding midpoint 948perpendicular. Hence the whole system has 8 solutions and by geometric 949reasons the conclusion 950\begin{code}\> 951con:=concurrent(pp\_line(A,P), pp\_line(B,Q), pp\_line(C,R)); 952\end{code} 953will hold on at most two of them. Due to the special structure the 954interreduced polynomial system is already a \gr\ basis and hence can't 955be split by the \gr\ factorizer. A full decomposition into isolated 956primes yields four components over $R(\uhh)$, each corresponding to a 957pair of solutions over the algebraic closure. On one of them the 958conclusion polynomial reduces to zero thus proving the geometry 959theorem. 960\begin{code}\>\+ 961vars:=\{x1,x2,x3,x4,x5,x6\};\\ 962setring(vars,\{\},lex);\\ 963iso:=isolatedprimes polys;\\[6pt] 964 965for each u in iso collect con mod u; 966\end{code} 967With a formulation as in \cite[p.~123]{Chou:88}, that uses oriented 968angles, we may force all Napoleon triangles to be erected on the {\em 969same} side (internally resp.\ externally) and prove a more general 970theorem as above. Taking isosceles triangles with equal base angles 971and (due to one more degree of freedom) $x_5$ as independent the 972conclusion remains valid: 973\begin{code} 974polys2:=\{\>\>sqrdist(P,B)-sqrdist(P,C),\+\+\\ 975 sqrdist(Q,A)-sqrdist(Q,C), \\ 976 sqrdist(R,A)-sqrdist(R,B), \\ 977 num(p3\_angle(R,A,B)-p3\_angle(P,B,C)), \\ 978 num(p3\_angle(Q,C,A)-p3\_angle(P,B,C))\};\-\-\\[6pt] 979 980sol:=solve(polys2,\{x1,x2,x3,x4,x6\});\\ 981sub(first sol,con); 982\end{code} 983again simplifies to zero. Note that the new theorem is of linear type. 984 985\section{The Procedures Supplied by \geo}\label{description} 986 987This section contains a short description of all procedures available 988in \geo. We refer to the data types {\tt Scalar, Point, Line, Circle1} 989and {\tt Circle} described above. Booleans are represented as extended 990booleans, i.e.\ the procedure returns a {\tt Scalar} that is zero iff 991the condition is fulfilled. In some cases also a non zero result has a 992geometric meaning. For example, {\tt collinear(A,B,C)} returns the 993signed area of the corresponding parallelogram. 994\bigskip 995 996\xxyy{angle\_sum(a,b:Scalar):Scalar }{Returns $\tan(\alpha+\beta)$, if 997$a=\tan(\alpha), b=\tan(\beta)$.} 998\xxyy{altitude(A,B,C:Point):Line }{The altitude from $A$ onto 999$g(BC)$. } 1000\xxyy{c1\_circle(M:Point,sqr:Scalar):Circle}{The circle with given 1001center and sqradius.} 1002\xxyy{cc\_tangent(c1,c2:Circle):Scalar}{Zero iff $c_1$ and $c_2$ are 1003tangent.} 1004\xxyy{choose\_pc(M:Point,r,u):Point}{Chooses a point on the circle 1005around $M$ with radius $r$ using its rational parametrization with 1006parameter $u$.} 1007\xxyy{choose\_pl(a:Line,u):Point }{Chooses a point on $a$ using 1008parameter $u$.} 1009\xxyy{Circle(c1,c2,c3,c4:Scalar):Circle}{The {\tt Circle} constructor.} 1010\xxyy{Circle1(M:Point,sqr:Scalar):Circle1}{The {\tt Circle1} 1011constructor. } 1012\xxyy{circle\_center(c:Circle):Point}{The center of $c$.} 1013\xxyy{circle\_sqradius(c:Circle):Point}{The sqradius of $c$.} 1014\xxyy{cl\_tangent(c:Circle,l:Line):Scalar}{Zero iff $l$ is tangent to 1015$c$.} 1016\xxyy{collinear(A,B,C:Point):Scalar}{Zero iff $A,B,C$ are on a common 1017line. In general the signed area of the parallelogram spanned by 1018$\vec{AB}$ and $\vec{AC}$. } 1019\xxyy{concurrent(a,b,c:Line):Scalar}{Zero iff $a,b,c$ have a common 1020point.} 1021\xxyy{intersection\_point(a,b:Line):Point}{The intersection point of 1022the lines $a,b$. } 1023\xxyy{l2\_angle(a,b:Line):Scalar}{Tangens of the angle between $a$ and 1024$b$. } 1025\xxyy{Line(a,b,c:Scalar):Line}{The {\tt Line} constructor.} 1026\xxyy{lot(P:Point,a:Line):Line}{The perpendicular from $P$ onto $a$.} 1027\xxyy{median(A,B,C:Point):Line}{The median line from $A$ to $BC$.} 1028\xxyy{midpoint(A,B:Point):Point}{The midpoint of $AB$. } 1029\xxyy{mp(B,C:Point):Line}{The midpoint perpendicular of $BC$.} 1030\xxyy{orthogonal(a,b:Line):Scalar}{zero iff the lines $a,b$ are 1031orthogonal. } 1032\xxyy{other\_cc\_point(P:Point,c1,c2:Circle):Point}{ $c_1$ and $c_2$ 1033intersect at $P$. The procedure returns the second intersection 1034point. } 1035\xxyy{other\_cl\_point(P:Point,c:Circle,l:Line):Point}{$c$ and $l$ 1036intersect at $P$. The procedure returns the second intersection 1037point.} 1038\xxyy{p3\_angle(A,B,C:Point):Scalar}{Tangens of the angle between 1039$\vec{BA}$ and $\vec{BC}$. } 1040\xxyy{p3\_circle(A,B,C:Point):Circle\ {\rm or\ }\\ 1041p3\_circle1(A,B,C:Point):Circle1}{The circle through 3 given points. } 1042\xxyy{p4\_circle(A,B,C,D:Point):Scalar}{Zero iff four given points 1043are on a common circle. } 1044\xxyy{par(P:Point,a:Line):Line}{The line through $P$ parallel to 1045$a$. } 1046\xxyy{parallel(a,b:Line):Scalar}{Zero iff the lines $a,b$ are 1047parallel. } 1048\xxyy{pedalpoint(P:Point,a:Line):Point}{The pedal point of the 1049perpendicular from $P$ onto $a$.} 1050\xxyy{Point(a,b:Scalar):Point}{The {\tt Point} constructor.} 1051\xxyy{point\_on\_bisector(P,A,B,C:Point):Scalar}{Zero iff $P$ is a 1052point on the (inner or outer) bisector of the angle $\angle\,ABC$.} 1053\xxyy{point\_on\_circle(P:Point,c:Circle):Scalar\ {\rm or\ }\\ 1054point\_on\_circle1(P:Point,c:Circle1):Scalar}{Zero iff $P$ is on the 1055circle $c$.} 1056\xxyy{point\_on\_line(P:Point,a:Line):Scalar}{Zero iff $P$ is on the 1057line $a$. } 1058\xxyy{pp\_line(A,B:Point):Line}{The line through $A$ and $B$.} 1059\xxyy{sqrdist(A,B:Point):Scalar}{Square of the distance between $A$ 1060and $B$.} 1061\xxyy{sympoint(P:Point,l:Line):Point}{The point symmetric to $P$ wrt.\ 1062the line $l$.} 1063\xxyy{symline(a:Line,l:Line):Line}{The line symmetric to $a$ wrt.\ the 1064line $l$.} 1065\xxyy{varpoint(A,B:Point,u):Point}{The point $D=u\cdot A+(1-u)\cdot 1066B$. } 1067 1068\noindent \geo\ supplies as additional tools the functions 1069\bigskip 1070 1071\xxyy{extractmat(polys,vars)}{Returns the coefficient matrix of the 1072list of equations $polys$ that are linear in the variables $vars$. } 1073\xxyy{red\_hom\_coords(u:\{Line,Circle\})}{Returns the reduced 1074homogeneous coordinates of $u$, i.e., divides out the content. } 1075 1076 1077 1078\section{More Examples} 1079 1080Here we give a more detailed explanation of some of the examples 1081collected in the test file {\tt geometry.tst} and give a list of 1082exercises. Their solutions can be found in the test file, too. 1083 1084\subsection{Theorems that can be translated into theorems of 1085constructive or linear type} 1086 1087There are many geometry theorems that may be reformulated as theorems 1088of constructive type. 1089\medskip 1090 1091 1092\noindent 9) The affine version of {\em Desargue's theorem}: 1093\begin{quote} 1094If two triangles $\Delta\,ABC$ and $\Delta\,RST$ are in similarity 1095position,\linebreak i.e., $g(AB)\,\|g(RS),\ g(BC)\|g(ST)$ and 1096$g(AC)\|g(RT)$, then $g(AR),\linebreak g(BS)$ and $g(CT)$ pass through 1097a common point (or are parallel). 1098\end{quote} 1099 1100The given configuration may be constructed step by step in the 1101following way: Take $A,B,C,R$ arbitrarily, choose $S$ arbitrarily on 1102the line through $R$ parallel to $g(AB)$ and $T$ as the intersection 1103point of the lines through $R$ parallel to $g(AC)$ and through $S$ 1104parallel to $g(BC)$. 1105\begin{code}\>\+ 1106A:=Point(a1,a2); B:=Point(b1,b2);\\ 1107C:=Point(c1,c2); R:=Point(d1,d2);\\ 1108S:=choose\_pl(par(R,pp\_line(A,B)),u);\\ 1109T:=intersection\_point(\\\>\> 1110 par(R,pp\_line(A,C)),par(S,pp\_line(B,C)));\\[6pt] 1111 1112con:=concurrent(pp\_line(A,R),pp\_line(B,S),pp\_line(C,T)); 1113\end{code} 1114Another proof may be obtained translating the statement into a theorem 1115of linear type. Since the geometric conditions put no restrictions on 1116$A,B,C,R$, one restriction on $S$ ($g(AB)\|g(RS)$) and two 1117restrictions on $T$ ($g(BC)\|g(ST),\,$ $g(AC)\|g(RT)$), 1118we may take as generic coordinates 1119\begin{code}\>\+ 1120A:=Point(u1,u2); B:=Point(u3,u4); C:=Point(u5,u6);\\ 1121R:=Point(u7,u8); S:=Point(u9,x1); T:=Point(x2,x3); 1122\end{code} 1123with $u_1,\ldots,u_9$ independent and $x_1,x_2,x_3$ dependent, as 1124polynomial conditions 1125\begin{code}\+\+ 1126polys:=\{\>\>parallel(pp\_line(R,S),pp\_line(A,B)),\\ 1127 parallel(pp\_line(S,T),pp\_line(B,C)),\\ 1128 parallel(pp\_line(R,T),pp\_line(A,C))\}; 1129\end{code} 1130and as conclusion 1131\begin{code}\> 1132con:=concurrent(pp\_line(A,R),pp\_line(B,S),pp\_line(C,T)); 1133\end{code} 1134The polynomial conditions are linear in $x_1,x_2,x_3$ and thus 1135\begin{code}\>\+ 1136sol:=solve(polys,\{x1,x2,x3\});\\ 1137sub(sol,con); 1138\end{code} 1139proves the theorem since the expression obtained from $con$ 1140substituting the dependent variables by their rational expressions in 1141$\uhh$ simplifies to zero. 1142\medskip 1143 1144The general version of {\em Desargue's theorem}: 1145\begin{quote} 1146The lines $g(AR),\ g(BS)$ and $g(CT)$ pass through a common point iff 1147the intersection points $g(AB)\wedge g(RS),\ g(BC)\wedge g(ST)$ and 1148$g(AC)\wedge g(RT)$ are collinear. 1149\end{quote} 1150may be reduced to the above theorem by a projective transformation 1151mapping the line through the three intersection points to infinity. 1152Its algebraic formulation 1153\begin{code}\>\+ 1154A:=Point(0,0); B:=Point(0,1); C:=Point(u5,u6);\\ 1155R:=Point(u7,u8); S:=Point(u9,u1); T:=Point(u2,x1);\\[6pt] 1156con1:=collinear(\+\\intersection\_point(pp\_line(R,S),pp\_line(A,B)),\\ 1157 intersection\_point(pp\_line(S,T),pp\_line(B,C)),\\ 1158 intersection\_point(pp\_line(R,T),pp\_line(A,C)));\-\\ 1159 1160con2:=concurrent(pp\_line(A,R),pp\_line(B,S),pp\_line(C,T)); 1161\end{code} 1162contains a polynomial $con_2$ linear in $x_1$ and a rational function 1163$con_1$ with numerator quadratic in $x_1$ that factors as 1164\[{\rm num}(con_1)=con_2\cdot {\rm collinear}(R,S,T)\] 1165thus also proving the general theorem. 1166\medskip 1167 1168\noindent 10) Consider the following theorem about the {\em Brocard 1169points} (\cite[p.~336]{Chou:88}) 1170\begin{quote} 1171Let $\Delta\,ABC$ be a triangle. The circles $c_1$ through $A,B$ and 1172tangent to $g(AC)$, $c_2$ through $B,C$ and tangent to $g(AB)$, and 1173$c_3$ through $A,C$ and tangent to $g(BC)$ pass through a common 1174point. 1175\end{quote} 1176It leads to a theorem of linear type that can't be translated into 1177constructive type in an obvious way. The circles may be described each 1178by 3 dependent variables and 3 conditions 1179\begin{code}\>\+ 1180A:=Point(0,0); B:=Point(1,0); C:=Point(u1,u2);\\[6pt] 1181 1182c1:=Circle(1,x1,x2,x3);\\ 1183c2:=Circle(1,x4,x5,x6);\\ 1184c3:=Circle(1,x7,x8,x9);\-\\[6pt] 1185 1186polys:=\{\>\> 1187 cl\_tangent(c1,pp\_line(A,C)), \+\+\\ 1188 point\_on\_circle(A,c1), \\ 1189 point\_on\_circle(B,c1), \\ 1190 cl\_tangent(c2,pp\_line(A,B)), \\ 1191 point\_on\_circle(B,c2), \\ 1192 point\_on\_circle(C,c2), \\ 1193 cl\_tangent(c3,pp\_line(B,C)), \\ 1194 point\_on\_circle(A,c3), \\ 1195 point\_on\_circle(C,c3)\}; 1196\end{code} 1197that are linear in the dependent variables. Hence the coordinates of 1198the circles and the intersection point of two of them may be computed 1199and checked for incidence with the third circle: 1200\begin{code}\>\+ 1201vars:=\{x1,x2,x3,x4,x5,x6,x7,x8,x9\};\\ 1202sol:=solve(polys,vars);\\[6pt] 1203 1204P:=other\_cc\_point(C,sub(sol,c1),sub(sol,c2));\\ 1205con:=point\_on\_circle(P,sub(sol,c3)); 1206\end{code} 1207Again $con$ simplifies to zero thus proving the theorem. 1208\medskip 1209 1210Even some theorems involving nonlinear objects as circles may be 1211translated into theorems of constructive type using a rational 1212parametrization of the non linear object. For a circle with radius $r$ 1213and center $M=(m_1,m_2)$ we may use the rational parametrization 1214\[\{(\frac{1-u^2}{1+u^2}r+m_1,\frac{2u}{1+u^2}r+m_2)\ |\ u\in {\bf 1215C}\}.\] 1216This way we can prove 1217\medskip 1218 1219\noindent 11) {\em Simson's theorem} (\cite[p. 261]{Chou:84}, 1220\cite[thm. 2.51]{Coxeter:67}): 1221\begin{quote} 1222Let $P$ be a point on the circle circumscribed to the triangle 1223$\Delta\,ABC$ and $X,Y,Z$ the pedal points of the perpendiculars from 1224$P$ onto the lines passing through pairs of vertices of the triangle. 1225These points are collinear. 1226\end{quote} 1227 1228Take the center $M$ of the circumscribed circle as the origin and $r$ 1229as its radius. The proof of the problem may be mechanized in the 1230following way: 1231\begin{code}\>\+ 1232 M:=Point(0,0);\\ 1233 A:=choose\_pc(M,r,u1);\\ 1234 B:=choose\_pc(M,r,u2);\\ 1235 C:=choose\_pc(M,r,u3);\\ 1236 P:=choose\_pc(M,r,u4);\\ 1237 X:=pedalpoint(P,pp\_line(A,B));\\ 1238 Y:=pedalpoint(P,pp\_line(B,C));\\ 1239 Z:=pedalpoint(P,pp\_line(A,C));\\[8pt] 1240 1241 con:=collinear(X,Y,Z); 1242\end{code} 1243Since $con$ simplifies to zero this proves the theorem. 1244 1245 1246\subsection{Theorems of equational type} 1247 1248An ``almost'' constructive proof of Simson's theorem may be obtained 1249in the following way: 1250\begin{code}\>\+ 1251 A:=Point(0,0); B:=Point(u1,u2);\\ 1252 C:=Point(u3,u4); P:=Point(u5,x1);\\ 1253 X:=pedalpoint(P,pp\_line(A,B));\\ 1254 Y:=pedalpoint(P,pp\_line(B,C));\\ 1255 Z:=pedalpoint(P,pp\_line(A,C));\\[6pt] 1256 1257 poly:=p4\_circle(A,B,C,P);\\[6pt] 1258 1259 con:=collinear(X,Y,Z); 1260\end{code} 1261There is a single dependent variable bound by the quadratic condition 1262$poly$ that the given points are on a common circle. $con$ is a 1263rational expression with numerator equal to 1264\formel{poly\cdot {\rm collinear}(A,B,C)^2. } 1265Since the second factor may be considered as degeneracy condition this 1266also proves Simson's theorem. The factors of the denominator 1267\formel{{\rm den}(con)={\rm sqrdist}(A,B)\cdot {\rm sqrdist}(A,C)\cdot 1268{\rm sqrdist}(B,C) } 1269are exactly the non degeneracy conditions collected during the 1270computation. They may be printed with {\tt print\_ndg()}. 1271\medskip 1272 1273One may also substitute the rational coordinate construction of 1274$X,Y,Z$ through {\tt pedalpoint} with additional dependent variables 1275and polynomial conditions: 1276\begin{code}\>\+ 1277M:=Point(0,0); A:=Point(0,1); \\ 1278B:=Point(u1,x1); C:=Point(u2,x2); P:=Point(u3,x3);\\ 1279X:=varpoint(A,B,x4);\\ Y:=varpoint(B,C,x5);\\ Z:=varpoint(A,C,x6); 1280\end{code} 1281The polynomial conditions 1282\begin{code} 1283polys:=\{\>\> sqrdist(M,B)-1, sqrdist(M,C)-1, sqrdist(M,P)-1,\+\+\\ 1284 orthogonal(pp\_line(A,B),pp\_line(P,X)),\\ 1285 orthogonal(pp\_line(A,C),pp\_line(P,Z)),\\ 1286 orthogonal(pp\_line(B,C),pp\_line(P,Y))\}; 1287\end{code} 1288contain three quadratic polynomials in $x_1,x_2,x_3$ and three 1289polynomials linear in $x_4,x_5,x_6$. The quadratic polynomials 1290correspond to different points on the circle with given 1291$x$-coordinate. The best variable order eliminates linear variables 1292first. Thus the following computations prove the theorem 1293\begin{code} 1294con:=collinear(X,Y,Z);\\[8pt] 1295 1296vars:=\{x4,x5,x6,x1,x2,x3\};\\ 1297setring(vars,\{\},lex);\\ 1298setideal(polys,polys);\\ 1299con mod gbasis polys; 1300\end{code} 1301since the conclusion polynomial reduces to zero. 1302\medskip 1303 1304\noindent 12) The Butterfly Theorem (\cite[p. 269]{Chou:84}, 1305\cite[thm. 2.81]{Coxeter:67}) : 1306\begin{quote} 1307Let $A,B,C,D$ be four points on a circle with center $O$, $P$ the 1308intersection point of $AC$ and $BD$ and $F$ resp. $G$ the intersection 1309point of the line through $P$ perpendicular to $OP$ with $AB$ 1310resp. $CD$. Then $P$ is the midpoint of $FG$. 1311\end{quote} 1312Taking $P$ as the origin and the lines $g(FG)$ and $g(OP)$ as axes we 1313get the following coordinatization: 1314\begin{code}\>\+ 1315P:=Point(0,0); O:=Point(u1,0);\\ 1316A:=Point(u2,u3); B:=Point(u4,x1);\\ 1317C:=Point(x2,x3); D:=Point(x4,x5); \\ 1318F:=Point(0,x6); G:=Point(0,x7);\-\\[6pt] 1319 1320polys:=\{\>\> sqrdist(O,B)-sqrdist(O,A),\+\+\\ 1321 sqrdist(O,C)-sqrdist(O,A), \\ 1322 sqrdist(O,D)-sqrdist(O,A),\\ 1323 point\_on\_line(P,pp\_line(A,C)),\\ 1324 point\_on\_line(P,pp\_line(B,D)),\\ 1325 point\_on\_line(F,pp\_line(A,D)),\\ 1326 point\_on\_line(G,pp\_line(B,C))\};\-\-\\[6pt] 1327 1328con:=num sqrdist(P,midpoint(F,G)); 1329\end{code} 1330Note that the formulation of the theorem includes $A\neq C$ and $B\neq 1331D$. Hence the conclusion may (and will) fail on some of the components 1332of $Z(polys)$. This can be avoided supplying appropriate constraints 1333to the \gr\ factorizer: 1334\begin{code}\>\+ 1335vars:=\{x6,x7,x3,x5,x1,x2,x4\};\\ 1336setring(vars,\{\},lex);\\[6pt] 1337 1338sol:=groebfactor(polys,\{sqrdist(A,C),sqrdist(B,D)\});\\[6pt] 1339 1340for each u in sol collect con mod u; 1341\end{code} 1342$sol$ contains a single solution that reduces the conclusion $con$ to 1343zero. Hence the \gr\ factorizer could split the components and remove 1344the auxiliary ones. 1345 1346 1347 1348Note that there is also a constructive proof of the Butterfly theorem, 1349see {\tt geometry.tst}. 1350\medskip 1351 1352 1353\noindent 13) Let's prove another property of Feuerbach's circle 1354(\cite[thm. 5.61]{Coxeter:67}): 1355\begin{quote} 1356For an arbitrary triangle $\Delta\,ABC$ Feuerbach's circle is tangent 1357to its in- and excircles (tangent circles for short). 1358\end{quote} 1359Take the same coordinates as in example 5 and construct the 1360coordinates of the center $N$ of Feuerbach's circle $c_1$ as in 1361example 4: 1362\begin{code}\>\+ 1363A:=Point(0,0); B:=Point(2,0); C:=Point(u1,u2);\\ 1364 1365M:=intersection\_point(mp(A,B),mp(B,C));\\ 1366H:=intersection\_point(altitude(A,B,C),altitude(B,C,A));\\ 1367N:=midpoint(M,H);\\[6pt] 1368 1369c1:=c1\_circle(N,sqrdist(N,midpoint(A,B))); 1370\end{code} 1371The coordinates of the center {\tt P:=Point(x1,x2)} of one of the 1372tangent circles are bound by the conditions 1373\begin{code} 1374polys:=\{point\_on\_bisector(P,A,B,C), point\_on\_bisector(P,B,C,A)\}; 1375\end{code} 1376Due to the choice of the coordinates $x_2$ is the radius of this 1377circle. Hence the conclusion may be expressed as 1378\begin{code}\> 1379con:=cc\_tangent(c1\_circle(P,x2\^{}2),c1); 1380\end{code} 1381The polynomial conditions $polys$ have four generic solutions, the 1382centers of the four tangent circles, as derived in example 5. Since 1383\begin{code}\>\+ 1384vars:=\{x1,x2\};\\ 1385setring(vars,\{\},lex);\\ 1386setideal(polys,polys);\\ 1387num con mod gbasis polys; 1388\end{code} 1389yields zero this proves that all four circles are tangent to 1390Feuerbach's circle. \cite[ch.5,\S 6]{Coxeter:67} points out that 1391Feuerbach's circle of $\Delta\,ABC$ coincides with Feuerbach's circle 1392of each of the triangles $\Delta\,ABH,\, \Delta\,ACH$ and 1393$\Delta\,BCH$. Hence there are another 12 circles tangent to 1394$c_1$. This may be proved 1395 1396 1397 1398 1399Note that the proof in \cite{Coxeter:67} uses inversion geometry. The 1400author doesn't know about a really ``elementary'' proof of this 1401theorem. 1402 1403\section{Exercises} 1404 1405\begin{itemize} 1406\item[1.] (\cite[p. 267]{Chou:84}) Let $ABCD$ be a square and $P$ a 1407point on the line parallel to $BD$ through $C$ such that 1408$l(BD)=l(BP)$, where $l(BD)$ denotes the distance between $B$ and 1409$D$. Let $Q$ be the intersection point of $BF$ and $CD$. Show that 1410$l(DP)=l(DQ)$. 1411 1412\item[2.] The altitudes' pedal points theorem: Let $P,Q,R$ be the 1413altitudes' pedal points in the triangle $\Delta\,ABC$. Show that the 1414altitude through $Q$ bisects $\angle\, PQR$. 1415 1416\item[3.] Let $\Delta\,ABC$ be an arbitrary triangle. Consider the 1417three altitude pedal points and the pedal points of the perpendiculars 1418from these points onto the the opposite sides of the triangle. Show 1419that these 6 points are on a common circle, the {\em Taylor circle}. 1420 1421\item[4.] Prove the formula \[F(\Delta\,ABC) = \frac{a\,b\,c}{4\,R},\] 1422for the area of the triangle $\Delta\,ABC$, if $a,b,c$ are the lengths 1423of its sides and $R$ the radius of its circumscribed circle. 1424 1425\item[5.] (\cite[p. 283]{Chou:84}) Let $k$ be a circle, $A$ the contact 1426point of the tangent line from a point $B$ to $k$, $M$ the midpoint of 1427$AB$ and $D$ a point on $k$. Let $C$ be the second intersection point 1428of $DM$ with $k$, $E$ the second intersection point of $BD$ with $k$ 1429and $F$ the second intersection point of $BC$ with $k$. Show that $EF$ 1430is parallel to $AB$. 1431 1432\item[6.] (35th IMO 1995, Toronto, problem 1, \cite{IMO}) Let 1433$A,B,C,D$ be four distinct points on a line, in that order. The 1434circles with diameters $AC$ and $BD$ intersect at the points $X$ and 1435$Y$. The line $XY$ meets $BC$ at the point $Z$. Let $P$ be a point on 1436the line $XY$ different from $Z$. The line $CP$ intersects the circle 1437with diameter $AC$ at the points $C$ and $M$, and the line $BP$ 1438intersects the circle with diameter $BD$ at the points $B$ and 1439$N$. Prove that the lines $AM, DN$ and $XY$ are concurrent. 1440 1441\item[7.] (34th IMO 1994, Hong Kong, problem 2, \cite{IMO}) $ABC$ is 1442an isosceles triangle with $AB = AC$. Suppose that 1443\begin{enumerate} 1444\item[(i)] $M$ is the midpoint of $BC$ and $O$ is the point on the 1445line $AM$ such that $OB$ is perpendicular to $AB$; 1446\item[(ii)] $Q$ is an arbitrary point on the segment $BC$ different 1447from $B$ and $C$; 1448\item[(iii)] $E$ lies on the line $AB$ and $F$ lies on the line $AC$ 1449such that $E, Q$ and $F$ are distinct and collinear. 1450\end{enumerate} 1451\noindent 1452Prove that $OQ$ is perpendicular to $EF$ if and only if $QE = QF$. 1453 1454\item[8.] (4th IMO 1959, Czechia, problem 6, \cite{Morozova:68}) Show 1455that the distance $d$ between the centers of the inscribed and the 1456circumscribed circles of a triangle $\Delta\,ABC$ satisfies 1457$d^2=r^2-2r\rho$, where $r$ is the radius of the circumscribed circle 1458and $\rho$ the radius of the inscribed circle. 1459 1460\item[9.] (1th IMO 1959, Roumania, problem 5, \cite{Morozova:68}) Let 1461$M$ be a point on AB, $AMCD$ and $MBEF$ squares to the same side of 1462$g(AB)$ and $N$ the intersection point of their circumscribed circles, 1463different from $M$. 1464\begin{enumerate} 1465\item[(i)] Show that $g(AF)$ and $g(BC)$ intersect at $N$. 1466\item[(ii)] Show that all lines $g(MN)$ for various $M$ meet at a 1467common point. 1468\end{enumerate} 1469 1470\end{itemize} 1471 1472 1473\bibliographystyle{plain} \bibliography{geometry} 1474 1475\end{document} 1476