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 | ginit():=(geqns:hypotheses:conclusions:gvars:gparams:[],
|
---|
17 | gindex:gparindex:1);
|
---|
18 | ghypot():=(hypotheses:geqns,geqns:[]);
|
---|
19 |
|
---|
20 | gconcl():=(conclusions:geqns,geqns:[]);
|
---|
21 |
|
---|
22 | gideal():= (gideal:append(hypotheses,
|
---|
23 | makelist(1-genpar()*conclusions[i],i,1,length(conclusions))));
|
---|
24 |
|
---|
25 | showideal():=expand(gideal);
|
---|
26 |
|
---|
27 | gstringout(file):=block([val:ev(string(showideal()),grind=true)],
|
---|
28 | stringout(file,concat("(string-grobner-system \"",
|
---|
29 | val,"\" '",
|
---|
30 | lispl(gvars),
|
---|
31 | " '",lispl(gparams),")")));
|
---|
32 |
|
---|
33 | lispl(l):=apply(concat,append(["("],makelist(concat(" ",e," "),e,l),[")"]));
|
---|
34 |
|
---|
35 | gpoints([L]):=map(lambda([P],
|
---|
36 | P::genpoint(),gvars:append(gvars,eval(P))),L);
|
---|
37 |
|
---|
38 | garbitrary([L]):=map(lambda([P],gparams:append(gparams,eval(P))),L);
|
---|
39 |
|
---|
40 | /* X, Y, Z on the plane are colinear */
|
---|
41 | collinear(X,Y,Z):=
|
---|
42 | (geqns:endcons(det(matrix(cons(1,X),cons(1,Y),cons(1,Z))),geqns));
|
---|
43 |
|
---|
44 | /* Vector AB and CD are perpendicular */
|
---|
45 | perp(A,B,C,D):= (geqns:endcons((B-A).(D-C),geqns));
|
---|
46 |
|
---|
47 | /* AB and CD have equal length */
|
---|
48 | eqlen(A,B,C,D):=(geqns:endcons((B-A).(B-A)-(D-C).(D-C),geqns));
|
---|
49 |
|
---|
50 | /* AB and CD are parallel */
|
---|
51 | parallel(A,B,C,D):=(geqns:endcons(geqns,det(matrix(B-A,D-C))));
|
---|
52 |
|
---|
53 | /* M is the midpoint of AB; 2 equations */
|
---|
54 | midpoint(M,A,B):=(geqns:append(geqns,2*M-(A+B)));
|
---|
55 |
|
---|
56 | /* Points A and B are identical */
|
---|
57 | identical(A,B):=(geqns:append(geqns,A-B));
|
---|
58 |
|
---|
59 | /* Generate a point with coords [xi,yi] */
|
---|
60 | genpoint():=block([i:gindex],gindex:gindex+1,[concat('x,i),concat('y,i)]);
|
---|
61 |
|
---|
62 | /* Generate a parameter ui */
|
---|
63 | genpar():=block([i:gparindex,sym:concat('u,i)],
|
---|
64 | gvars:endcons(sym,gvars),gparindex:gparindex+1,sym);
|
---|
65 |
|
---|
66 |
|
---|