Check-ins Using Download Hex

Artifact 20ce6d4ffee9c6b751981263f5c0c7e214624f217b255b17bafb0297cec85133:

% Author H.-G. Graebe | Univ. Leipzig | Version 6.9.1998
% graebe@informatik.uni-leipzig.de

comment 

Test suite for the package GEOMETRY 1.1

end comment;

algebraic;
load cali,geometry;
off nat;
on echo;
showtime;


% #####################
% Some one line proofs
% #####################

% A generic triangle ABC

A:=Point(a1,a2); B:=Point(b1,b2); C:=Point(c1,c2);

% Its midpoint perpendiculars have a point in common:

	concurrent(mp(a,b),mp(b,c),mp(c,a));
 
% This point

	M:=intersection_point(mp(a,b),mp(b,c));

% is the center of the circumscribed circle

	sqrdist(M,A) - sqrdist(M,B);	

% The altitutes intersection theorem

	concurrent(altitude(a,b,c),altitude(b,c,a),altitude(c,a,b));

% The median intersection theorem

	concurrent(median(a,b,c),median(b,c,a),median(c,a,b));

% Euler's line

        M:=intersection_point(mp(a,b),mp(b,c));
        H:=intersection_point(altitude(a,b,c),altitude(b,c,a));
        S:=intersection_point(median(a,b,c),median(b,c,a));

                collinear(M,H,S);
                sqrdist(S,varpoint(M,H,2/3));

% Feuerbach's circle

	% Choose a special coordinate system
	A:=Point(0,0); B:=Point(u1,0); C:=Point(u2,u3);

        M:=intersection_point(mp(a,b),mp(b,c));
        H:=intersection_point(altitude(a,b,c),altitude(b,c,a));
        N:=midpoint(M,H);

                sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(B,C));
                sqrdist(N,midpoint(A,B))-sqrdist(N,midpoint(H,C));

        D:=intersection_point(pp_line(A,B),pp_line(H,C));

                sqrdist(N,midpoint(A,B))-sqrdist(N,D);

clear_ndg(); clear(A,B,C,D,M,H,S,N);

% ############################# 
% Non-linear Geometric Objects
% #############################

% Bisector intersection theorem
 
A:=Point(0,0); B:=Point(1,0); C:=Point(u1,u2);
P:=Point(x1,x2);
 
polys:={
        point_on_bisector(P,A,B,C),
        point_on_bisector(P,B,C,A),
        point_on_bisector(P,C,A,B)};

con1:=num(sqrdist(P,pedalpoint(p,pp_line(A,C)))-x2^2);
con2:=num(sqrdist(p,pedalpoint(p,pp_line(B,C)))-x2^2);

setring({x1,x2},{},lex);
setideal(polys,polys);
gbasis polys;
{con1,con2} mod gbasis polys;

% Bisector intersection theorem. A constructive proof.
 
A:=Point(0,0); B:=Point(1,0); P:=Point(u1,u2);
l1:=pp_line(A,B);
l2:=symline(l1,pp_line(A,P));
l3:=symline(l1,pp_line(B,P));

point_on_bisector(P,A,B,intersection_point(l2,l3));

clear_ndg(); clear(A,B,C,P,l1,l2,l3);

% Miquel's theorem

on gcd;
A:=Point(0,0); B:=Point(1,0); C:=Point(c1,c2);
P:=choose_pl(pp_line(A,B),u1);
Q:=choose_pl(pp_line(B,C),u2);
R:=choose_pl(pp_line(A,C),u3);

X:=other_cc_point(P,p3_circle(A,P,R),p3_circle(B,P,Q))$

point_on_circle(X,p3_circle(C,Q,R));

off gcd;
clear_ndg(); clear(A,B,C,P,Q,R,X);

% ########################
% Theorems of linear type
% ########################

% Pappus' theorem

A:=Point(u1,u2); B:=Point(u3,u4); C:=Point(x1,u5); 
P:=Point(u6,u7); Q:=Point(u8,u9); R:=Point(u0,x2);

polys:={collinear(A,B,C), collinear(P,Q,R)};

con:=collinear(
	intersection_point(pp_line(A,Q),pp_line(P,B)),
	intersection_point(pp_line(A,R),pp_line(P,C)),
	intersection_point(pp_line(B,R),pp_line(Q,C)))$

vars:={x1,x2};
sol:=solve(polys,vars);

sub(sol,con);

% Pappus' theorem. A constructive approach

A:=Point(u1,u2); B:=Point(u3,u4);  
P:=Point(u6,u7); Q:=Point(u8,u9); 

C:=choose_pl(pp_line(A,B),u5);
R:=choose_pl(pp_line(P,Q),u0);

con:=collinear(intersection_point(pp_line(A,Q),pp_line(P,B)),
	intersection_point(pp_line(A,R),pp_line(P,C)),
	intersection_point(pp_line(B,R),pp_line(Q,C)));

clear_ndg(); clear(A,B,C,P,Q,R);

% ###########################
% Theorems of non linear type
% ###########################

% Fermat Point

A:=Point(0,0); B:=Point(0,2); C:=Point(u1,u2);
P:=Point(x1,x2); Q:=Point(x3,x4); R:=Point(x5,x6);

polys1:={sqrdist(P,B)-sqrdist(B,C), sqrdist(P,C)-sqrdist(B,C), 
	sqrdist(Q,A)-sqrdist(A,C), sqrdist(Q,C)-sqrdist(A,C), 
	sqrdist(R,B)-sqrdist(A,B), sqrdist(R,A)-sqrdist(A,B)};

con:=concurrent(pp_line(A,P), pp_line(B,Q), pp_line(C,R));

vars:={x1,x2,x3,x4,x5,x6};
setring(vars,{},lex);
iso:=isolatedprimes polys1;

for each u in iso collect con mod u;

polys2:={sqrdist(P,B)-sqrdist(P,C), 
	sqrdist(Q,A)-sqrdist(Q,C),  
	sqrdist(R,A)-sqrdist(R,B), 
	num(p3_angle(R,A,B)-p3_angle(P,B,C)), 
	num(p3_angle(Q,C,A)-p3_angle(P,B,C))};

sol:=solve(polys2,{x1,x2,x3,x4,x6});
sub(sol,con);

clear_ndg(); clear(A,B,C,P,Q,R);

% ####################
%  Desargue's theorem
% ####################

% A constructive proof.

A:=Point(a1,a2); B:=Point(b1,b2); 
C:=Point(c1,c2); R:=Point(d1,d2);

S:=choose_pl(par(R,pp_line(A,B)),u);
T:=intersection_point(par(R,pp_line(A,C)),par(S,pp_line(B,C)));
 
con:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

% Desargue's theorem as theorem of linear type.

A:=Point(u1,u2); B:=Point(u3,u4); C:=Point(u5,u6);
R:=Point(u7,u8); S:=Point(u9,x1); T:=Point(x2,x3);

polys:={parallel(pp_line(R,S),pp_line(A,B)),
	parallel(pp_line(S,T),pp_line(B,C)),
	parallel(pp_line(R,T),pp_line(A,C))};

con:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

sol:=solve(polys,{x1,x2,x3});
sub(sol,con);

% The general theorem of Desargue.

A:=Point(0,0); B:=Point(0,1); C:=Point(u5,u6);
R:=Point(u7,u8); S:=Point(u9,u1); T:=Point(u2,x1);

con1:=collinear(intersection_point(pp_line(R,S),pp_line(A,B)),
	intersection_point(pp_line(S,T),pp_line(B,C)),
	intersection_point(pp_line(R,T),pp_line(A,C)));

con2:=concurrent(pp_line(A,R),pp_line(B,S),pp_line(C,T));

sol:=solve(con2,x1);
sub(sol,con1);

clear_ndg(); clear(A,B,C,R,S,T);

% #################
%  Brocard points
% #################

A:=Point(0,0); B:=Point(1,0); C:=Point(u1,u2);

c1:=Circle(1,x1,x2,x3);
c2:=Circle(1,x4,x5,x6);
c3:=Circle(1,x7,x8,x9);

polys:={
	cl_tangent(c1,pp_line(A,C)), 
	point_on_circle(A,c1), 
	point_on_circle(B,c1), 
	cl_tangent(c2,pp_line(A,B)), 
	point_on_circle(B,c2), 
	point_on_circle(C,c2), 
	cl_tangent(c3,pp_line(B,C)), 
	point_on_circle(A,c3), 
	point_on_circle(C,c3)};
 
vars:={x1,x2,x3,x4,x5,x6,x7,x8,x9};
sol:=solve(polys,vars);

P:=other_cc_point(B,sub(sol,c1),sub(sol,c2));
con:=point_on_circle(P,sub(sol,c3));

clear_ndg(); clear A,B,C,c1,c2,c3;	

% ##################
%  Simson's theorem
% ##################

% A constructive proof

        M:=Point(0,0);
        A:=choose_pc(M,r,u1);
        B:=choose_pc(M,r,u2);
        C:=choose_pc(M,r,u3);
        P:=choose_pc(M,r,u4);
        X:=pedalpoint(P,pp_line(A,B))$
        Y:=pedalpoint(P,pp_line(B,C))$
        Z:=pedalpoint(P,pp_line(A,C))$
 
        collinear(X,Y,Z);

clear_ndg(); clear(M,A,B,C,P,X,Y,Z);

% Simson's theorem almost constructive

clear_ndg();

	A:=Point(0,0); B:=Point(u1,u2); 
	C:=Point(u3,u4); P:=Point(u5,x1);
        X:=pedalpoint(P,pp_line(A,B));
        Y:=pedalpoint(P,pp_line(B,C));
        Z:=pedalpoint(P,pp_line(A,C));

	poly:=p4_circle(A,B,C,P); 

        con:=collinear(X,Y,Z);

	remainder(num con,poly);

print_ndg();

% Equational proof, first version:

M:=Point(0,0); A:=Point(0,1); 
B:=Point(u1,x1); C:=Point(u2,x2); P:=Point(u3,x3);

X:=varpoint(A,B,x4); Y:=varpoint(B,C,x5); Z:=varpoint(A,C,x6);

polys:={sqrdist(M,B)-1, sqrdist(M,C)-1, sqrdist(M,P)-1,
	orthogonal(pp_line(A,B),pp_line(P,X)),
	orthogonal(pp_line(A,C),pp_line(P,Z)),
	orthogonal(pp_line(B,C),pp_line(P,Y))};

con:=collinear(X,Y,Z);

vars:={x4,x5,x6,x1,x2,x3};
setring(vars,{},lex);
setideal(polys,polys);
con mod gbasis polys;

% Second version:

A:=Point(0,0);
B:=Point(1,0);
C:=Point(u1,u2);
P:=Point(u3,x1);
X:=Point(x2,0);		% => on the line AB 
Y:=varpoint(B,C,x3);
Z:=varpoint(A,C,x4);

polys:={orthogonal(pp_line(A,C),pp_line(P,Z)),
	orthogonal(pp_line(B,C),pp_line(P,Y)),
	orthogonal(pp_line(A,B),pp_line(P,X)),
       	p4_circle(A,B,C,P)};

con:=collinear(X,Y,Z);

vars:={x2,x3,x4,x1};
setring(vars,{},lex);
con mod interreduce polys;

% The inverse theorem

polys:={orthogonal(pp_line(A,C),pp_line(P,Z)),
	orthogonal(pp_line(B,C),pp_line(P,Y)),
	orthogonal(pp_line(A,B),pp_line(P,X)),
       	collinear(X,Y,Z)};

con:=p4_circle(A,B,C,P);

con mod interreduce polys;

clear_ndg(); clear(M,A,B,C,P,Y,Z);

% ########################
%  The butterfly theorem
% ########################
 
% An equational proof with groebner factorizer and constraints. 

P:=Point(0,0);
O:=Point(u1,0);
A:=Point(u2,u3);	
B:=Point(u4,x1);
C:=Point(x2,x3); 
D:=Point(x4,x5); 
F:=Point(0,x6);
G:=Point(0,x7);

polys:={sqrdist(O,B)-sqrdist(O,A), 
	sqrdist(O,C)-sqrdist(O,A), 
	sqrdist(O,D)-sqrdist(O,A),
	point_on_line(P,pp_line(A,C)),
	point_on_line(P,pp_line(B,D)),
	point_on_line(F,pp_line(A,D)),
	point_on_line(G,pp_line(B,C))
};

con:=num sqrdist(P,midpoint(F,G));

vars:={x6,x7,x3,x5,x1,x2,x4};
setring(vars,{},lex);

sol:=groebfactor(polys,{sqrdist(A,C),sqrdist(B,D)});

for each u in sol collect con mod u;

% A constructive proof

on gcd;

O:=Point(0,0);
A:=Point(1,0);	
B:=choose_pc(O,1,u1);
C:=choose_pc(O,1,u2);
D:=choose_pc(O,1,u3);
P:=intersection_point(pp_line(A,C),pp_line(B,D));

h:=lot(P,pp_line(O,P));

F:=intersection_point(h,pp_line(A,D)); 
G:=intersection_point(h,pp_line(B,C));

con:=sqrdist(P,midpoint(F,G));

off gcd;
clear_ndg(); clear(O,A,B,C,D,P,h,F,G);

% ################################
% Tangency of Feuerbach's circle
% ################################
 
A:=Point(0,0); B:=Point(2,0); C:=Point(u1,u2);
M:=intersection_point(mp(A,B),mp(B,C));
H:=intersection_point(altitude(A,B,C),altitude(B,C,A));
N:=midpoint(M,H);	
c1:=c1_circle(N,sqrdist(N,midpoint(A,B)));
			% Feuerbach's circle

P:=Point(x1,x2);	% => x2 is the radius of the inscribed circle. 

polys:={point_on_bisector(P,A,B,C), point_on_bisector(P,B,C,A)};

con:=cc_tangent(c1_circle(P,x2^2),c1); 

vars:={x1,x2};
setring(vars,{},lex);
setideal(polys,polys);
num con mod gbasis polys;

% Now let P be the incenter of the triangle ABH

polys1:={point_on_bisector(P,A,B,H), point_on_bisector(P,B,H,A)};

con1:=cc_tangent(c1_circle(P,x2^2),c1); 
setideal(polys1,polys1);
num con1 mod gbasis polys1;

clear_ndg(); clear A,B,C,P,M,N,H,c1;

% #############################
% Solutions to the exercises
% #############################

% 1)

A:=Point(0,0); B:=Point(1,0); C:=Point(1,1); D:=Point(0,1);
P:=Point(x1,x2); Q:=Point(x3,1);

polys:={point_on_line(P,par(C,pp_line(B,D))),
	sqrdist(B,D)-sqrdist(B,P),
	point_on_line(Q,pp_line(B,P))};

con:=sqrdist(D,P)-sqrdist(D,Q);

setring({x1,x2,x3},{},lex);
setideal(polys,polys);
con mod gbasis polys;

clear_ndg(); clear(A,B,C,D,P,Q);

% 2)

A:=Point(u1,0); B:=Point(u2,0); C:=Point(0,u3); 
Q:=Point(0,0);		% the pedal point on AB
R:=pedalpoint(B,pp_line(A,C)); 
P:=pedalpoint(A,pp_line(B,C)); 

con1:=point_on_bisector(C,P,Q,R);
con2:=angle_sum(p3_angle(P,Q,C),p3_angle(R,Q,C));

clear_ndg(); clear(A,B,C,P,Q,R);

% 3)

A:=Point(u1,0); B:=Point(u2,0); C:=Point(0,u3); 
P:=pedalpoint(A,pp_line(B,C)); 
Q:=pedalpoint(B,pp_line(A,C)); 
R:=pedalpoint(C,pp_line(A,B));

P1:=pedalpoint(P,pp_line(A,B));
P2:=pedalpoint(P,pp_line(A,C));
Q1:=pedalpoint(Q,pp_line(A,B));
Q2:=pedalpoint(Q,pp_line(B,C));
R1:=pedalpoint(R,pp_line(A,C));
R2:=pedalpoint(R,pp_line(B,C));

con:=for each X in {Q2,R1,R2} collect p4_circle(P1,P2,Q1,X);

clear_ndg(); clear(O,A,B,C,P,Q,R,P1,P2,Q1,Q2,R1,R2);

% 4) 

A:=Point(u1,0); B:=Point(u2,0); C:=Point(0,u3); 
		% => Pedalpoint from C is (0,0)
M:=intersection_point(mp(A,B),mp(B,C));

% Prove (2*h_c*R = a*b)^2

con:=4*u3^2*sqrdist(M,A)-sqrdist(C,B)*sqrdist(A,C);

clear_ndg(); clear(A,B,C,M);

% 5. A solution of constructive type.

on gcd;
O:=Point(0,u1); A:=Point(0,0);	% hence k has radius u1.
B:=Point(u2,0);
M:=midpoint(A,B);
D:=choose_pc(O,u1,u3); 
k:=c1_circle(O,u1^2);
C:=other_cl_point(D,k,pp_line(M,D));
Eh:=other_cl_point(D,k,pp_line(B,D));
F:=other_cl_point(C,k,pp_line(B,C));

con:=parallel(pp_line(A,B),pp_line(Eh,F));

off gcd;
clear_ndg(); clear(O,A,B,C,D,Eh,F,M,k);

% 6)

Z:=Point(0,0); X:=Point(0,1); Y:=Point(0,-1); 
B:=Point(u1,0); C:=Point(u2,0); P:=Point(0,u3);
M:=Point(x1,x2); N:=Point(x3,x4); 
A:=Point(x5,0); D:=Point(x6,0);

polys:={p4_circle(X,Y,B,N), p4_circle(X,Y,C,M),
	p4_circle(X,Y,B,D), p4_circle(X,Y,C,A),
	collinear(B,P,N), collinear(C,P,M)};

con:=concurrent(pp_line(A,M),pp_line(D,N),pp_line(X,Y));

vars:={x1,x2,x3,x4,x5,x6};
setring(vars,{},lex);
res:=groebfactor(polys,{x5-u2,x1-u2,x6-u1,x3-u1});
	% constraints A\neq C, M\neq C, D\neq B, N\neq B
for each u in res collect con mod u;

clear_ndg(); clear(Z,X,Y,B,C,P,M,N,A,D);

% 7)

M:=Point(0,0);
A:=Point(0,u1); B:=Point(-1,0); C:=Point(1,0); 
Eh:=varpoint(A,B,x1); F:=varpoint(A,C,x2);
O:=intersection_point(pp_line(A,M),lot(B,pp_line(A,B))); 
Q:=intersection_point(pp_line(Eh,F),pp_line(B,C));

con1:=num orthogonal(pp_line(O,Q),pp_line(Eh,Q));
con2:=num sqrdist(Q,midpoint(Eh,F));

vars:={x1,x2};
setring(vars,{},lex);
p1:=groebfactor({con1},{x1-1,x2-1,x1,x2});
p2:=groebfactor({con2},{x1-1,x2-1,x1,x2});
	% constraint A,C\neq Eh, B,C\neq F

for each u in p1 collect con2 mod u;
for each u in p2 collect con1 mod u;

% Note that the second component of p2 has no relevant *real* roots,
% since it factors as u1^2 * (x1 - x2)^2 + (x1 + x2 -2)^2 :

u1^2 * (x1 - x2)^2 + (x1 + x2 -2)^2 mod second p2;

clear_ndg(); clear(M,A,B,C,O,Eh,F,Q);

% 8)

on gcd; 

A:=Point(u1,0); B:=Point(u2,0); l1:=pp_line(A,B);
M:=Point(0,u3);		% the incenter, hence u3 = incircle radius 

C:=intersection_point(symline(l1,pp_line(A,M)),
		symline(l1,pp_line(B,M)));  

N:=intersection_point(mp(A,B),mp(B,C)); % the outcenter

sqr_rad:=sqrdist(A,N);	% the outcircle sqradius.

(sqr_rad-sqrdist(M,N))^2-4*u3^2*sqr_rad;

off gcd;
clear_ndg(); clear A,B,C,M,N,l1,sqr_rad;

% 9)

on gcd;

A:=Point(0,0); B:=Point(1,0); M:=Point(u1,0);
C:=Point(u1,u1); F:=Point(u1,1-u1);

c1:=red_hom_coords p3_circle(A,M,C); 
c2:=red_hom_coords p3_circle(B,M,F);
N:=other_cc_point(M,c1,c2);

point_on_line(N,pp_line(A,F));
point_on_line(N,pp_line(B,C));

l1:=red_hom_coords pp_line(M,N);
l2:=sub(u1=u2,l1);

intersection_point(l1,l2); % = (1/2,-1/2)

off gcd;
clear_ndg(); clear A,B,C,F,M,N,c1,c2,l1,l2;

% ####################
% Some more examples
% ####################

% Origin: D. Wang at
%	http://cosmos.imag.fr/ATINF/Dongming.Wang/geother.html
% --------------------------
% Given triangle ABC, H orthocenter, O circumcenter, A1 circumcenter
% of BHC, B1 circumcenter of AHC.
%
% Claim: OH, AA1, BB1 are concurrent.
% --------------------------

A:=Point(u1,0); B:=Point(u2,0); C:=Point(0,u3); 
H:=intersection_point(altitude(C,A,B),altitude(A,B,C));
O:=circle_center(p3_circle(A,B,C)); 
A1:=circle_center(p3_circle(H,B,C)); 
B1:=circle_center(p3_circle(H,A,C)); 

con:=concurrent(pp_line(O,H),pp_line(A,A1),pp_line(B,B1));

end;
REDUCE Historical
[ REDUCE Sourceforge Project | Historical SVN Repository | GitHub Mirror | SourceHut Mirror | NotABug Mirror | Chisel Mirror | Chisel RSS ]