;;; abstract-proofs.lisp
;;; Definition and properties of abstract proofs.
;;; Created: 10-6-99 Last Revision: 05-10-00
;;; =============================================================================

;;; To certify this book:

#|
(in-package "ACL2")

;;; Replace this path for your own path where the structures book (which
;;; comes with the ACL2 distribution) is located.
(defconst *structures-book*
  "/usr/local/acl2/v2-5/acl2-sources/books/data-structures/structures")

(certify-book "abstract-proofs" 1)
|#

(in-package "ACL2")


(defmacro include-structures-book () `(include-book ,*structures-book*))
;;; This defmacro is an ugly trick to have this file independent of the
;;; location of the structures book which comes with the ACL2
;;; distribution:

(include-structures-book)


;;; *******************************************
;;; ABSTRACT PROOFS: DEFINITIONS AND PROPERTIES
;;; *******************************************

;;; ============================================================================
;;; 1. Proof steps
;;; ============================================================================

;;; We see here proofs from a very general point of view. Proofs are
;;; lists of r-steps, and r-steps are structures with four fields:
;;; elt1, elt2, direct and operator (every step "connect" elt1 and elt2
;;; in the direction given by direct, and by application of operator). 

;;; Definition and properties about manipulation of proofs and its form
;;; are given here. 

;;; The following is the definition of an abstract reduction step:

(defstructure r-step
   direct
   operator
   elt1
   elt2
   (:options (:conc-name nil)
	     (:do-not :tag)))   

;;; REMARK: An abstract proof will be defined as a list of r-steps. Note
;;; that, in this book, we do not require that the operator is applicable
;;; to one of the elements returning the other. This will be required
;;; for each particular reduction relation. We are only concerned with the
;;; "shape" of proofs.


;;; ============================================================================
;;; 2. Useful definitions
;;; ============================================================================

;;; The last element of a non-empty list

(defmacro last-elt (l)
  `(car (last ,l)))

;;; First and last elements of a proof (including empty proofs) 

(defun first-of-proof (x p)
   (if (endp p) x (elt1 (car p))))

(defun last-of-proof (x p)
   (if (endp p) x (elt2 (last-elt p))))

;;; Steps-up: A chain of inverse steps

(defun steps-up (p)
   (if (endp p)
       t
     (and
      (not (direct (car p)))
      (steps-up (cdr p)))))

;;; Steps-down: A chain of direct steps
 
(defun steps-down (p)
   (if (endp p)
       t
     (and
      (direct (car p))
      (steps-down (cdr p)))))

;;; Steps-valley: down and up
 
(defun steps-valley (p)
   (cond ((endp p) t)
	 ((direct (car p)) (steps-valley (cdr p)))
	 (t (steps-up (cdr p)))))


;;; Steps-mountain: up and down
 
(defun steps-mountain (p)
   (cond ((endp p) t)
	 ((direct (car p)) (steps-down (cdr p)))
	 (t (steps-mountain (cdr p)))))


;;; A local peak

(defun local-peak-p (p)
   (and (consp p)
	(consp (cdr p))
	(atom (cddr p))
	(not (direct (car p)))
	(direct (cadr p))))


;;; Inverse step

(defun inverse-r-step (st)
   (make-r-step
    :direct (not (direct st))
    :elt1 (elt2 st)
    :elt2 (elt1 st)
    :operator (operator st)))
      
;;; The piece of proof just before the first local-peak

(defun proof-before-peak (p)
  (cond ((or (atom p) (atom (cdr p))) p)
	((and (not (direct (car p))) (direct (cadr p))) nil)
	(t (cons (car p) (proof-before-peak (cdr p))))))

;;; The piece of proof just after the first local peak  

(defun proof-after-peak (p)
  (cond ((atom p) p)
	((atom (cdr p)) (cdr p))
	((and (not (direct (car p))) (direct (cadr p)))
	 (cddr p))
	(t (proof-after-peak (cdr p)))))

;;; The first peak of a proof

(defun local-peak (p)
  (cond ((atom p) p)
	((atom (cdr p)) (cdr p))
	((and (not (direct (car p))) (direct (cadr p)))
	 (list (car p) (cadr p)))
	(t (local-peak (cdr p))))))

;;; The top element of a peak

(defun peak-element (p)
   (elt1 (cadr (local-peak p))))

;;; The down part of a valley

(defun proof-before-valley (p)
  (cond ((atom p) p)
	((direct (car p)) (cons (car p)
				(proof-before-valley (cdr p))))
	(t nil))))

;;; Inverse proof

(defun inverse-proof (p)
   (if (atom p)
       p
     (append (inverse-proof (cdr p))
	     (list (inverse-r-step (car p))))))

;;; The up part of a valley

(defun proof-after-valley (p)
  (cond ((atom p) p)
	((direct (car p)) (proof-after-valley (cdr p)))
	(t p))))

;;; The list of elements involved in a proof

(defun proof-measure (p)
  (if (endp p)
      nil
    (cons (elt1 (car p)) (proof-measure (cdr p)))))


;;; ============================================================================
;;; 3. Useful properties
;;; ============================================================================

(defthm steps-down-append
  (equal (steps-down (append p1 p2))
	 (and (steps-down p1) (steps-down p2))))

(defthm steps-up-append
  (equal (steps-up (append p1 p2))
	 (and (steps-up p1) (steps-up p2))))


(defthm steps-valley-append
  (implies (and (steps-down p1)
		(steps-up p2))
	   (steps-valley (append p1 p2))))


(defthm steps-mountain-append
  (implies (and (steps-up p1)
		(steps-down p2))
	   (steps-mountain (append p1 p2))))


(defthm steps-up-inverse-proof
  (equal
   (steps-up (inverse-proof p))
   (steps-down p)))


(defthm steps-down-inverse-proof
  (equal
   (steps-down (inverse-proof p))
   (steps-up p)))


(defthm proof-measure-append
  (equal (proof-measure (append p1 p2))
	 (append (proof-measure p1)
		 (proof-measure p2))))


(defthm steps-down-proof-before-valley
  (steps-down (proof-before-valley p)))


(defthm steps-up-proof-before-valley
  (implies (steps-valley p)
	   (steps-up (proof-after-valley p))))


(defthm proof-valley-append
  (equal
   (append (proof-before-valley p)
	   (proof-after-valley p))
   p)
  :rule-classes nil))

(defthm first-element-of-proof-before-valley
  (implies (consp (proof-before-valley p))
	   (equal (elt1 (car (proof-before-valley p)))
		  (elt1 (car p)))))

(defthm last-element-of-proof-after-valley
   (implies (consp (proof-after-valley p))
 	   (equal (elt2 (last-elt (proof-after-valley p)))
 		  (elt2 (last-elt p)))))


(defthm steps-valley-append-steps-up
  (implies (and (steps-up p2)
		(steps-valley p1))
	   (steps-valley (append p1 p2))))

(defthm steps-dowm-append-steps-valley
  (implies (and (steps-down p1)
		(steps-valley p2))
	   (steps-valley (append p1 p2))))
  
(defthm steps-up-steps-valley
  (implies (steps-up p)
	   (steps-valley p)))

(defthm steps-down-steps-valley
  (implies (steps-down p)
	   (steps-valley p)))

(defthm steps-valley-inverse-proof
  (implies (steps-valley p)
	   (steps-valley (inverse-proof p))))