[1] | 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 |
|
---|