1% GeoProver test file for Reduce, created on Jan 18 2003 2load cali,geoprover; 3 4 5off nat; 6 7 on echo; 8 9 10 11% The following "in" fails in the test harness that I use at present and 12% so I have put the contents of the file that would have been read in-line 13% in the test script. 14 15%in "$reduce/packages/geometry/supp.red"$ 16 17%############################################################### 18% 19% FILE: supp.red 20% AUTHOR: graebe 21% CREATED: 2/2002 22% PURPOSE: Interface for the extended GEO syntax to Reduce 23% VERSION: $Id: supp.red,v 1.1 2002/12/26 16:27:22 compalg Exp $ 24 25 26% Redistribution and use in source and binary forms, with or without 27% modification, are permitted provided that the following conditions are met: 28% 29% * Redistributions of source code must retain the relevant copyright 30% notice, this list of conditions and the following disclaimer. 31% * Redistributions in binary form must reproduce the above copyright 32% notice, this list of conditions and the following disclaimer in the 33% documentation and/or other materials provided with the distribution. 34% 35% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" 36% AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, 37% THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR 38% PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNERS OR 39% CONTRIBUTORS 40% BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 41% CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF 42% SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS 43% INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN 44% CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 45% ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 46% POSSIBILITY OF SUCH DAMAGE. 47% 48 49algebraic procedure geo_simplify u; u; 50 51 52geo_simplify$ 53 54algebraic procedure geo_normal u; u; 55 56 57geo_normal$ 58 59algebraic procedure geo_subs(a,b,c); sub(a=b,c); 60 61 62geo_subs$ 63 64 65algebraic procedure geo_gbasis(polys,vars); 66 begin 67 setring(vars,{},lex); 68 setideal(uhu,polys); 69 return gbasis uhu; 70 end; 71 72 73geo_gbasis$ 74 75 76algebraic procedure geo_groebfactor(polys,vars,nondeg); 77 begin 78 setring(vars,{},lex); 79 return groebfactor(polys,nondeg); 80 end; 81 82 83geo_groebfactor$ 84 85 86algebraic procedure geo_normalf(p,polys,vars); 87 begin 88 setring(vars,{},lex); 89 return p mod polys; 90 end; 91 92 93geo_normalf$ 94 95 96algebraic procedure geo_eliminate(polys,vars,elivars); 97 begin 98 setring(vars,{},lex); 99 return eliminate(polys,elivars); 100 end; 101 102 103geo_eliminate$ 104 105 106algebraic procedure geo_solve(polys,vars); 107 solve(polys,vars); 108 109 110geo_solve$ 111 112 113algebraic procedure geo_solveconstrained(polys,vars,nondegs); 114 begin scalar u; 115 setring(vars,{},lex); 116 u:=groebfactor(polys,nondegs); 117 return for each x in u join solve(x,vars); 118 end; 119 120 121geo_solveconstrained$ 122 123 124algebraic procedure geo_eval(con,sol); 125 for each x in sol collect sub(x,con); 126 127 128geo_eval$ 129 130 131% End of what was in supp.red 132 133 134 135 136 137% Example Arnon 138% 139% The problem: 140% Let $ABCD$ be a square and $P$ a point on the line parallel to $BD$ 141% through $C$ such that $l(BD)=l(BP)$, where $l(BD)$ denotes the 142% distance between $B$ and $D$. Let $Q$ be the intersection point of 143% $BF$ and $CD$. Show that $l(DP)=l(DQ)$. 144% 145% The solution: 146 147vars_:=List(x1, x2, x3); 148 149 150vars_ := {x1,x2,x3}$ 151 152% Points 153A__:=Point(0,0); 154 155 156a__ := {0,0}$ 157 B__:=Point(1,0); 158 159 160b__ := {1,0}$ 161 P__:=Point(x1,x2); 162 163 164p__ := {x1,x2}$ 165 166% coordinates 167D__:=rotate(A__,B__,1/2); 168 169 170d__ := {0,1}$ 171 172C__:=par_point(D__,A__,B__); 173 174 175c__ := {1,1}$ 176 177Q__:=varpoint(D__,C__,x3); 178 179 180q__ := {x3,1}$ 181 182% polynomials 183polys_:=List(on_line(P__,par_line(C__,pp_line(B__,D__))), 184 eq_dist(B__,D__,B__,P__), on_line(Q__,pp_line(B__,P__))); 185 186 187polys_ := {x1 + x2 - 2, 188 - x1**2 + 2*x1 - x2**2 + 1, 189 - x1 + x2*x3 - x2 + 1}$ 190 191% conclusion 192con_:=eq_dist(D__,P__,D__,Q__); 193 194 195con_ := x1**2 + x2**2 - 2*x2 - x3**2 + 1$ 196 197% solution 198gb_:=geo_gbasis(polys_,vars_); 199 200 201gb_ := {x3**2 + 2*x3 - 2,2*x2 - x3 - 2,2*x1 + x3 - 2}$ 202 203result_:=geo_normalf(con_,gb_,vars_); 204 205 206result_ := 0$ 207 208 209 210% Example CircumCenter_1 211% 212% The problem: 213% The intersection point of the midpoint perpendiculars is the 214% center of the circumscribed circle. 215% 216% The solution: 217 218parameters_:=List(a1, a2, b1, b2, c1, c2); 219 220 221parameters_ := {a1, 222a2, 223b1, 224b2, 225c1, 226c2}$ 227 228% Points 229A__:=Point(a1,a2); 230 231 232a__ := {a1,a2}$ 233 234B__:=Point(b1,b2); 235 236 237b__ := {b1,b2}$ 238 239C__:=Point(c1,c2); 240 241 242c__ := {c1,c2}$ 243 244% coordinates 245M__:=intersection_point(p_bisector(A__,B__), 246 p_bisector(B__,C__)); 247 248 249m__ := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1 250**2 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - 251a2*b1 + a2*c1 + b1*c2 - b2*c1)), 252( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 + 253 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1 254 + a2*c1 + b1*c2 - b2*c1))}$ 255 256% conclusion 257result_:=List( eq_dist(M__,A__,M__,B__), eq_dist(M__,A__,M__,C__) ); 258 259 260result_ := {0,0}$ 261 262 263 264% Example EulerLine_1 265% 266% The problem: 267% Euler's line: The center $M$ of the circumscribed circle, 268% the orthocenter $H$ and the barycenter $S$ are collinear and $S$ 269% divides $MH$ with ratio 1:2. 270% 271% The solution: 272 273parameters_:=List(a1, a2, b1, b2, c1, c2); 274 275 276parameters_ := {a1, 277a2, 278b1, 279b2, 280c1, 281c2}$ 282 283% Points 284A__:=Point(a1,a2); 285 286 287a__ := {a1,a2}$ 288 289B__:=Point(b1,b2); 290 291 292b__ := {b1,b2}$ 293 294C__:=Point(c1,c2); 295 296 297c__ := {c1,c2}$ 298 299% coordinates 300S__:=intersection_point(median(A__,B__,C__),median(B__,C__,A__)); 301 302 303s__ := {(a1 + b1 + c1)/3,(a2 + b2 + c2)/3}$ 304 305M__:=intersection_point(p_bisector(A__,B__), 306 p_bisector(B__,C__)); 307 308 309m__ := {(a1**2*b2 - a1**2*c2 + a2**2*b2 - a2**2*c2 - a2*b1**2 - a2*b2**2 + a2*c1 310**2 + a2*c2**2 + b1**2*c2 + b2**2*c2 - b2*c1**2 - b2*c2**2)/(2*(a1*b2 - a1*c2 - 311a2*b1 + a2*c1 + b1*c2 - b2*c1)), 312( - a1**2*b1 + a1**2*c1 + a1*b1**2 + a1*b2**2 - a1*c1**2 - a1*c2**2 - a2**2*b1 + 313 a2**2*c1 - b1**2*c1 + b1*c1**2 + b1*c2**2 - b2**2*c1)/(2*(a1*b2 - a1*c2 - a2*b1 314 + a2*c1 + b1*c2 - b2*c1))}$ 315 316H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 317 318 319h__ := {( - a1*a2*b1 + a1*a2*c1 + a1*b1*b2 - a1*c1*c2 - a2**2*b2 + a2**2*c2 + a2 320*b2**2 - a2*c2**2 - b1*b2*c1 + b1*c1*c2 - b2**2*c2 + b2*c2**2)/(a1*b2 - a1*c2 - 321a2*b1 + a2*c1 + b1*c2 - b2*c1), 322(a1**2*b1 - a1**2*c1 + a1*a2*b2 - a1*a2*c2 - a1*b1**2 + a1*c1**2 - a2*b1*b2 + a2 323*c1*c2 + b1**2*c1 + b1*b2*c2 - b1*c1**2 - b2*c1*c2)/(a1*b2 - a1*c2 - a2*b1 + a2* 324c1 + b1*c2 - b2*c1)}$ 325 326% conclusion 327result_:=List(is_collinear(M__,H__,S__), sqrdist(S__,fixedpoint(M__,H__,1/3))); 328 329 330result_ := {0,0}$ 331 332 333 334% Example Brocard_3 335% 336% The problem: 337% Theorem about the Brocard points: 338% Let $\Delta\,ABC$ be a triangle. The circles $c_1$ through $A,B$ and 339% tangent to $g(AC)$, $c_2$ through $B,C$ and tangent to $g(AB)$, and 340% $c_3$ through $A,C$ and tangent to $g(BC)$ pass through a common 341% point. 342% 343% The solution: 344 345parameters_:=List(u1, u2); 346 347 348parameters_ := {u1,u2}$ 349 350% Points 351A__:=Point(0,0); 352 353 354a__ := {0,0}$ 355 356B__:=Point(1,0); 357 358 359b__ := {1,0}$ 360 361C__:=Point(u1,u2); 362 363 364c__ := {u1,u2}$ 365 366% coordinates 367M_1_:=intersection_point(altitude(A__,A__,C__),p_bisector(A__,B__)); 368 369 370m_1_ := {1/2,( - u1)/(2*u2)}$ 371 372M_2_:=intersection_point(altitude(B__,B__,A__),p_bisector(B__,C__)); 373 374 375m_2_ := {1,(u1**2 - 2*u1 + u2**2 + 1)/(2*u2)}$ 376 377M_3_:=intersection_point(altitude(C__,C__,B__),p_bisector(A__,C__)); 378 379 380m_3_ := {( - u1**2 + 2*u1 - u2**2)/2,(u1**3 - u1**2 + u1*u2**2 + u2**2)/(2*u2)}$ 381 382c1_:=pc_circle(M_1_,A__); 383 384 385c1_ := {u2, - u2,u1,0}$ 386 387c2_:=pc_circle(M_2_,B__); 388 389 390c2_ := {u2, - 2*u2, - u1**2 + 2*u1 - u2**2 - 1,u2}$ 391 392c3_:=pc_circle(M_3_,C__); 393 394 395c3_ := {u2, 396u2*(u1**2 - 2*u1 + u2**2), 397 - u1**3 + u1**2 - u1*u2**2 - u2**2, 3980}$ 399 400P__:=other_cc_point(B__,c1_,c2_); 401 402 403p__ := {(u1**3 - u1**2 + u1*u2**2 + u1 + u2**2)/(u1**4 - 2*u1**3 + 2*u1**2*u2**2 404 + 3*u1**2 - 2*u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1), 405(u2*(u1**2 - 2*u1 + u2**2 + 1))/(u1**4 - 2*u1**3 + 2*u1**2*u2**2 + 3*u1**2 - 2* 406u1*u2**2 - 2*u1 + u2**4 + 3*u2**2 + 1)}$ 407 408% conclusion 409result_:= on_circle(P__,c3_); 410 411 412result_ := 0$ 413 414 415 416% Example Feuerbach_1 417% 418% The problem: 419% Feuerbach's circle or nine-point circle: The midpoint $N$ of $MH$ is 420% the center of a circle that passes through nine special points, the 421% three pedal points of the altitudes, the midpoints of the sides of the 422% triangle and the midpoints of the upper parts of the three altitudes. 423% 424% The solution: 425 426parameters_:=List(u1, u2, u3); 427 428 429parameters_ := {u1,u2,u3}$ 430 431% Points 432A__:=Point(0,0); 433 434 435a__ := {0,0}$ 436 437B__:=Point(u1,0); 438 439 440b__ := {u1,0}$ 441 442C__:=Point(u2,u3); 443 444 445c__ := {u2,u3}$ 446 447% coordinates 448H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 449 450 451h__ := {u2,(u2*(u1 - u2))/u3}$ 452 453D__:=intersection_point(pp_line(A__,B__),pp_line(H__,C__)); 454 455 456d__ := {u2,0}$ 457 458M__:=intersection_point(p_bisector(A__,B__), 459 p_bisector(B__,C__)); 460 461 462m__ := {u1/2,( - u1*u2 + u2**2 + u3**2)/(2*u3)}$ 463 464N__:=midpoint(M__,H__); 465 466 467n__ := {(u1 + 2*u2)/4,(u1*u2 - u2**2 + u3**2)/(4*u3)}$ 468 469% conclusion 470result_:=List( eq_dist(N__,midpoint(A__,B__),N__,midpoint(B__,C__)), 471 eq_dist(N__,midpoint(A__,B__),N__,midpoint(H__,C__)), 472 eq_dist(N__,midpoint(A__,B__),N__,D__) ); 473 474 475result_ := {0,0,0}$ 476 477 478 479% Example FeuerbachTangency_1 480% 481% The problem: 482% For an arbitrary triangle $\Delta\,ABC$ Feuerbach's circle (nine-point 483% circle) is tangent to its 4 tangent circles. 484% 485% The solution: 486 487vars_:=List(x1, x2); 488 489 490vars_ := {x1,x2}$ 491 492parameters_:=List(u1, u2); 493 494 495parameters_ := {u1,u2}$ 496 497% Points 498A__:=Point(0,0); 499 500 501a__ := {0,0}$ 502 503B__:=Point(2,0); 504 505 506b__ := {2,0}$ 507 508C__:=Point(u1,u2); 509 510 511c__ := {u1,u2}$ 512 513P__:=Point(x1,x2); 514 515 516p__ := {x1,x2}$ 517 518% coordinates 519M__:=intersection_point(p_bisector(A__,B__), p_bisector(B__,C__)); 520 521 522m__ := {1,(u1**2 - 2*u1 + u2**2)/(2*u2)}$ 523 524H__:=intersection_point(altitude(A__,B__,C__),altitude(B__,C__,A__)); 525 526 527h__ := {u1,(u1*( - u1 + 2))/u2}$ 528 529N__:=midpoint(M__,H__); 530 531 532n__ := {(u1 + 1)/2,( - u1**2 + 2*u1 + u2**2)/(4*u2)}$ 533 534c1_:=pc_circle(N__,midpoint(A__,B__)); 535 536 537c1_ := {2*u2, 538 - 2*u2*(u1 + 1), 539u1**2 - 2*u1 - u2**2, 5402*u1*u2}$ 541 542Q__:=pedalpoint(P__,pp_line(A__,B__)); 543 544 545q__ := {x1,0}$ 546 547% polynomials 548polys_:=List(on_bisector(P__,A__,B__,C__), on_bisector(P__,B__,C__,A__)); 549 550 551polys_ := {2*( - 2*u1*x1*x2 + 4*u1*x2 + u2*x1**2 - 4*u2*x1 - u2*x2**2 + 4*u2 + 4 552*x1*x2 - 8*x2), 5532*( - u1**3*x2 + u1**2*u2*x1 - u1**2*u2 + u1**2*x1*x2 + 2*u1**2*x2 - u1*u2**2*x2 554 - u1*u2*x1**2 + u1*u2*x2**2 - 2*u1*x1*x2 + u2**3*x1 - u2**3 - u2**2*x1*x2 + 2* 555u2**2*x2 + u2*x1**2 - u2*x2**2)}$ 556 557% conclusion 558con_:=is_cc_tangent(pc_circle(P__,Q__),c1_); 559 560 561con_ := 16*u2*( - u1**3*x1*x2 + u1**3*x2 + u1**2*u2*x1**2 - 2*u1**2*u2*x1 - u1** 5622*u2*x2**2 + u1**2*u2 + u1**2*x1**2*x2 + u1**2*x1*x2 - 2*u1**2*x2 + u1*u2**2*x1* 563x2 - u1*u2**2*x2 - 2*u1*u2*x1**3 + 4*u1*u2*x1**2 - 2*u1*u2*x1 + 2*u1*u2*x2**2 - 5642*u1*x1**2*x2 + 2*u1*x1*x2 - u2**2*x1**2*x2 + u2**2*x1*x2 + u2*x1**4 - 2*u2*x1** 5653 + u2*x1**2 - u2*x2**2)$ 566 567% solution 568gb_:=geo_gbasis(polys_,vars_); 569 570 571gb_ := {u1**2*u2*x2**2 - 2*u1**2*x2**3 - 2*u1*u2*x2**2 + 4*u1*x2**3 + u2**3*x2** 5722 - u2**3 - 2*u2**2*x2**3 + 4*u2**2*x2 + u2*x2**4 - 4*u2*x2**2, 573 - u1**2*u2*x2 - 2*u1**2*x2**2 + u1*u2**2*x1 - u1*u2**2 + 2*u1*u2*x2 + 4*u1*x2** 5742 - u2**2*x1 - u2**2*x2**2 + 2*u2**2 + u2*x2**3 - 4*u2*x2}$ 575 576result_:=geo_normalf(con_,gb_,vars_); 577 578 579result_ := 0$ 580 581 582 583% Example GeneralizedFermatPoint_1 584% 585% The problem: 586% A generalized theorem about Napoleon triangles: 587% Let $\Delta\,ABC$ be an arbitrary triangle and $P,Q$ and $R$ the third 588% vertex of isosceles triangles with equal base angles erected 589% externally on the sides $BC, AC$ and $AB$ of the triangle. Then the 590% lines $g(AP), g(BQ)$ and $g(CR)$ pass through a common point. 591% 592% The solution: 593 594vars_:=List(x1, x2, x3, x4, x5); 595 596 597vars_ := {x1, 598x2, 599x3, 600x4, 601x5}$ 602 603parameters_:=List(u1, u2, u3); 604 605 606parameters_ := {u1,u2,u3}$ 607 608% Points 609A__:=Point(0,0); 610 611 612a__ := {0,0}$ 613 614B__:=Point(2,0); 615 616 617b__ := {2,0}$ 618 619C__:=Point(u1,u2); 620 621 622c__ := {u1,u2}$ 623 624P__:=Point(x1,x2); 625 626 627p__ := {x1,x2}$ 628 629Q__:=Point(x3,x4); 630 631 632q__ := {x3,x4}$ 633 634R__:=Point(x5,u3); 635 636 637r__ := {x5,u3}$ 638 639% polynomials 640polys_:=List(eq_dist(P__,B__,P__,C__), 641 eq_dist(Q__,A__,Q__,C__), 642 eq_dist(R__,A__,R__,B__), 643 eq_angle(R__,A__,B__,P__,B__,C__), 644 eq_angle(Q__,C__,A__,P__,B__,C__)); 645 646 647polys_ := { - u1**2 + 2*u1*x1 - u2**2 + 2*u2*x2 - 4*x1 + 4, 648 - u1**2 + 2*u1*x3 - u2**2 + 2*u2*x4, 6494*(x5 - 1), 650(u1*u3*x1 - 2*u1*u3 - u1*x2*x5 + u2*u3*x2 + u2*x1*x5 - 2*u2*x5 - 2*u3*x1 + 4*u3 651+ 2*x2*x5)/(x5*(u1*x1 - 2*u1 + u2*x2 - 2*x1 + 4)), 652( - u1**3*x2 + u1**2*u2*x1 - 2*u1**2*u2 - u1**2*x1*x4 + u1**2*x2*x3 + 2*u1**2*x2 653 + 2*u1**2*x4 - u1*u2**2*x2 + 2*u1*x1*x4 - 2*u1*x2*x3 - 4*u1*x4 + u2**3*x1 - 2* 654u2**3 - u2**2*x1*x4 + u2**2*x2*x3 + 2*u2**2*x2 + 2*u2**2*x4 - 2*u2*x1*x3 - 2*u2* 655x2*x4 + 4*u2*x3)/(u1**3*x1 - 2*u1**3 + u1**2*u2*x2 - u1**2*x1*x3 - 2*u1**2*x1 + 6562*u1**2*x3 + 4*u1**2 + u1*u2**2*x1 - 2*u1*u2**2 - u1*u2*x1*x4 - u1*u2*x2*x3 + 2* 657u1*u2*x4 + 2*u1*x1*x3 - 4*u1*x3 + u2**3*x2 - 2*u2**2*x1 - u2**2*x2*x4 + 4*u2**2 658+ 2*u2*x1*x4 - 4*u2*x4)}$ 659 660% conclusion 661con_:=is_concurrent(pp_line(A__,P__), pp_line(B__,Q__), pp_line(C__,R__)); 662 663 664con_ := - u1*u3*x1*x4 + u1*u3*x2*x3 - 2*u1*u3*x2 + 2*u1*x2*x4 + u2*x1*x4*x5 - 2 665*u2*x1*x4 - u2*x2*x3*x5 + 2*u2*x2*x5 + 2*u3*x1*x4 - 2*x2*x4*x5$ 666 667% solution 668sol_:=geo_solve(polys_,vars_); 669 670 671sol_ := {{x1=(u1 - u2*u3 + 2)/2, 672x2=(u1*u3 + u2 - 2*u3)/2, 673x3=(u1 + u2*u3)/2, 674x4=( - u1*u3 + u2)/2, 675x5=1}}$ 676 677result_:=geo_eval(con_,sol_); 678 679 680result_ := {0}$ 681 682 683 684% Example TaylorCircle_1 685% 686% The problem: 687% Let $\Delta\,ABC$ be an arbitrary triangle. Consider the three 688% altitude pedal points and the pedal points of the perpendiculars from 689% these points onto the the opposite sides of the triangle. Show that 690% these 6 points are on a common circle, the {\em Taylor circle}. 691% 692% The solution: 693 694parameters_:=List(u1, u2, u3); 695 696 697parameters_ := {u1,u2,u3}$ 698 699% Points 700A__:=Point(u1,0); 701 702 703a__ := {u1,0}$ 704 705B__:=Point(u2,0); 706 707 708b__ := {u2,0}$ 709 710C__:=Point(0,u3); 711 712 713c__ := {0,u3}$ 714 715% coordinates 716P__:=pedalpoint(A__,pp_line(B__,C__)); 717 718 719p__ := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2), 720(u2*u3*( - u1 + u2))/(u2**2 + u3**2)}$ 721 722Q__:=pedalpoint(B__,pp_line(A__,C__)); 723 724 725q__ := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2), 726(u1*u3*(u1 - u2))/(u1**2 + u3**2)}$ 727 728R__:=pedalpoint(C__,pp_line(A__,B__)); 729 730 731r__ := {0,0}$ 732 733P_1_:=pedalpoint(P__,pp_line(A__,B__)); 734 735 736p_1_ := {(u2*(u1*u2 + u3**2))/(u2**2 + u3**2),0}$ 737 738P_2_:=pedalpoint(P__,pp_line(A__,C__)); 739 740 741p_2_ := {(u1*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 + 742 u2**2*u3**2 + u3**4), 743(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3 744**4)}$ 745 746Q_1_:=pedalpoint(Q__,pp_line(A__,B__)); 747 748 749q_1_ := {(u1*(u1*u2 + u3**2))/(u1**2 + u3**2),0}$ 750 751Q_2_:=pedalpoint(Q__,pp_line(B__,C__)); 752 753 754q_2_ := {(u2*(u1**2*u2**2 + 2*u1*u2*u3**2 + u3**4))/(u1**2*u2**2 + u1**2*u3**2 + 755 u2**2*u3**2 + u3**4), 756(u3**3*(u1**2 - 2*u1*u2 + u2**2))/(u1**2*u2**2 + u1**2*u3**2 + u2**2*u3**2 + u3 757**4)}$ 758 759R_1_:=pedalpoint(R__,pp_line(A__,C__)); 760 761 762r_1_ := {(u1*u3**2)/(u1**2 + u3**2),(u1**2*u3)/(u1**2 + u3**2)}$ 763 764R_2_:=pedalpoint(R__,pp_line(B__,C__)); 765 766 767r_2_ := {(u2*u3**2)/(u2**2 + u3**2),(u2**2*u3)/(u2**2 + u3**2)}$ 768 769% conclusion 770result_:=List( is_concyclic(P_1_,P_2_,Q_1_,Q_2_), 771 is_concyclic(P_1_,P_2_,Q_1_,R_1_), 772 is_concyclic(P_1_,P_2_,Q_1_,R_2_)); 773 774 775result_ := {0,0,0}$ 776 777 778 779% Example Miquel_1 780% 781% The problem: 782% Miquels theorem: Let $\Delta\,ABC$ be a triangle. Fix arbitrary points 783% $P,Q,R$ on the sides $AB, BC, AC$. Then the three circles through each 784% vertex and the chosen points on adjacent sides pass through a common 785% point. 786% 787% The solution: 788 789parameters_:=List(c1, c2, u1, u2, u3); 790 791 792parameters_ := {c1, 793c2, 794u1, 795u2, 796u3}$ 797 798% Points 799A__:=Point(0,0); 800 801 802a__ := {0,0}$ 803 804B__:=Point(1,0); 805 806 807b__ := {1,0}$ 808 809C__:=Point(c1,c2); 810 811 812c__ := {c1,c2}$ 813 814% coordinates 815P__:=varpoint(A__,B__,u1); 816 817 818p__ := {u1,0}$ 819 820Q__:=varpoint(B__,C__,u2); 821 822 823q__ := {c1*u2 - u2 + 1,c2*u2}$ 824 825R__:=varpoint(A__,C__,u3); 826 827 828r__ := {c1*u3,c2*u3}$ 829 830X__:=other_cc_point(P__,p3_circle(A__,P__,R__),p3_circle(B__,P__,Q__)); 831 832 833x__ := {( - c1**4*u2*u3 + c1**4*u3**2 + c1**3*u1*u2 - c1**3*u1*u3 + 2*c1**3*u2* 834u3 - c1**3*u3 - 2*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 - 2*c1**2*u1*u2 - c1** 8352*u1*u3 + c1**2*u1 - c1**2*u2*u3 + c1**2*u3 + c1*c2**2*u1*u2 - c1*c2**2*u1*u3 + 8362*c1*c2**2*u2*u3 - c1*c2**2*u3 + c1*u1**2 + c1*u1*u2 - c1*u1 - c2**4*u2*u3 + c2 837**4*u3**2 - c2**2*u1*u3 + c2**2*u1 - c2**2*u2*u3 + c2**2*u3)/(c1**4*u2**2 - 2*c1 838**4*u2*u3 + c1**4*u3**2 - 4*c1**3*u2**2 + 4*c1**3*u2*u3 + 2*c1**3*u2 - 2*c1**3* 839u3 + 2*c1**2*c2**2*u2**2 - 4*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 + 2*c1**2* 840u1*u2 - 2*c1**2*u1*u3 + 6*c1**2*u2**2 - 2*c1**2*u2*u3 - 6*c1**2*u2 + 2*c1**2*u3 841+ c1**2 - 4*c1*c2**2*u2**2 + 4*c1*c2**2*u2*u3 + 2*c1*c2**2*u2 - 2*c1*c2**2*u3 - 8424*c1*u1*u2 + 2*c1*u1 - 4*c1*u2**2 + 6*c1*u2 - 2*c1 + c2**4*u2**2 - 2*c2**4*u2*u3 843 + c2**4*u3**2 + 2*c2**2*u1*u2 - 2*c2**2*u1*u3 + 2*c2**2*u2**2 - 2*c2**2*u2*u3 - 844 2*c2**2*u2 + 2*c2**2*u3 + c2**2 + u1**2 + 2*u1*u2 - 2*u1 + u2**2 - 2*u2 + 1), 845(c2*(c1**2*u1*u2 - c1**2*u1*u3 + c1**2*u3 - 2*c1*u1*u2 + c2**2*u1*u2 - c2**2*u1* 846u3 + c2**2*u3 + u1**2 + u1*u2 - u1))/(c1**4*u2**2 - 2*c1**4*u2*u3 + c1**4*u3**2 847- 4*c1**3*u2**2 + 4*c1**3*u2*u3 + 2*c1**3*u2 - 2*c1**3*u3 + 2*c1**2*c2**2*u2**2 848- 4*c1**2*c2**2*u2*u3 + 2*c1**2*c2**2*u3**2 + 2*c1**2*u1*u2 - 2*c1**2*u1*u3 + 6* 849c1**2*u2**2 - 2*c1**2*u2*u3 - 6*c1**2*u2 + 2*c1**2*u3 + c1**2 - 4*c1*c2**2*u2**2 850 + 4*c1*c2**2*u2*u3 + 2*c1*c2**2*u2 - 2*c1*c2**2*u3 - 4*c1*u1*u2 + 2*c1*u1 - 4* 851c1*u2**2 + 6*c1*u2 - 2*c1 + c2**4*u2**2 - 2*c2**4*u2*u3 + c2**4*u3**2 + 2*c2**2* 852u1*u2 - 2*c2**2*u1*u3 + 2*c2**2*u2**2 - 2*c2**2*u2*u3 - 2*c2**2*u2 + 2*c2**2*u3 853+ c2**2 + u1**2 + 2*u1*u2 - 2*u1 + u2**2 - 2*u2 + 1)}$ 854 855% conclusion 856result_:=on_circle(X__,p3_circle(C__,Q__,R__)); 857 858 859result_ := 0$ 860 861 862 863% Example PappusPoint_1 864% 865% The problem: 866% Let $A,B,C$ and $P,Q,R$ be two triples of collinear points. Then by 867% the Theorem of Pappus the intersection points $g(AQ)\wedge g(BP), 868% g(AR)\wedge g(CP)$ and $g(BR)\wedge g(CQ)$ are collinear. 869% 870% Permuting $P,Q,R$ we get six such {\em Pappus lines}. Those 871% corresponding to even resp. odd permutations are concurrent. 872% 873% The solution: 874 875parameters_:=List(u1, u2, u3, u4, u5, u6, u7, u8); 876 877 878parameters_ := {u1, 879u2, 880u3, 881u4, 882u5, 883u6, 884u7, 885u8}$ 886 887% Points 888A__:=Point(u1,0); 889 890 891a__ := {u1,0}$ 892 893B__:=Point(u2,0); 894 895 896b__ := {u2,0}$ 897 898P__:=Point(u4,u5); 899 900 901p__ := {u4,u5}$ 902 903Q__:=Point(u6,u7); 904 905 906q__ := {u6,u7}$ 907 908% coordinates 909C__:=varpoint(A__,B__,u3); 910 911 912c__ := { - u1*u3 + u1 + u2*u3,0}$ 913 914R__:=varpoint(P__,Q__,u8); 915 916 917r__ := { - u4*u8 + u4 + u6*u8, - u5*u8 + u5 + u7*u8}$ 918 919% conclusion 920result_:=is_concurrent(pappus_line(A__,B__,C__,P__,Q__,R__), 921 pappus_line(A__,B__,C__,Q__,R__,P__), 922 pappus_line(A__,B__,C__,R__,P__,Q__)); 923 924 925result_ := 0$ 926 927 928 929% Example IMO/36_1 930% 931% The problem: 932% Let $A,B,C,D$ be four distinct points on a line, in that order. The 933% circles with diameters $AC$ and $BD$ intersect at the points $X$ and 934% $Y$. The line $XY$ meets $BC$ at the point $Z$. Let $P$ be a point on 935% the line $XY$ different from $Z$. The line $CP$ intersects the circle 936% with diameter $AC$ at the points $C$ and $M$, and the line $BP$ 937% intersects the circle with diameter $BD$ at the points $B$ and 938% $N$. Prove that the lines $AM, DN$ and $XY$ are concurrent. 939% 940% The solution: 941 942vars_:=List(x1, x2, x3, x4, x5, x6); 943 944 945vars_ := {x1, 946x2, 947x3, 948x4, 949x5, 950x6}$ 951 952parameters_:=List(u1, u2, u3); 953 954 955parameters_ := {u1,u2,u3}$ 956 957% Points 958X__:=Point(0,1); 959 960 961x__ := {0,1}$ 962 963Y__:=Point(0,-1); 964 965 966y__ := {0,-1}$ 967 968M__:=Point(x1,x2); 969 970 971m__ := {x1,x2}$ 972 973N__:=Point(x3,x4); 974 975 976n__ := {x3,x4}$ 977 978% coordinates 979P__:=varpoint(X__,Y__,u3); 980 981 982p__ := {0, - 2*u3 + 1}$ 983 984Z__:=midpoint(X__,Y__); 985 986 987z__ := {0,0}$ 988 989l_:=p_bisector(X__,Y__); 990 991 992l_ := {0,1,0}$ 993 994B__:=line_slider(l_,u1); 995 996 997b__ := {u1,0}$ 998 999C__:=line_slider(l_,u2); 1000 1001 1002c__ := {u2,0}$ 1003 1004A__:=line_slider(l_,x5); 1005 1006 1007a__ := {x5,0}$ 1008 1009D__:=line_slider(l_,x6); 1010 1011 1012d__ := {x6,0}$ 1013 1014% polynomials 1015polys_:=List(is_concyclic(X__,Y__,B__,N__), is_concyclic(X__,Y__,C__,M__), 1016 is_concyclic(X__,Y__,B__,D__), is_concyclic(X__,Y__,C__,A__), 1017 is_collinear(B__,P__,N__), is_collinear(C__,P__,M__)); 1018 1019 1020polys_ := { - u1**2*x3 + u1*x3**2 + u1*x4**2 - u1 + x3, 1021 - u2**2*x1 + u2*x1**2 + u2*x2**2 - u2 + x1, 1022 - u1**2*x6 + u1*x6**2 - u1 + x6, 1023 - u2**2*x5 + u2*x5**2 - u2 + x5, 1024 - 2*u1*u3 - u1*x4 + u1 + 2*u3*x3 - x3, 1025 - 2*u2*u3 - u2*x2 + u2 + 2*u3*x1 - x1}$ 1026 1027% constraints 1028nondeg_:=List(x5-u2,x1-u2,x6-u1,x3-u1); 1029 1030 1031nondeg_ := { - u2 + x5, 1032 - u2 + x1, 1033 - u1 + x6, 1034 - u1 + x3}$ 1035 1036% conclusion 1037con_:=is_concurrent(pp_line(A__,M__),pp_line(D__,N__),pp_line(X__,Y__)); 1038 1039 1040con_ := - x1*x4*x6 + x2*x3*x5 - x2*x5*x6 + x4*x5*x6$ 1041 1042% solution 1043sol_:=geo_solveconstrained(polys_,vars_,nondeg_); 1044 1045 1046sol_ := {{x1=(4*u2*u3**2 - 4*u2*u3)/(u2**2 + 4*u3**2 - 4*u3 + 1), 1047x2=( - 2*u2**2*u3 + u2**2 - 2*u3 + 1)/(u2**2 + 4*u3**2 - 4*u3 + 1), 1048x3=(4*u1*u3**2 - 4*u1*u3)/(u1**2 + 4*u3**2 - 4*u3 + 1), 1049x4=( - 2*u1**2*u3 + u1**2 - 2*u3 + 1)/(u1**2 + 4*u3**2 - 4*u3 + 1), 1050x5=( - 1)/u2, 1051x6=( - 1)/u1}}$ 1052 1053result_:=geo_eval(con_,sol_); 1054 1055 1056result_ := {0}$ 1057 1058 1059 1060% Example IMO/43_2 1061% 1062% The problem: 1063% 1064% No verbal problem description available 1065% 1066% The solution: 1067 1068vars_:=List(x1, x2); 1069 1070 1071vars_ := {x1,x2}$ 1072 1073parameters_:=List(u1); 1074 1075 1076parameters_ := {u1}$ 1077 1078% Points 1079B__:=Point(-1,0); 1080 1081 1082b__ := {-1,0}$ 1083 1084C__:=Point(1,0); 1085 1086 1087c__ := {1,0}$ 1088 1089% coordinates 1090O__:=midpoint(B__,C__); 1091 1092 1093o__ := {0,0}$ 1094 1095gamma_:=pc_circle(O__,B__); 1096 1097 1098gamma_ := {1,0,0,-1}$ 1099 1100D__:=circle_slider(O__,B__,u1); 1101 1102 1103d__ := {( - u1**2 + 1)/(u1**2 + 1),(2*u1)/(u1**2 + 1)}$ 1104 1105E__:=circle_slider(O__,B__,x1); 1106 1107 1108e__ := {( - x1**2 + 1)/(x1**2 + 1),(2*x1)/(x1**2 + 1)}$ 1109 1110F__:=circle_slider(O__,B__,x2); 1111 1112 1113f__ := {( - x2**2 + 1)/(x2**2 + 1),(2*x2)/(x2**2 + 1)}$ 1114 1115A__:=sym_point(B__,pp_line(O__,D__)); 1116 1117 1118a__ := {( - u1**4 + 6*u1**2 - 1)/(u1**4 + 2*u1**2 + 1),(4*u1*(u1**2 - 1))/(u1**4 1119 + 2*u1**2 + 1)}$ 1120 1121J__:=intersection_point(pp_line(A__,C__), par_line(O__, pp_line(A__,D__))); 1122 1123 1124j__ := {(2*(3*u1**2 - 1))/(u1**4 + 2*u1**2 + 1),(2*u1*(u1**2 - 3))/(u1**4 + 2*u1 1125**2 + 1)}$ 1126 1127m_:=p_bisector(O__,A__); 1128 1129 1130m_ := {2*(u1**4 - 6*u1**2 + 1),8*u1*( - u1**2 + 1),u1**4 + 2*u1**2 + 1}$ 1131 1132P_1_:=pedalpoint(J__,m_); 1133 1134 1135p_1_ := {( - u1**8 + 20*u1**6 + 10*u1**4 - 12*u1**2 - 1)/(2*(u1**8 + 4*u1**6 + 6 1136*u1**4 + 4*u1**2 + 1)), 1137(4*u1**3*(u1**4 - 2*u1**2 - 3))/(u1**8 + 4*u1**6 + 6*u1**4 + 4*u1**2 + 1)}$ 1138 1139P_2_:=pedalpoint(J__,pp_line(C__,E__)); 1140 1141 1142p_2_ := {(u1**4 - 2*u1**3*x1 + 6*u1**2*x1**2 + 2*u1**2 + 6*u1*x1 - 2*x1**2 + 1)/ 1143(u1**4*x1**2 + u1**4 + 2*u1**2*x1**2 + 2*u1**2 + x1**2 + 1), 1144(u1**4*x1 + 2*u1**3 - 4*u1**2*x1 - 6*u1 + 3*x1)/(u1**4*x1**2 + u1**4 + 2*u1**2* 1145x1**2 + 2*u1**2 + x1**2 + 1)}$ 1146 1147P_3_:=pedalpoint(J__,pp_line(C__,F__)); 1148 1149 1150p_3_ := {(u1**4 - 2*u1**3*x2 + 6*u1**2*x2**2 + 2*u1**2 + 6*u1*x2 - 2*x2**2 + 1)/ 1151(u1**4*x2**2 + u1**4 + 2*u1**2*x2**2 + 2*u1**2 + x2**2 + 1), 1152(u1**4*x2 + 2*u1**3 - 4*u1**2*x2 - 6*u1 + 3*x2)/(u1**4*x2**2 + u1**4 + 2*u1**2* 1153x2**2 + 2*u1**2 + x2**2 + 1)}$ 1154 1155% polynomials 1156polys_:=List(on_line(E__,m_), on_line(F__,m_)); 1157 1158 1159polys_ := {( - u1**4*x1**2 + 3*u1**4 - 16*u1**3*x1 + 14*u1**2*x1**2 - 10*u1**2 + 1160 16*u1*x1 - x1**2 + 3)/(x1**2 + 1), 1161( - u1**4*x2**2 + 3*u1**4 - 16*u1**3*x2 + 14*u1**2*x2**2 - 10*u1**2 + 16*u1*x2 - 1162 x2**2 + 3)/(x2**2 + 1)}$ 1163 1164% constraints 1165nondegs_:=List(x1-x2); 1166 1167 1168nondegs_ := {x1 - x2}$ 1169 1170% conclusion 1171con_:=List(eq_dist(J__,P_1_,J__,P_2_), eq_dist(J__,P_1_,J__,P_3_)); 1172 1173 1174con_ := {(u1**8*x1**4 - 2*u1**8*x1**2 - 3*u1**8 + 16*u1**7*x1**3 + 16*u1**7*x1 - 1175 20*u1**6*x1**4 + 8*u1**6*x1**2 + 28*u1**6 - 112*u1**5*x1**3 - 112*u1**5*x1 + 94 1176*u1**4*x1**4 + 4*u1**4*x1**2 - 90*u1**4 + 240*u1**3*x1**3 + 240*u1**3*x1 - 132* 1177u1**2*x1**4 - 24*u1**2*x1**2 + 108*u1**2 - 144*u1*x1**3 - 144*u1*x1 + 9*x1**4 - 117818*x1**2 - 27)/(4*(u1**8*x1**4 + 2*u1**8*x1**2 + u1**8 + 4*u1**6*x1**4 + 8*u1**6 1179*x1**2 + 4*u1**6 + 6*u1**4*x1**4 + 12*u1**4*x1**2 + 6*u1**4 + 4*u1**2*x1**4 + 8* 1180u1**2*x1**2 + 4*u1**2 + x1**4 + 2*x1**2 + 1)), 1181(u1**8*x2**4 - 2*u1**8*x2**2 - 3*u1**8 + 16*u1**7*x2**3 + 16*u1**7*x2 - 20*u1**6 1182*x2**4 + 8*u1**6*x2**2 + 28*u1**6 - 112*u1**5*x2**3 - 112*u1**5*x2 + 94*u1**4*x2 1183**4 + 4*u1**4*x2**2 - 90*u1**4 + 240*u1**3*x2**3 + 240*u1**3*x2 - 132*u1**2*x2** 11844 - 24*u1**2*x2**2 + 108*u1**2 - 144*u1*x2**3 - 144*u1*x2 + 9*x2**4 - 18*x2**2 - 1185 27)/(4*(u1**8*x2**4 + 2*u1**8*x2**2 + u1**8 + 4*u1**6*x2**4 + 8*u1**6*x2**2 + 4 1186*u1**6 + 6*u1**4*x2**4 + 12*u1**4*x2**2 + 6*u1**4 + 4*u1**2*x2**4 + 8*u1**2*x2** 11872 + 4*u1**2 + x2**4 + 2*x2**2 + 1))}$ 1188 1189% solution 1190sol_:=geo_solveconstrained(polys_,vars_,nondegs_); 1191 1192 1193sol_ := {{x1=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 1194 - 14*u1**2 + 1), 1195x2=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1** 11962 + 1)}, 1197{x1=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1 1198**2 + 1), 1199x2=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14* 1200u1**2 + 1)}, 1201{x1=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14* 1202u1**2 + 1), 1203x2=(sqrt(3)*u1**4 + 2*sqrt(3)*u1**2 + sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14*u1** 12042 + 1)}, 1205{x1=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14* 1206u1**2 + 1), 1207x2=( - sqrt(3)*u1**4 - 2*sqrt(3)*u1**2 - sqrt(3) - 8*u1**3 + 8*u1)/(u1**4 - 14* 1208u1**2 + 1)}}$ 1209 1210result_:=geo_simplify(geo_eval(con_,sol_)); 1211 1212 1213result_ := {{0,0},{0,0},{0,0},{0,0}}$ 1214 1215 1216showtime; 1217 1218 1219 1220 1221end; 1222 1223Tested on x86_64-pc-windows CSL 1224Time (counter 1): 125 ms 1225 1226End of Lisp run after 0.12+0.06 seconds 1227real 0.33 1228user 0.03 1229sys 0.03 1230