source: CGBLisp/src/prover.lisp@ 1

;;; -*- Mode: Lisp; Syntax: Common-Lisp; Package: Grobner; Base: 10 -*-
#|
        $Id: prover.lisp,v 1.3 2009/01/22 04:06:51 marek Exp $
  *--------------------------------------------------------------------------*
  |  Copyright (C) 1994, Marek Rychlik (e-mail: rychlik@math.arizona.edu)    |
  |    Department of Mathematics, University of Arizona, Tucson, AZ 85721    |
  |                                                                          |
  | Everyone is permitted to copy, distribute and modify the code in this    |
  | directory, as long as this copyright note is preserved verbatim.         |
  *--------------------------------------------------------------------------*
|#
(defpackage "PROVER"
  (:use "COMMON-LISP" "GROBNER" "PARSE" "ORDER" "COEFFICIENT-RING" "PRINTER")
  (:export identical-points perpendicular parallel collinear translate-theorem prove-theorem
           equidistant midpoint translate-statements real-identical-points
           euclidean-distance
           *prover-order*))

(in-package "PROVER")

#+debug(proclaim '(optimize (speed 0) (debug 3)))
#-debug(proclaim '(optimize (speed 3) (safety 0)))

(defvar *prover-order* #'grevlex>
  "Admissible monomial order used internally in the proofs of theorems.")

;; Translate a geometric theorem specification into a statement of the
;; form
;; for all u1, u2, ... , us f1=f2=...=fn=0 => g=0

(defun csym (symbol number)
  "Return symbol whose name is a concatenation of (SYMBOL-NAME SYMBOL)
and a number NUMBER."
  (intern (concatenate 'string (symbol-name symbol) (format nil "~d" number))))

(defmacro real-identical-points (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."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2)))
    `(list
      '((+ (expt (- ,A1 ,B1) 2) (expt (- ,A2 ,B2) 2)))
      '(,A1 ,A2 ,B1 ,B2))))

(defmacro identical-points (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."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2)))
    `(list
      '((- ,A1 ,B1) (- ,A2 ,B2))
      '(,A1 ,A2 ,B1 ,B2))))

(defmacro perpendicular (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)."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2))
        (C1 (csym C 1))
        (C2 (csym C 2))
        (D1 (csym D 1))
        (D2 (csym D 2)))
    `(list
      '((+ (* (- ,A1 ,B1) (- ,C1 ,D1))
           (* (- ,A2 ,B2) (- ,C2 ,D2))))
      '(,A1 ,A2 ,B1 ,B2 ,C1 ,C2 ,D1 ,D2))))

(defmacro parallel (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)."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2))
        (C1 (csym C 1))
        (C2 (csym C 2))
        (D1 (csym D 1))
        (D2 (csym D 2)))
    `(list
      '((- (* (- ,A1 ,B1) (- ,C2 ,D2))
           (* (- ,A2 ,B2) (- ,C1 ,D1))))
      '(,A1 ,A2 ,B1 ,B2 ,C1 ,C2 ,D1 ,D2))))


(defmacro collinear (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)."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2))
        (C1 (csym C 1))
        (C2 (csym C 2)))
    `(list
      '((+ (- (* ,B1 ,C2) (* ,B2 ,C1))
           (- (* ,A2 ,C1) (* ,A1 ,C2))
           (- (* ,A1 ,B2) (* ,A2 ,B1))))
      '(,A1 ,A2 ,B1 ,B2 ,C1 ,C2))))

(defmacro equidistant (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)."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2))
        (C1 (csym C 1))
        (C2 (csym C 2))
        (D1 (csym D 1))
        (D2 (csym D 2)))
    `(list
      '((- (+ (expt (- ,A1 ,B1) 2) (expt (- ,A2 ,B2) 2))
           (+ (expt (- ,C1 ,D1) 2) (expt (- ,C2 ,D2) 2))))
      '(,A1 ,A2 ,B1 ,B2 ,C1 ,C2 ,D1 ,D2))))
  
(defmacro euclidean-distance (A B R)
  "Return the polynomial [(A1-B1)**2+(A2-B2)**2-R^2] in lisp (prefix)
notation. The second value is the list of variables (A1 A2 B1 B2 R)."
    (let ((A1 (csym A 1))
          (A2 (csym A 2))
          (B1 (csym B 1))
          (B2 (csym B 2)))
      `(list
        '((- (+ (expt (- ,A1 ,B1) 2) (expt (- ,A2 ,B2) 2))
             (expt ,R 2)))
        '(,A1 ,A2 ,B1 ,B2 ,R))))

(defmacro midpoint (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)."
  (let ((A1 (csym A 1))
        (A2 (csym A 2))
        (B1 (csym B 1))
        (B2 (csym B 2))
        (C1 (csym C 1))
        (C2 (csym C 2)))
    `(list
      '((- (* 2 ,C1) ,A1 ,B1) (- (* 2 ,C2) ,A2 ,B2))
      '(,A1 ,A2 ,B1 ,B2 ,C1 ,C2))))

(defmacro translate-statements (&rest statements)
  `(list (mapcar #'car (list ,@statements))
         (remove-duplicates (apply #'append (mapcar #'cadr (list ,@statements))))))

(defmacro translate-assumptions (&rest assumptions)
  (let ((x (gensym)))
    `(let ((,x (translate-statements ,@assumptions)))
       (list (apply #'append (car ,x))
             (cadr ,x)))))

(defmacro translate-conclusions (&rest conclusions)
  `(translate-statements ,@conclusions))
  
(defmacro translate-theorem ((&rest assumptions) (&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."
  `(values
    (translate-assumptions ,@assumptions)
    (translate-conclusions ,@conclusions)))

(defmacro prove-theorem ((&rest assumptions) (&rest conclusions)
                         &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."
  (let ((vars (gensym))
        (ideal (gensym))
        (assump (gensym))
        (concl (gensym)))
    `(multiple-value-bind (,assump ,concl)
         (translate-theorem ,assumptions ,conclusions)
       (let* ((,vars (union (second ,assump) (second ,concl)))
              (,ideal (ideal-polysaturation 
                      (cdr (poly-eval `(:[ ,@(car ,assump)) ,vars
                                      ,order *ring-of-integers*))
                      (mapcar #'(lambda (x)
                                  (cdr (poly-eval (cons :[ x) ,vars
                                                  ,order *ring-of-integers*)))
                              (car ,concl))
                      ,order
                      0
                      nil
                      *ring-of-integers*)))
         (poly-print (cons '[ ,ideal) ,vars)
         (values)))))