1% GeoProver test file for Reduce, created on Jan 18 2003 2load cali,geoprover; 3off nat; on echo; 4 5% The following "in" fails in the test harness that I use at present and 6% so I have put the contents of the file that would have been read in-line 7% in the test script. 8 9%in "$reduce/packages/geometry/supp.red"$ 10 11%############################################################### 12% 13% FILE: supp.red 14% AUTHOR: graebe 15% CREATED: 2/2002 16% PURPOSE: Interface for the extended GEO syntax to Reduce 17% VERSION: $Id: supp.red,v 1.1 2002/12/26 16:27:22 compalg Exp $ 18 19 20% Redistribution and use in source and binary forms, with or without 21% modification, are permitted provided that the following conditions are met: 22% 23% * Redistributions of source code must retain the relevant copyright 24% notice, this list of conditions and the following disclaimer. 25% * Redistributions in binary form must reproduce the above copyright 26% notice, this list of conditions and the following disclaimer in the 27% documentation and/or other materials provided with the distribution. 28% 29% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 30% AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, 31% THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR 32% PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR 33% CONTRIBUTORS 34% BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 35% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF 36% SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 37% INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN 38% CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 39% ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 40% POSSIBILITY OF SUCH DAMAGE. 41% 42 43algebraic procedure geo_simplify u; u; 44algebraic procedure geo_normal u; u; 45algebraic procedure geo_subs(a,b,c); sub(a=b,c); 46 47algebraic procedure geo_gbasis(polys,vars); 48 begin 49 setring(vars,{},lex); 50 setideal(uhu,polys); 51 return gbasis uhu; 52 end; 53 54algebraic procedure geo_groebfactor(polys,vars,nondeg); 55 begin 56 setring(vars,{},lex); 57 return groebfactor(polys,nondeg); 58 end; 59 60algebraic procedure geo_normalf(p,polys,vars); 61 begin 62 setring(vars,{},lex); 63 return p mod polys; 64 end; 65 66algebraic procedure geo_eliminate(polys,vars,elivars); 67 begin 68 setring(vars,{},lex); 69 return eliminate(polys,elivars); 70 end; 71 72algebraic procedure geo_solve(polys,vars); 73 solve(polys,vars); 74 75algebraic procedure geo_solveconstrained(polys,vars,nondegs); 76 begin scalar u; 77 setring(vars,{},lex); 78 u:=groebfactor(polys,nondegs); 79 return for each x in u join solve(x,vars); 80 end; 81 82algebraic procedure geo_eval(con,sol); 83 for each x in sol collect sub(x,con); 84 85% End of what was in supp.red 86 87 88 89 90 91% Example Arnon 92% 93% The problem: 94% Let $ABCD$ be a square and $P$ a point on the line parallel to $BD$ 95% through $C$ such that $l(BD)=l(BP)$, where $l(BD)$ denotes the 96% distance between $B$ and $D$. Let $Q$ be the intersection point of 97% $BF$ and $CD$. Show that $l(DP)=l(DQ)$. 98% 99% The solution: 100 101vars_:=List(x1, x2, x3); 102% Points 103A__:=Point(0,0); B__:=Point(1,0); P__:=Point(x1,x2); 104% coordinates 105D__:=rotate(A__,B__,1/2); 106C__:=par_point(D__,A__,B__); 107Q__:=varpoint(D__,C__,x3); 108% polynomials 109polys_:=List(on_line(P__,par_line(C__,pp_line(B__,D__))), 110 eq_dist(B__,D__,B__,P__), on_line(Q__,pp_line(B__,P__))); 111% conclusion 112con_:=eq_dist(D__,P__,D__,Q__); 113% solution 114gb_:=geo_gbasis(polys_,vars_); 115result_:=geo_normalf(con_,gb_,vars_); 116 117 118% Example CircumCenter_1 119% 120% The problem: 121% The intersection point of the midpoint perpendiculars is the 122% center of the circumscribed circle. 123% 124% The solution: 125 126parameters_:=List(a1, a2, b1, b2, c1, c2); 127% Points 128A__:=Point(a1,a2); 129B__:=Point(b1,b2); 130C__:=Point(c1,c2); 131% coordinates 132M__:=intersection_point(p_bisector(A__,B__), 133 p_bisector(B__,C__)); 134% conclusion 135result_:=List( eq_dist(M__,A__,M__,B__), eq_dist(M__,A__,M__,C__) ); 136 137 138% Example EulerLine_1 139% 140% The problem: 141% Euler's line: The center $M$ of the circumscribed circle, 142% the orthocenter $H$ and the barycenter $S$ are collinear and $S$ 143% divides $MH$ with ratio 1:2. 144% 145% The solution: 146 147parameters_:=List(a1, a2, b1, b2, c1, c2); 148% Points 149A__:=Point(a1,a2); 150B__:=Point(b1,b2); 151C__:=Point(c1,c2); 152% coordinates 153S__:=intersection_point(median(A__,B__,C__),median(B__,C__,A__)); 154M__:=intersection_point(p_bisector(A__,B__), 155 p_bisector(B__,C__)); 156H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 157% conclusion 158result_:=List(is_collinear(M__,H__,S__), sqrdist(S__,fixedpoint(M__,H__,1/3))); 159 160 161% Example Brocard_3 162% 163% The problem: 164% Theorem about the Brocard points: 165% Let $\Delta\,ABC$ be a triangle. The circles $c_1$ through $A,B$ and 166% tangent to $g(AC)$, $c_2$ through $B,C$ and tangent to $g(AB)$, and 167% $c_3$ through $A,C$ and tangent to $g(BC)$ pass through a common 168% point. 169% 170% The solution: 171 172parameters_:=List(u1, u2); 173% Points 174A__:=Point(0,0); 175B__:=Point(1,0); 176C__:=Point(u1,u2); 177% coordinates 178M_1_:=intersection_point(altitude(A__,A__,C__),p_bisector(A__,B__)); 179M_2_:=intersection_point(altitude(B__,B__,A__),p_bisector(B__,C__)); 180M_3_:=intersection_point(altitude(C__,C__,B__),p_bisector(A__,C__)); 181c1_:=pc_circle(M_1_,A__); 182c2_:=pc_circle(M_2_,B__); 183c3_:=pc_circle(M_3_,C__); 184P__:=other_cc_point(B__,c1_,c2_); 185% conclusion 186result_:= on_circle(P__,c3_); 187 188 189% Example Feuerbach_1 190% 191% The problem: 192% Feuerbach's circle or nine-point circle: The midpoint $N$ of $MH$ is 193% the center of a circle that passes through nine special points, the 194% three pedal points of the altitudes, the midpoints of the sides of the 195% triangle and the midpoints of the upper parts of the three altitudes. 196% 197% The solution: 198 199parameters_:=List(u1, u2, u3); 200% Points 201A__:=Point(0,0); 202B__:=Point(u1,0); 203C__:=Point(u2,u3); 204% coordinates 205H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 206D__:=intersection_point(pp_line(A__,B__),pp_line(H__,C__)); 207M__:=intersection_point(p_bisector(A__,B__), 208 p_bisector(B__,C__)); 209N__:=midpoint(M__,H__); 210% conclusion 211result_:=List( eq_dist(N__,midpoint(A__,B__),N__,midpoint(B__,C__)), 212 eq_dist(N__,midpoint(A__,B__),N__,midpoint(H__,C__)), 213 eq_dist(N__,midpoint(A__,B__),N__,D__) ); 214 215 216% Example FeuerbachTangency_1 217% 218% The problem: 219% For an arbitrary triangle $\Delta\,ABC$ Feuerbach's circle (nine-point 220% circle) is tangent to its 4 tangent circles. 221% 222% The solution: 223 224vars_:=List(x1, x2); 225parameters_:=List(u1, u2); 226% Points 227A__:=Point(0,0); 228B__:=Point(2,0); 229C__:=Point(u1,u2); 230P__:=Point(x1,x2); 231% coordinates 232M__:=intersection_point(p_bisector(A__,B__), p_bisector(B__,C__)); 233H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 234N__:=midpoint(M__,H__); 235c1_:=pc_circle(N__,midpoint(A__,B__)); 236Q__:=pedalpoint(P__,pp_line(A__,B__)); 237% polynomials 238polys_:=List(on_bisector(P__,A__,B__,C__), on_bisector(P__,B__,C__,A__)); 239% conclusion 240con_:=is_cc_tangent(pc_circle(P__,Q__),c1_); 241% solution 242gb_:=geo_gbasis(polys_,vars_); 243result_:=geo_normalf(con_,gb_,vars_); 244 245 246% Example GeneralizedFermatPoint_1 247% 248% The problem: 249% A generalized theorem about Napoleon triangles: 250% Let $\Delta\,ABC$ be an arbitrary triangle and $P,Q$ and $R$ the third 251% vertex of isosceles triangles with equal base angles erected 252% externally on the sides $BC, AC$ and $AB$ of the triangle. Then the 253% lines $g(AP), g(BQ)$ and $g(CR)$ pass through a common point. 254% 255% The solution: 256 257vars_:=List(x1, x2, x3, x4, x5); 258parameters_:=List(u1, u2, u3); 259% Points 260A__:=Point(0,0); 261B__:=Point(2,0); 262C__:=Point(u1,u2); 263P__:=Point(x1,x2); 264Q__:=Point(x3,x4); 265R__:=Point(x5,u3); 266% polynomials 267polys_:=List(eq_dist(P__,B__,P__,C__), 268 eq_dist(Q__,A__,Q__,C__), 269 eq_dist(R__,A__,R__,B__), 270 eq_angle(R__,A__,B__,P__,B__,C__), 271 eq_angle(Q__,C__,A__,P__,B__,C__)); 272% conclusion 273con_:=is_concurrent(pp_line(A__,P__), pp_line(B__,Q__), pp_line(C__,R__)); 274% solution 275sol_:=geo_solve(polys_,vars_); 276result_:=geo_eval(con_,sol_); 277 278 279% Example TaylorCircle_1 280% 281% The problem: 282% Let $\Delta\,ABC$ be an arbitrary triangle. Consider the three 283% altitude pedal points and the pedal points of the perpendiculars from 284% these points onto the the opposite sides of the triangle. Show that 285% these 6 points are on a common circle, the {\em Taylor circle}. 286% 287% The solution: 288 289parameters_:=List(u1, u2, u3); 290% Points 291A__:=Point(u1,0); 292B__:=Point(u2,0); 293C__:=Point(0,u3); 294% coordinates 295P__:=pedalpoint(A__,pp_line(B__,C__)); 296Q__:=pedalpoint(B__,pp_line(A__,C__)); 297R__:=pedalpoint(C__,pp_line(A__,B__)); 298P_1_:=pedalpoint(P__,pp_line(A__,B__)); 299P_2_:=pedalpoint(P__,pp_line(A__,C__)); 300Q_1_:=pedalpoint(Q__,pp_line(A__,B__)); 301Q_2_:=pedalpoint(Q__,pp_line(B__,C__)); 302R_1_:=pedalpoint(R__,pp_line(A__,C__)); 303R_2_:=pedalpoint(R__,pp_line(B__,C__)); 304% conclusion 305result_:=List( is_concyclic(P_1_,P_2_,Q_1_,Q_2_), 306 is_concyclic(P_1_,P_2_,Q_1_,R_1_), 307 is_concyclic(P_1_,P_2_,Q_1_,R_2_)); 308 309 310% Example Miquel_1 311% 312% The problem: 313% Miquels theorem: Let $\Delta\,ABC$ be a triangle. Fix arbitrary points 314% $P,Q,R$ on the sides $AB, BC, AC$. Then the three circles through each 315% vertex and the chosen points on adjacent sides pass through a common 316% point. 317% 318% The solution: 319 320parameters_:=List(c1, c2, u1, u2, u3); 321% Points 322A__:=Point(0,0); 323B__:=Point(1,0); 324C__:=Point(c1,c2); 325% coordinates 326P__:=varpoint(A__,B__,u1); 327Q__:=varpoint(B__,C__,u2); 328R__:=varpoint(A__,C__,u3); 329X__:=other_cc_point(P__,p3_circle(A__,P__,R__),p3_circle(B__,P__,Q__)); 330% conclusion 331result_:=on_circle(X__,p3_circle(C__,Q__,R__)); 332 333 334% Example PappusPoint_1 335% 336% The problem: 337% Let $A,B,C$ and $P,Q,R$ be two triples of collinear points. Then by 338% the Theorem of Pappus the intersection points $g(AQ)\wedge g(BP), 339% g(AR)\wedge g(CP)$ and $g(BR)\wedge g(CQ)$ are collinear. 340% 341% Permuting $P,Q,R$ we get six such {\em Pappus lines}. Those 342% corresponding to even resp. odd permutations are concurrent. 343% 344% The solution: 345 346parameters_:=List(u1, u2, u3, u4, u5, u6, u7, u8); 347% Points 348A__:=Point(u1,0); 349B__:=Point(u2,0); 350P__:=Point(u4,u5); 351Q__:=Point(u6,u7); 352% coordinates 353C__:=varpoint(A__,B__,u3); 354R__:=varpoint(P__,Q__,u8); 355% conclusion 356result_:=is_concurrent(pappus_line(A__,B__,C__,P__,Q__,R__), 357 pappus_line(A__,B__,C__,Q__,R__,P__), 358 pappus_line(A__,B__,C__,R__,P__,Q__)); 359 360 361% Example IMO/36_1 362% 363% The problem: 364% Let $A,B,C,D$ be four distinct points on a line, in that order. The 365% circles with diameters $AC$ and $BD$ intersect at the points $X$ and 366% $Y$. The line $XY$ meets $BC$ at the point $Z$. Let $P$ be a point on 367% the line $XY$ different from $Z$. The line $CP$ intersects the circle 368% with diameter $AC$ at the points $C$ and $M$, and the line $BP$ 369% intersects the circle with diameter $BD$ at the points $B$ and 370% $N$. Prove that the lines $AM, DN$ and $XY$ are concurrent. 371% 372% The solution: 373 374vars_:=List(x1, x2, x3, x4, x5, x6); 375parameters_:=List(u1, u2, u3); 376% Points 377X__:=Point(0,1); 378Y__:=Point(0,-1); 379M__:=Point(x1,x2); 380N__:=Point(x3,x4); 381% coordinates 382P__:=varpoint(X__,Y__,u3); 383Z__:=midpoint(X__,Y__); 384l_:=p_bisector(X__,Y__); 385B__:=line_slider(l_,u1); 386C__:=line_slider(l_,u2); 387A__:=line_slider(l_,x5); 388D__:=line_slider(l_,x6); 389% polynomials 390polys_:=List(is_concyclic(X__,Y__,B__,N__), is_concyclic(X__,Y__,C__,M__), 391 is_concyclic(X__,Y__,B__,D__), is_concyclic(X__,Y__,C__,A__), 392 is_collinear(B__,P__,N__), is_collinear(C__,P__,M__)); 393% constraints 394nondeg_:=List(x5-u2,x1-u2,x6-u1,x3-u1); 395% conclusion 396con_:=is_concurrent(pp_line(A__,M__),pp_line(D__,N__),pp_line(X__,Y__)); 397% solution 398sol_:=geo_solveconstrained(polys_,vars_,nondeg_); 399result_:=geo_eval(con_,sol_); 400 401 402% Example IMO/43_2 403% 404% The problem: 405% 406% No verbal problem description available 407% 408% The solution: 409 410vars_:=List(x1, x2); 411parameters_:=List(u1); 412% Points 413B__:=Point(-1,0); 414C__:=Point(1,0); 415% coordinates 416O__:=midpoint(B__,C__); 417gamma_:=pc_circle(O__,B__); 418D__:=circle_slider(O__,B__,u1); 419E__:=circle_slider(O__,B__,x1); 420F__:=circle_slider(O__,B__,x2); 421A__:=sym_point(B__,pp_line(O__,D__)); 422J__:=intersection_point(pp_line(A__,C__), par_line(O__, pp_line(A__,D__))); 423m_:=p_bisector(O__,A__); 424P_1_:=pedalpoint(J__,m_); 425P_2_:=pedalpoint(J__,pp_line(C__,E__)); 426P_3_:=pedalpoint(J__,pp_line(C__,F__)); 427% polynomials 428polys_:=List(on_line(E__,m_), on_line(F__,m_)); 429% constraints 430nondegs_:=List(x1-x2); 431% conclusion 432con_:=List(eq_dist(J__,P_1_,J__,P_2_), eq_dist(J__,P_1_,J__,P_3_)); 433% solution 434sol_:=geo_solveconstrained(polys_,vars_,nondegs_); 435result_:=geo_simplify(geo_eval(con_,sol_)); 436 437showtime; 438 439end; 440