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