source: CGBLisp/latex-doc/prover.tex@ 1

\begin{lisp:documentation}{*prover$-$order*}{VARIABLE}{\#'grevlex$>$ }
Admissible monomial order used internally in the proofs of theorems.
\end{lisp:documentation}

\begin{lisp:documentation}{csym}{FUNCTION}{symbol number }
Return symbol whose name is a concatenation of (SYMBOL$-$NAME SYMBOL)
and a number NUMBER.
\end{lisp:documentation}

\begin{lisp:documentation}{real$-$identical$-$points}{MACRO}{a b }
Return [ (A1$-$B1)**2 + (A2$-$B2)**2 ] in lisp (prefix) notation.
The second value is the list of variables (A1 B1 A2 B2). Note that
if the distance between two complex points A, B is zero, it does not
mean that the points are identical. Use IDENTICAL$-$POINTS to express
the fact that A and B are really identical. Use this macro in
conclusions of theorems, as it may not be possible to prove that A
and B are trully identical in the complex domain.
\end{lisp:documentation}

\begin{lisp:documentation}{identical$-$points}{MACRO}{a b }
Return [ A1$-$B1, A2$-$B2 ] in lisp (prefix) notation.
The second value is the list of variables (A1 B1 A2 B2). Note that
sometimes one is able to prove only that (A1$-$B1)**2 + (A2$-$B2)**2
= 0. This equation in the complex domain has solutions with A and B
distinct. Use REAL$-$IDENTICAL$-$POINTS to express the fact that the
distance between two points is 0. Use this macro in assumptions of
theorems, although this is seldom necessary because we assume most of
the time that in assumptions all points are distinct if they are
denoted by different symbols. 
\end{lisp:documentation}

\begin{lisp:documentation}{perpendicular}{MACRO}{a b c d }
Return [ (A1$-$B1) * (C1$-$D1) + (A2$-$B2) * (C2$-$D2) ] in lisp
(prefix) notation. The second value is the list of variables (A1 A2
B1 B2 C1 C2 D1 D2). 
\end{lisp:documentation}

\begin{lisp:documentation}{parallel}{MACRO}{a b c d }
Return [ (A1$-$B1) * (C2$-$D2) $-$ (A2$-$B2) * (C1$-$D1) ] in lisp
(prefix) notation. The second value is the list of variables (A1 A2
B1 B2 C1 C2 D1 D2). 
\end{lisp:documentation}

\begin{lisp:documentation}{collinear}{MACRO}{a b c }
Return the determinant det([[A1,A2,1],[B1,B2,1],[C1,C2,1]]) in lisp
(prefix) notation. The second value is the list of variables (A1 A2
B1 B2 C1 C2). 
\end{lisp:documentation}

\begin{lisp:documentation}{equidistant}{MACRO}{a b c d }
Return the polynomial
[(A1$-$B1)**2+(A2$-$B2)**2$-$(C1$-$D1)**2$-$(C2$-$D2)**2] in lisp
(prefix) notation. The second value is the list of variables (A1 A2
B1 B2 C1 C2 D1 D2). 
\end{lisp:documentation}

\begin{lisp:documentation}{euclidean$-$distance}{MACRO}{a b r }
Return the polynomial [(A1$-$B1)**2+(A2$-$B2)**2$-$R\symbol{94}2] in
lisp (prefix) notation. The second value is the list of variables (A1
A2 B1 B2 R). 
\end{lisp:documentation}

\begin{lisp:documentation}{midpoint}{MACRO}{a b c }
Express the fact that C is a midpoint of the segment AB.
Returns the list [ 2*C1$-$A1$-$B1, 2*C2$-$A2$-$B2 ]. The second value
returned is the list of variables (A1 A2 B1 B2 C1 C2).
\end{lisp:documentation}

\begin{lisp:documentation}{translate$-$statements}{MACRO}{{\sf \&rest} statements }
{\ } % NO DOCUMENTATION FOR TRANSLATE-STATEMENTS
\end{lisp:documentation}

\begin{lisp:documentation}{translate$-$assumptions}{MACRO}{{\sf \&rest} assumptions }
{\ } % NO DOCUMENTATION FOR TRANSLATE-ASSUMPTIONS
\end{lisp:documentation}

\begin{lisp:documentation}{translate$-$conclusions}{MACRO}{{\sf \&rest} conclusions }
{\ } % NO DOCUMENTATION FOR TRANSLATE-CONCLUSIONS
\end{lisp:documentation}

\begin{lisp:documentation}{translate$-$theorem}{MACRO}{({\sf \&rest} assumptions) ({\sf \&rest} conclusions) }
Translates a planar geometry theorem into a system of polynomial
equations. Each assumption or conclusion takes form of a declaration
(RELATION$-$NAME A B C ...) where A B C are points, entered as
symbols and RELATION$-$NAME is a name of a geometric relation, for
example, (COLLINEAR A B C) means that points A, B, C are all
collinear. The translated equations use the convention that (A1,A2)
are the coordinates of the point A. This macro returns multiple
values. The first value is a list of polynomial expressions and the
second value is an automatically generated list of variables from
points A, B, C, etc. For convenience, several macros have been
defined in order to make specifying common geometric relations easy. 
\end{lisp:documentation}

\begin{lisp:documentation}{prove$-$theorem}{MACRO}{({\sf \&rest} assumptions) ({\sf \&rest} conclusions) {\sf \&key} (order *prover$-$order*) }
Proves a geometric theorem, specified in the same manner as in
the macro TRANSLATE$-$THEOREM. The proof is achieved by a call to
IDEAL$-$POLYSATURATION. The theorem is true if the returned value
is a trivial ideal containing 1.
\end{lisp:documentation}