1 | /*----------------------------------------------------------------
|
---|
2 | Basic function for construction of equations
|
---|
3 | in Geometric Theorem proving
|
---|
4 | ----------------------------------------------------------------*/
|
---|
5 | put('geometry,1,'version);
|
---|
6 |
|
---|
7 | define_variable(geqns,[],any);
|
---|
8 | define_variable(hypotheses,[],any);
|
---|
9 | define_variable(conclusions,[],any);
|
---|
10 | define_variable(gvars,[],any);
|
---|
11 | define_variable(gparams,[],any);
|
---|
12 | define_variable(gindex,1,any);
|
---|
13 | define_variable(gparindex,1,any);
|
---|
14 | define_variable(gideal,FALSE,any);
|
---|
15 |
|
---|
16 | geometry_initialize():=(geqns:hypotheses:conclusions:gvars:gparams:[],
|
---|
17 | gindex:gparindex:1);
|
---|
18 | end_of_hypotheses():=(hypotheses:geqns,geqns:[]);
|
---|
19 |
|
---|
20 | end_of_conclusions():=(conclusions:geqns,geqns:[]);
|
---|
21 |
|
---|
22 | generate_ideal():= (gideal:append(hypotheses,
|
---|
23 | makelist(1-genpar()*conclusions[i],i,1,length(conclusions))));
|
---|
24 |
|
---|
25 | show_ideal():=expand(gideal);
|
---|
26 |
|
---|
27 | /* Generate a point with coords [xi,yi] */
|
---|
28 | genpoint():=block([i:gindex],gindex:gindex+1,[concat('x,i),concat('y,i)]);
|
---|
29 | genangle():=block([i:gindex],gindex:gindex+1,[concat('x,i),concat('y,i)]);
|
---|
30 |
|
---|
31 | /* Generate a parameter ui */
|
---|
32 | genpar():=block([i:gparindex,sym:concat('u,i)],
|
---|
33 | gvars:endcons(sym,gvars),gparindex:gparindex+1,sym);
|
---|
34 |
|
---|
35 | /*------------------------------- Lisp Output --------------------------------*/
|
---|
36 |
|
---|
37 | gstringout(file):=block([val:ev(string(showideal()),grind=true)],
|
---|
38 | stringout(file,concat("(string-grobner-system \"",
|
---|
39 | val,"\" '",
|
---|
40 | lispl(gvars),
|
---|
41 | " '",lispl(gparams),")")));
|
---|
42 |
|
---|
43 | /* Output a list as Lisp */
|
---|
44 | lispl(l):=apply(concat,append(["("],makelist(concat(" ",e," "),e,l),[")"]));
|
---|
45 |
|
---|
46 | consider_points([L]):=map(lambda([P],
|
---|
47 | P::genpoint(),gvars:append(gvars,eval(P))),L);
|
---|
48 |
|
---|
49 | consider_angles([L]):=map(lambda([A],
|
---|
50 | A::genangle(),gangles:append(gangles,eval(A),L);
|
---|
51 |
|
---|
52 | arbitrary_points([L]):=map(lambda([P],gparams:append(gparams,eval(P))),L);
|
---|
53 | arbitrary_angles([L]):=map(lambda([P],gparams:endcons(gparams,eval(P))),L);
|
---|
54 | /*--------------- Geometric Declarations -----------------------------------*/
|
---|
55 | /* X, Y, Z on the plane are colinear */
|
---|
56 | are_collinear(X,Y,Z):=
|
---|
57 | (geqns:endcons(det(matrix(cons(1,X),cons(1,Y),cons(1,Z))),geqns));
|
---|
58 |
|
---|
59 | /* Vector AB and CD are perpendicular */
|
---|
60 | are_perpendicular(A,B,C,D):= (geqns:endcons((B-A).(D-C),geqns));
|
---|
61 |
|
---|
62 | /* AB and CD have equal length */
|
---|
63 | have_equal_length(A,B,C,D):=(geqns:endcons((B-A).(B-A)-(D-C).(D-C),geqns));
|
---|
64 |
|
---|
65 | /* AB and CD are parallel */
|
---|
66 | are_parallel(A,B,C,D):=(geqns:endcons(geqns,det(matrix(B-A,D-C))));
|
---|
67 |
|
---|
68 | /* M is the midpoint of AB; 2 equations */
|
---|
69 | is_midpoint(M,A,B):=(geqns:append(geqns,2*M-(A+B)));
|
---|
70 |
|
---|
71 | /* Points A and B are identical */
|
---|
72 | are_identical(A,B):=(geqns:append(geqns,A-B));
|
---|
73 |
|
---|
74 | /* Angles ABC and DEF are equal */
|
---|
75 | /* equal_angles(A,B,C,D,E,F):=(geqns:endcons(geqns,*/
|
---|
76 |
|
---|
77 |
|
---|