rw.lisp

;;; rewriting.lisp
;;; Directed equations as reductions: rewrite rules and normal forms.
;;; Created: 13-11-99 Last revision: 10-04-2001
;;; ====================================================================

#| To certify this book:

(in-package "ACL2")

(certify-book "rewriting")

|#

(in-package "ACL2")
(include-book "../terminos/subsumption")
(include-book "equational-theories")


;;; *******************************************************************
;;; REDUCIBILITY, REWRITE RULES, NORMAL FORMS, REDUCTION ORDERINGS
;;; *******************************************************************

;;; In this book:

;;; - Definition and verification of a reducibility test for the
;;;   equational reduction defined in equational-theories.lisp.
;;; - Definition of term rewriting systems.
;;; - Verification of a function to perform one step of reduction
;;;   w.r.t. term rewriting systems.
;;; - Definition and properties of reduction orderings.
;;; - Definition of  a function to compute normal form with respect to
;;;   terminating term rewriting systems. 

;;; ============================================================================
;;; 1. A reducibility test: definition and verification.
;;; ============================================================================


;;; Recall from the book convergent.lisp that we need to define an applicability
;;; test (or reducibility test) in order to export the main result of
;;; that book from the abstract case to the equational case. By
;;; definition, a reducibility test is a function receiving an element
;;; (a term in this case) and returning a legal operator (equational
;;; operator) whenever it exists. 

;;; In this section we define a reducibility test for the equational
;;; reduction defined in equational-theories.lisp.


;;; ----------------------------------------------------------------------------
;;; 1.1 Definition of a reducibility test
;;; ----------------------------------------------------------------------------


;;; REDUCIBLE-TOP
;;; ·············

;;; To be reducible at top position by a rule of E (we return a
;;; multivalue with the first rule that reduces term + the matching
;;; substitution + t if such a rule exists, or (mv nil nil nil)
;;; otherwise.
  
(defun eq-reducible-top (term E)
  (declare (xargs :guard (and (term-p term) (system-p E))))
  (if (endp E)
      (mv nil nil nil)
    (let ((equ (car E)))
      (mv-let (matching subsumption)
	      (subs-mv (lhs equ) term)
	      (if subsumption
		  (mv equ matching t)
		(eq-reducible-top term (cdr E)))))))

;;; Closure property

(local
 (defthm eq-reducible-top-substitution-s-p
   (implies (and (term-s-p term)
		 (system-s-p E)
		 (third (eq-reducible-top term E)))
	    (substitution-s-p (second (eq-reducible-top term E))))))

;;; The following results are needed for guard verification

(local
 (defthm eq-reducible-top-term-p
   (implies (and (term-p-aux flg term) flg
		 (system-p E)
		 (third (eq-reducible-top term E)))
	    (and
	     (term-p  (lhs (first (eq-reducible-top term E))))
	     (term-p  (rhs (first (eq-reducible-top term E))))))))


(local
 (encapsulate
  ()

  (local
   (defthm eq-reducible-top-substitution-p-lemma
     (implies (and (term-p term)  
		   (system-p E)
		   (third (eq-reducible-top term E)))
	      (substitution-p (second (eq-reducible-top term E))))
     :rule-classes nil))
  
  (defthm eq-reducible-top-substitution-p
    (implies (and (term-p-aux flg term) flg  
		  (system-p E)
		  (third (eq-reducible-top term E)))
	     (substitution-p (second (eq-reducible-top term E))))
    :otf-flg t
    :hints (("Goal" :use eq-reducible-top-substitution-p-lemma)))))


;;; EQ-REDUCIBLE (and EQ-REDUCIBLE-AUX)
;;; ···································

;;; Recall from equational-theories.lisp that an equational operator
;;; consists of a rule, a position and a matching substitution.  This
;;; function has to return a legal eq-operator for a given term if such
;;; exists, nil otherwise.  We use an auxiliary function
;;; eq-reducible-aux with three extra parameters (flg, posr and arg) in
;;; addition to term and E.
  
;;; Intuitively, we search a legal equational operator for a given term
;;; t1 in a depth-first way. The function eq-reducible-aux implements
;;; this recursive search. Initially, the function is called
;;; (eq-reducible-aux t t1 nil 0 E). During the proccess,
;;; (eq-reducible-aux flg term posr arg E) intuitively means the
;;; following : (reverse posr) is the position where term is included in
;;; the original term t1. So term is the subterm of the original term to
;;; be explored and posr is the reverse of the position of that subterm
;;; in the original term t1. If flg=nil, term is considered as a list of
;;; terms (the arguments of the subterm being explored) and arg is the
;;; number of argument. More precisely, the interpretation of
;;; eq-reducidible-aux is as follows:

;;; - If flg=t, term is a term and the function returns nil or the
;;;   eq-operator with three components:

;;;   * position: (append (reverse posr) q) 
;;;   * rule: l -> r 
;;;   * matching: sigma where q is the first
;;;     position (searching in a depth-first way) such that term/q =
;;;     sigma(l), for some rule l -> r in E.

;;; - If flg=nil, term is a list of terms and returns nil or the
;;;   eq-operator with three components:

;;;   * position: (append (reverse posr) (cons n q))
;;;   * rule: l -> r
;;;   * matching: sigma where n >= arg and t1 = (nth (- n arg 1) term)
;;;     is the first element of term such that a subterm of it is
;;;     reducible by the rule, and such that q is the first position of t1
;;;     (searching in a depth-first way) such that t1/q is equal to
;;;     sigma(l), for some rule l -> r in E.

;;; Note that we are interested in the case posr=nil, flg=t, arg=0.

(defun eq-reducible-aux (flg term posr arg E)
  (if flg
      (mv-let (equ match top-reducible)
	      (eq-reducible-top term E)
	      (if top-reducible
		  (make-eq-operator :pos (revlist posr)
				    :rule equ
				    :match match) 
		(if (variable-p term)
		    nil
		  (eq-reducible-aux nil (cdr term)  posr 0 E))))
    (if (endp term)
	nil
      (let ((first-arg-red
	     (eq-reducible-aux t (car term) (cons (1+ arg) posr) 0 E)))
	(if first-arg-red
	    first-arg-red
	  (eq-reducible-aux nil (cdr term) posr (1+ arg) E))))))

;;; Closure property

(local
 (defthm eq-reducible-aux-substitution-s-p
   (implies (and (term-s-p-aux flg term)
		 (system-s-p E)
		 (eq-reducible-aux flg term posr arg E))
	    (substitution-s-p
	     (op-match (eq-reducible-aux flg term posr arg E))))))

	  
(defun eq-reducible (term E)
  (eq-reducible-aux t term nil 0 E))
  


;;; ----------------------------------------------------------------------------
;;; 1.2 Verification of the reducibility test
;;; ----------------------------------------------------------------------------

;;; Remember form convergent.lisp that the function that tests
;;; reducibility in a given abstact relation has to verify this two
;;; properties: 

;;; 1) eq-reducible, when not nil, returns a legal eq-operator for the
;;;    term in a given signature.

;;;    I.e. the following theorem:

;;;    (defthm eq-reducible-implies-legal
;;;         (implies (and (term-s-p term)
;;;		          (eq-reducible term E)
;;; 		          (system-s-p E))
;;;  	         (eq-legal term (eq-reducible term E) E)))

;;; 2) When eq-reducible returns nil, there are not eq-legal operators
;;;    for the term in a given signature.

;;; I.e., the following theorem:
 
;;;    (defthm not-eq-reducible-nothing-legal
;;;         (implies (not (eq-reducible term E))
;;;        	     (not (eq-legal term op E))))

;;; Our goal in the following is to prove the two above theorems

;;; ····················
;;; 1.2.1 Preliminaries
;;; ····················

;;; A boolean version of eq-reducible-aux 
;;; ·····································

;;; It will be useful to define a function that takes the same boolean
;;; values than eq-reducible-aux. 

(local
 (defun eq-reducible-p-aux (flg term E)
   (if flg
       (cond ((mv-let (equ match top-reducible)
		      (eq-reducible-top term E)
		      (declare (ignore equ match))
		      top-reducible) t)
	     ((variable-p term) nil)
	     (t (eq-reducible-p-aux nil (cdr term) E)))
     (cond ((endp term) nil)
	   ((eq-reducible-p-aux t (car term) E) t)
	   (t (eq-reducible-p-aux nil (cdr term) E))))))
 
;;; The following is the main property of eq-reducible-p-aux. Note that
;;; when only truth values of eq-reducible-p are important, the posr and
;;; arg arguments of eq-reducible-aux are irrelevant, and this rule
;;; allows us to forget about them.

(local
 (defthm eq-reducible-p-iff-eq-reducible
   (iff (eq-reducible-aux flg term posr arg E)
	(eq-reducible-p-aux flg term E))))
 
(local
 (in-theory (disable eq-reducible-p-iff-eq-reducible)))


;;; The main property of eq-reducible-top 
;;; ·····································

;;; When eq-reducible-top-succeeds, it returns a rule and matching
;;; substitution for that rule and the term: 

(local
 (defthm eq-reducible-top-subs-lhs
   (let ((eq-reducible-top 
	  (eq-reducible-top term E)))
     (implies (third eq-reducible-top)
	      (equal (instance (lhs (first eq-reducible-top))
			       (second eq-reducible-top))
		     term)))))

;;; The position of term computed by eq-reducible-aux
;;; ·················································

;;; By definition, (eq-reducible-aux flg term posr arg E) when non nil,
;;; computes a position appending (reverse posr) with the position of
;;; the subterm of term where reducibility is detected. This macro
;;; reducible-pos allows us to talk about the position computed without
;;; the prefix (reverse posr):

(local
 (defmacro reducible-pos (flg term posr arg E)
   `(difference-pos (revlist ,posr)
		    (op-pos (eq-reducible-aux ,flg ,term ,posr ,arg ,E)))))



;;; ·····························································
;;; 1.2.1 eq-reducible returns a legal eq-operator (when non-nil)
;;; ·····························································

;;; Our goal is the following lemma, stablishing the main property of
;;; eq-reducible-aux:
; ; (local 
; ;  (defthm eq-reducible-aux-main-lemma
; ;    (let* ((red (eq-reducible-aux flg term posr arg E))
; ; 	  (pos (op-pos red))
; ; 	  (rule (op-rule red))
; ; 	  (matching (op-match red))
; ; 	  (q (difference-pos (revlist posr) pos)))
; ;      (implies (and red (integerp arg) (>= arg 0))
; ; 	      (if flg
; ; 		  (and (position-p-rec flg q term)
; ; 		       (equal (instance (lhs rule) matching)
; ; 			     (occurrence-rec flg term q)))
; ; 		(and (position-p-rec flg (cons (- (car q) arg) (cdr q))
; ; 				    term)
; ; 		     (equal (instance (lhs rule) matching)
; ; 			    (occurrence-rec flg term (cons (- (car q) arg)
; ; 							  (cdr q)))))))))
;;; 
;;; Note how this lemma formalizes the desription of the function
;;; eq-reducible-aux given when we defined it. Note also that we are
;;; using the alternative recursive versions of position-p and
;;; occurrence. The intended result is a obtained instantiating this
;;; lemma for flg=t, posr=nil and arg=0

;;; Some previous lemmas needed
;;; ···························

;;; The following encapsulate proves that the argument posr is always a
;;; preffix of the returned position:

(local
 (encapsulate
  ()

;;; We need a specific induction scheme:

  (local
   (defun eq-reducible-append-induction (flg term l m arg  E)
     (if flg
	 (if (mv-let (equ match top-reducible)
		     (eq-reducible-top term E)
		     (declare (ignore equ match))
		     top-reducible)
	     arg ;; we make this formal relevant
	   (if (variable-p term)
	       t
	     (eq-reducible-append-induction nil (cdr term) l m 0 E)))
       (if (endp term)
	   t
	 (let ((first-arg-red
		(eq-reducible-aux t (car term)
				  (cons (1+ arg) (append l m)) 0 E)))
	   (if first-arg-red
	       (eq-reducible-append-induction t (car term)
					      (cons (1+ arg) l) m 0 E)
	     (eq-reducible-append-induction nil (cdr term) l m (1+ arg) E)))))))

;;; From the truth point of view the third argument (the position) is
;;; irrelevant:
   
  (local
   (defthm eq-reducible-aux-pos1-iff-pos2
     (implies (eq-reducible-aux flg term pos1 arg E)
	      (eq-reducible-aux flg term pos2 arg E))
     :hints (("Goal"
	      :in-theory (enable eq-reducible-p-iff-eq-reducible)))))
  
  
  (local
   (defthm eq-reducible-aux-pos1-iff-pos2-bis
     (implies (not (eq-reducible-aux flg term pos1 arg E))
	      (not (eq-reducible-aux flg term pos2 arg E)))))
  
;;; This is the main lemma. It generalizes the result we are looking
;;; form: every prefix of the reverse of the third argument is a prefix
;;; of the position finally computed:   
   
  (local
   (defthm eq-reducible-preffix-append
     (implies (eq-reducible-aux flg term (append l m) arg E)
	      (equal (op-pos (eq-reducible-aux flg term (append l m) arg E))
		     (append (revlist m)
			     (op-pos (eq-reducible-aux flg term l arg E)))))
     :rule-classes nil
     :hints (("Goal"
	      :induct (eq-reducible-append-induction flg term l m arg E)))))
  
;;; A particular case: 
 
  (defthm eq-reducible-preffix-append-instance
    (implies (eq-reducible-aux flg term (cons x l) arg E)
	     (equal
	      (op-pos (eq-reducible-aux flg term (cons x l) arg E))
	      (append (revlist (cons x l))
		      (op-pos (eq-reducible-aux flg term nil arg E)))))
    :hints (("Goal" :use (:instance eq-reducible-preffix-append
				    (l nil) (m (cons x l)))))))) 

;;; Some arithmetic results

(local
 (defthm arg-cancelation
   (equal (+ (- arg) 1 arg) 1)))

(local 
 (defthm integer-difference
   (implies (and (integerp x) (integerp y))
	    (integerp (+ (- x) y)))))
(local 
 (defthm distributivity-of-minus
   (equal (- (+ a b)) (+ (- a) (- b)))))
 

;;; The argument arg always increases when running on a list of terms:
  

(local
 (defthm arg-increases
   (implies (eq-reducible-aux nil term posr arg E)
	    (> (car (reducible-pos nil term posr arg E))
	       arg))
   :rule-classes :linear))

;;; A particular case:

(local
 (defthm arg-increases-instance
   (implies (and (integerp arg) (eq-reducible-aux nil term posr
						  (1+ arg) E))
	    (<= 2 (+ (- arg) (car (reducible-pos nil term posr
						 (+ 1 arg) E)))))))

;;; The argument arg is always integer if it is initially an integer.

(local
 (defthm arg-integer
   (implies (and (integerp arg) (eq-reducible-aux nil term posr arg E))
	    (integerp (car (reducible-pos nil term posr arg E))))))

;;; Before beginning the rest of the proofs, we enable the alternatives
;;; recursive versions of position-p, occurrence and replace-term.

(in-theory
 (union-theories (current-theory :here) *position-rec-versions*))


;;; This is the main lemma:
;;; ·······················

(local 
 (defthm eq-reducible-aux-main-lemma
   (let* ((red (eq-reducible-aux flg term posr arg E))
	  (pos (op-pos red))
	  (rule (op-rule red))
	  (matching (op-match red))
	  (q (difference-pos (revlist posr) pos)))
     (implies (and red (integerp arg) (>= arg 0))
	      (if flg
		  (and (position-p-rec flg q term)
		       (equal (instance (lhs rule) matching)
			     (occurrence-rec flg term q)))
		(and (position-p-rec flg (cons (- (car q) arg) (cdr q))
				    term)
		     (equal (instance (lhs rule) matching)
			    (occurrence-rec flg term (cons (- (car q) arg)
							  (cdr q))))))))
   :rule-classes nil))


;;; Some additional results needed
;;; ······························

;;; eq-reducible-aux returns nil or an eq-operator.

(local
 (defthm eq-reducible-aux-eq-operator-op
   (let ((reducible (eq-reducible-aux flg term posr arg E)))
     (implies reducible
	      (eq-operator-p reducible)))))
 
;;; eq-reducible-aux, when non nil, returns a rule of E (in the rule
;;; field). 

(local
 (defthm eq-reducible-top-member-E
   (implies (third (eq-reducible-top term E))
	    (member (first (eq-reducible-top term E))
		    E))))

(local
 (defthm eq-reducible-aux-rule-member-E
   (let ((reducible (eq-reducible-aux flg term posr arg E)))
     (implies reducible
	      (member (op-rule reducible) E)))))


;;; AT LAST, THE INTENDED RELATION, FIRST PART
;;; ··········································


(defthm eq-reducible-implies-eq-legal
  (implies (and (system-s-p E)
                (term-s-p term)
		(eq-reducible term E))
	   (eq-legal term (eq-reducible term E) E))
  :hints (("Goal" :use
	   (:instance
	    eq-reducible-aux-main-lemma (flg t) (posr nil) (arg 0)))))


;;; REMARK: Note that, exactly as we intended, we state the theorem in
;;; terms of position-p and occurrence, and NOT in terms of their
;;; recursive counterparts, position-p-rec and occurrence-rec, used till
;;; now for the above proofs.


;;; ····························································
;;; 1.2.2 If not eq-reducible, there are not eq-legal operators.
;;; ····························································


;;; Previous lemmas
;;; ···············

;;; The property for eq-reducible-top

(local
 (defthm not-eq-reducible-top-member
   (implies (and (not (third (eq-reducible-top term e)))
		 (member rule e))
	    (not (subs (car rule) term)))))

;;; The main lemma: 

(local
 (defthm not-eq-reducible-aux-not-subs-positions-lemma
   (implies (and (not (eq-reducible-p-aux flg term E))
		 (position-p-rec flg pos2 term)
		 (member rule E))
	   (not (subs (lhs rule) 
		      (occurrence-rec flg term pos2))))
   :rule-classes nil))

;;; The same lemma as above stablished in terms of instance, using
;;; subs-completeness: 

(local
 (defthm not-eq-reducible-aux-not-subs-positions
   (implies (and (not (eq-reducible-p-aux flg term E))
		 (position-p-rec flg pos2 term)
		 (member rule E))
	    (not (equal (instance (lhs rule) sigma)
			(occurrence-rec flg term pos2))))
   :hints (("Goal" :use
	    ((:instance not-eq-reducible-aux-not-subs-positions-lemma)
	     (:instance subs-completeness
			(t1 (lhs rule))
			(t2 (occurrence-rec flg term pos2))))))))


;;; THE INTENDED RELATION, SECOND PART
;;; ··································

 
(defthm not-eq-reducible-nothing-eq-legal
  (implies (not (eq-reducible term E))
	   (not (eq-legal term op E)))
  :hints (("Goal" :in-theory (enable eq-reducible-p-iff-eq-reducible))))


;;; ============================================================================
;;; 2. Rewrite systems. Definition
;;; ============================================================================

;;; ---------------
;;; REWRITE SYSTEMS
;;; ---------------

;;; Definition: a rewrite system is a true list of equations s.t. the
;;; lhs is not a variable and the variables in the right hand side are in
;;; the left hand side. The function rewrite-rules checks these
;;; conditions. The function rewrite-system-s-p checks additionally that we
;;; have a system of equations in the given signature.

(defun rewrite-rules (R)
  (if (atom R)
      (equal R nil)
    (and 
     (not (variable-p (lhs (car R))))
     (subsetp (variables t (rhs (car R)))
	      (variables t (lhs (car R))))
     (rewrite-rules (cdr R)))))

(defmacro rewrite-system-s-p (R)
  `(and (system-s-p ,R)
	(rewrite-rules ,R))) 


;;; ============================================================================
;;; 3. One step of reduction: definition and verification
;;; ============================================================================

;;; Note that functions eq-reducible and eq-reduce-one-step are given a
;;; "theoretical" implementation of applying one step of reduction:
;;; eq-reducible searches for an appliable equational operator and (if
;;; any) and eq-reduce-one-step applies the operator. But from a more
;;; practical point of view, we don't need to deal with equational
;;; operators.

;;; We will see now an executable function for testing reducibility of
;;; a term w.r.t a rewrite system and, at the same time, applying one
;;; step of reduction in case of reducibility. We will define it and we
;;; will prove that computes the same as a combination
;;; eq-reducible  and eq-reduce-one-step, in case of rewrite system.


;;; Guard verification
(local
 (defthm system-p-alistp
   (implies (substitution-p S) (alistp S))))


;;; ----------------------------------------------------------------------------
;;; 3.1 Definition of one step of reduction
;;; ----------------------------------------------------------------------------


;;; -------------------------
;;; R-REDUCE-AUX and R-REDUCE
;;; -------------------------

;;; This function r-reduce-aux receives as input a term (or list of
;;; terms, depending on flg) and and a term rewriting system R, and
;;; returns a multivalue of two: the second one is nil if the term is
;;; irreducible w.r.t. R and t if it can be reduced. In this case, the
;;; first value is the result of applying one-step of reduction. As with
;;; eq-reducible-aux, the search of an subterm instance of the lhs of a
;;; rule in R is done in a depth-first way.

(defun r-reduce-aux (flg term R)
  (declare (xargs :guard (and (term-p-aux flg term)
			      (system-p R))))
  (if flg
      (if (variable-p term)
	  (mv nil nil)
	(mv-let
	 (equ match top-red)
	 (eq-reducible-top term R)
	 (if top-red
	     (mv (instance (rhs equ) match) t)
	   (mv-let
	    (reduced-args reducible-args)
	    (r-reduce-aux nil (cdr term) R)
	    (if reducible-args
		(mv (cons (car term) reduced-args) t)
	      (mv nil nil))))))
    (if (endp term)
	(mv nil nil)
      (mv-let
       (reduced-first reducible-first)
       (r-reduce-aux t (car term) R)
       (if reducible-first
	   (mv (cons reduced-first (cdr term)) t)
	 (mv-let
	  (reduced-rest reducible-rest)
	  (r-reduce-aux nil (cdr term) R)
	  (if reducible-rest
	      (mv (cons (car term) reduced-rest) t)
	    (mv nil nil))))))))


;;; r-reduce is r-reduce-aux acting on terms:

(defun r-reduce (term R)
  (declare (xargs :guard (and (term-p term) (system-p R))))
  (r-reduce-aux t term R))


;;; ----------------------------------------------------------------------------
;;; 3.2 Closure property
;;; ----------------------------------------------------------------------------
	       
(local
 (defthm r-reduce-aux-term-p-aux
   (implies (and (term-p-aux flg term) (system-p TRS))
	    (term-p-aux flg (first (r-reduce-aux flg term TRS))))
   :hints (("Subgoal *1/2"
	    :in-theory (disable apply-subst-term-p-aux)
	    :use (:instance apply-subst-term-p-aux
			    (flg t)
			    (term (rhs (first (eq-reducible-top term
								TRS))))
			    (sigma (second (eq-reducible-top term TRS))))))))


(defthm r-reduce-term-p
  (implies (and (term-p term) (system-p TRS))
	   (term-p (first (r-reduce term TRS)))))


;;; ----------------------------------------------------------------------------
;;; 3.3 Main properties
;;; ----------------------------------------------------------------------------

;;; We have to prove:

;;; 1) the second value of r-reduce-aux is not nil if and only if
;;; eq-reducible-aux is not nil (the truth values are the same),
;;; whenever R is a rewrite system.

;;; 2) When the second value of r-reduce-aux is not nil, applying with
;;; eq-reduce-one-step the operator obtained, returns the first value
;;; returned by r-reduce-aux.

;;; ·····································································
;;; 3.2.1 r-reduce and eq-reducible returns the same truth values
;;; ·····································································

;;; Note that the only difference between r-reduce-aux and
;;; eq-reducible-aux (w.r.t. its truth values) is that we do not a to
;;; test reducibility of variables, since lhs of rules of rewrite
;;; systems are not variables:
       
(local
 (encapsulate
  ()

  (local
   (defthm If-apply-subst-returns-variable-then-variable
     (implies (and (not (variable-p t1)) (variable-p t2))
	      (not (equal (apply-subst flg sigma t1) t2)))))
  
  
  (defthm subs-variable-minimum
    (implies (and (variable-p t2) (not (variable-p t1)))
	     (not (subs t1 t2)))
    :hints (("Goal" :use subs-soundness
	     :in-theory (disable subs-soundness))))
  
  (defthm eq-reducible-p-aux-iff-r-reduce-aux
    (implies (rewrite-rules R)
	     (iff (eq-reducible-aux flg term pos arg R)
		  (second (r-reduce-aux flg term R)))))))
 
;;; As a particular case (flg=t), the first main property of r-reduce
;;; (non-local theorem):
 
(defthm eq-reducible-p-iff-r-reduce
  (implies (rewrite-rules R)
	   (iff (second (r-reduce term R))
		(eq-reducible term R))))


;;; ·····································································
;;; 3.2.2 r-reduce performs the same reduction step as
;;; eq-reduce-one-step when applied withe the operator given by
;;; eq-reducible 
;;; ·····································································

;;; Two technical lemmas: 

(local
 (defthm variables-not-reducible-by-rewrite-systems
   (implies (and (variable-p term)
		 (rewrite-rules R))
	    (not (third (eq-reducible-top term R))))))

(local
 (defthm consp-eq-reducible-aux-of-lists
   (implies (eq-reducible-aux nil term posr arg R)
	    (consp (difference-pos (revlist posr)
				   (op-pos (eq-reducible-aux nil term
							  posr arg r)))))))

;;; The main lemma, stablishing the relation between eq-reducible-aux and
;;; r-reduce-aux 

(local 
 (defthm eq-reducible-aux-r-reduce-aux-relation
   (let* ((red (eq-reducible-aux flg term posr arg R))
	  (pos (op-pos red))
	  (rule (op-rule red))
	  (matching (op-match red))
	  (sigma-rhs (instance (rhs rule) matching))
	  (q (difference-pos (revlist posr) pos))
	  (reduced (first (r-reduce-aux flg term R))))
     (implies (and red (integerp arg) (>= arg 0) (rewrite-rules R))
	      (if flg
		  (equal
		   (replace-term-rec flg term q sigma-rhs)
		   reduced)
		(equal
		 (replace-term-rec flg term
				   (cons (- (car q) arg) (cdr q))
				   sigma-rhs)
		 reduced))))
   :rule-classes nil))
;;; Too much cases, fix it!!

(local
 (defthm eq-reducible-implies-legal-corollary
   (implies (eq-reducible term E)
	    (position-p-rec t (op-pos (eq-reducible-aux t term  nil 0 E)) term))
   :hints (("Goal" :use (:instance
			 eq-reducible-aux-main-lemma
			 (flg t) (posr nil) (arg 0))))))



;;; As a particular case (flg=t), the second main property of r-reduce
;;; (non-local theorem):

(defthm r-reduce-equal-eq-reduce-one-step-when-non-nil
  (implies (and (rewrite-rules R)
		(second (r-reduce term R)))
	   (equal (first (r-reduce term R))
		  (eq-reduce-one-step
		   term
		   (eq-reducible term R))))
  :hints (("Goal" :use (:instance
			eq-reducible-aux-r-reduce-aux-relation
			(flg t) (posr nil) (arg 0)))))


;;; We now disable  the recursive versions of position-p, replace-term
;;; and occurrence 

(in-theory
 (set-difference-theories (current-theory :here) *position-rec-versions*))

 
;;; ============================================================================
;;; 4. Termination of term rewriting systems. Reduction orderings.
;;; ============================================================================

;;; Reduction orderings are stable, compatible and well-founded
;;; orderings. They give a necessary and sufficient condition for
;;; noetherianity of rewriting systems in a given signature.

;;; Remember from newman.lisp or convergent.lisp that we defined
;;; noetherianity of an abstract reduction relation as inclusion in a
;;; well-founded ordering. Now we give a general definition of a
;;; reduction ordering and we prove that every term rewriting system
;;; contained in a reduction ordering describes a noetherian reduction
;;; relation. Note the benefits: once a suitable reduction ordering is
;;; found, noetherianity of a finite TRS can be proved simply checking
;;; that all its elements (a finite amount of rules) are in the
;;; reduction ordering

;;; ---------------------------------------------------------------------
;;; 4.1 Definition of a general reduction ordering red0<
;;; ---------------------------------------------------------------------

;;; The reduction ordering will be defined in the set of terms in a
;;; given signature:

(defun term-s-p-f (x) (term-s-p x))

(encapsulate 
 ((red0< (t1 t2) booleanp)
  (fn0 (term) e0-ordinalp))

 (local (defun red0< (t1 t2) (declare (ignore t1 t2)) nil))
 (local (defun fn0 (term) (declare (ignore term)) 1))
 
 (defthm red0<-well-founded-relation-on-term-s-p
   (and
    (implies (term-s-p-f t1) (e0-ordinalp (fn0 t1)))
    (implies (and (term-s-p-f t1) (term-s-p-f t2) (red0< t1 t2))
	     (e0-ord-< (fn0 t1) (fn0 t2))))
   :rule-classes (:well-founded-relation
		  :rewrite))

 (defthm red0<-stable
   (implies (and (term-s-p t1) (term-s-p t2)
		 (substitution-s-p sigma)
		 (red0< t1 t2))
	    (red0< (instance t1 sigma)
		  (instance t2 sigma))))

 (defthm red0<-compatible
   (implies (and (term-s-p t1) (term-s-p t2) (term-s-p term)
		 (position-p pos term)
		 (red0< t1 t2))
	    (red0< (replace-term term pos t1)
		  (replace-term term pos t2))))
 
 (defthm red0<-transitive
   (implies (and (term-s-p t1) (term-s-p t2) (term-s-p t3)
                 (red0< t1 t2) (red0< t2 t3))
	    (red0< t1 t3))))


(in-theory (disable red0<-transitive))

;;; TECHNICAL REMARK: Note that we needed to define the function
;;; term-s-p-f exactly as the macro term-s-p. From the logical point of
;;; view it is the same. But the checks done for the syntax of a
;;; well-founded relation rule requires that the domain of definition
;;; has to be defined as a function. 

;;; IMPORTANT REMARK: The way we have defined reduction orderings can be
;;; an obstacle to show that concrete term rewriting systems are
;;; noetherian: we have to find efectively the function fn0. I think
;;; there is no easier way to show noetherianity of a reduction ordering
;;; or a term rewriting system in the ACL2 logic. This is the main
;;; drawback in our formalization of rewriting.


;;; --------------------------------------------------------------------
;;; 4.2 The main property of reduction orderings
;;; --------------------------------------------------------------------

;;; The following function checks if every rule in a TRS is in the order
;;; defined by the genral reduction ordering red0< defined above.

(defun noetherian-red0< (R)
  (if (endp R)
      t
    (and
     (red0< (rhs (car R))
	   (lhs (car R)))
     (noetherian-red0< (cdr R)))))

;;; Our goal is to prove that (noetherian-red0< R) implies noetherianity
;;; of the reduction relation defined by the TRS R. I.e., the following
;;; goal: 
; ; (defthm R-noetherian-if-subsetp-of-a-reduction-ordering
; ;   (implies (and
; ; 	    (noetherian-red0< R)
; ; 	    (system-s-p R)
; ; 	    (term-s-p term)
; ; 	    (eq-legal term op R))
; ; 	   (red0< (eq-reduce-one-step term op) term)))



;;; Previous lemmas

(local
 (encapsulate
  ()
  (defthm e0-ord-<-irreflexive
    (implies (e0-ordinalp x)
	     (not (e0-ord-< x x))))
  
  (defthm red0<-irreflexive
    (implies (term-s-p x) (not (red0< x x)))
    :hints (("Goal"
	     :use (:instance red0<-well-founded-relation-on-term-s-p
			     (t1 x) (t2 x))
	     :in-theory (disable red0<-well-founded-relation-on-term-s-p))))))




;;; REMARK: We enable occurrence-position-relation because we are going
;;; to do a proof similar to the last part of equational-theories.lisp
;;; (eq-equiv-p is the least congruence relation containing the
;;; equational axioms in E)

(local (in-theory (enable occurrence-position-relation)))


 
(local  
 (defthm red0<-contains-noetherian-rule
   (implies (and
	     (noetherian-red0< R)
	     (member (cons t1 t2) R))
	    (red0< t2 t1))))
;;; Not very good as rewriting rule, but it works




(local
 (defthm member-rewrite-system-noetherian-consp
   (implies (and (member rule R)
		 (not (consp rule)))
	    (not (noetherian-red0< R)))))

(local
 (defthm term-s-p-system-s-p
   (implies (and (member (cons l r) S) (system-s-p S) )
	    (and (term-s-p l) (term-s-p r)))
   :hints (("Goal" :induct (system-s-p S)))))

;;; This is the main lemma:

(local
 (defthm R-noetherian-if-subsetp-of-a-reduction-ordering-lemma
   (implies (and
	     (noetherian-red0< R)
	     (system-s-p R)
	     (member (cons t1 t2) R)
	     (term-s-p s) (substitution-s-p sigma)
	     (position-p p s)
	     (equal (replace-term s p (instance t1 sigma))
		    term))
	    (red0< (replace-term s p (instance t2 sigma))
		  term))))

;;; And, as a particular case, the intended result.

(defthm R-noetherian-if-subsetp-of-a-reduction-ordering
  (implies (and
	    (noetherian-red0< R)
	    (system-s-p R)
	    (term-s-p term)
	    (eq-legal term op R))
	   (red0< (eq-reduce-one-step term op) term)))


;;; REMARK: To enable or disable:

(defconst *equational-theories-and-rewriting*
  '(eq-legal eq-reduce-one-step eq-reducible r-reduce))

;;; IMPORTANT REMARK: we disable eq-reduce-one-step, eq-legal,
;;; r-reduce and eq-reducible: we want these rules to work.


(in-theory
	(set-difference-theories
	 (current-theory :here)
	 *equational-theories-and-rewriting*))

;;; ============================================================================
;;; 5. Normal form computation
;;; ============================================================================


;;; With the definition of r-reduce above we cold define the function
;;; r-normal-form to compute the normal form of a term w.r.t. a rewrite
;;; system R, in the following way:
; (defun r-normal-form (term R)
;   (let ((red (r-reduce term)))
;     (if (second red)
; 	(r-normal-form (first (r-reduce red R)))
;       term)))
;;; But this is obviously non-terminanting (for example, if we use a
;;; non-terminating R, we can obtain an infinite chain). 
;;; We have to assure that the system is noetherian and that we are
;;; dealing with terms in a the signature where we know that the
;;; reduction ordering is well-founded. Something like this:
; (defun r-normal-form (term R)
;   (if (and (noetherian-red0< R) (term-s-p term))
;       (let ((red (r-reduce term)))
; 	(if (second red)
; 	    (r-normal-form (first (r-reduce red R)))
; 	  term))
;     nil))
;;; But this is obviously a waste of time in every recursive call. We
;;; adopt two approaches to compute and reason about normal forms in
;;; ACL2. 

;;; 1) We will define r-normal-form with only one argument an being R an
;;; "external" rewrite system, known to be noetherian.

;;; 2) Define computation of n reduction steps. When n is big enough, a
;;; normal form can be computed in this way.

;;; So our goal in this section is:

;;; - Define (partially) a noetherian term rewriting system (justified
;;; by the general reduction ordering defined above and define and
;;; verify a function to compute the normal form of a term w.r.t. that
;;; term rewrite system.

;;; - Define computation of n reduction steps and show its relation with
;;;   normal form computation. 



;;; ---------------------------------------------------------------------
;;; 5.1 Normal form computation w.r.t. noetherian term rewriting systems
;;; ---------------------------------------------------------------------


;;; ·····································································
;;; 5.1.1 A noetherian term rewriting system
;;; ·····································································

(encapsulate
 ((RN () noetherian-rewrite-system))

 (local (defun RN () nil))

 (defthm RN-rewrite-system
   (rewrite-system-s-p (RN)))
 
 (defthm RN-noetherian-red<
   (noetherian-red0< (RN))))

;;; ·····································································
;;; 5.1.2 Normal form w.r.t. a noetherian term rewrite system
;;; ·····································································

 
(defun RN-normal-form (term)
   (declare (xargs :measure (if (term-s-p term) term 0)
		   :well-founded-relation red0<))
   (if (term-s-p term)
       (mv-let (reduced reducible)
	       (r-reduce term (RN))
	       (if reducible
		   (RN-normal-form reduced)
		 term))
     term))



;;; REMARK: Note also that RN-normal-form is a typical case of a
;;; function of TWO "arguments" that cannot be admited: the first one is
;;; a term and the second one is a term rewrite system. Since the
;;; function is not terminating in general, unless the second "argument"
;;; is a terminating term rewrite system, such a function of two
;;; arguments cannot be defined. Nevertheles, we can still reason about
;;; the function for the terminating cases: we partially define a
;;; constant, (RN) in this case, having the properties needed for
;;; termination. We define the function, RN-NORMAL-FORM in this case,
;;; without the problematic argument and using the constant in its
;;; body. Admission of the function without using local properties of
;;; the constant ((RN) in this case) can be guaranteed by disabling the
;;; constant and its executable counterpart. Futhermore, reasoning about
;;; the function is done outside encapsulate and then no local
;;; properties of the constant are assumed and only the properties
;;; needed for termination can be used.

;;; The main disadvantage of this approach is that the function is not
;;; execuable. Nevertheless, we can define concrete instances of this
;;; definition, replacing (RN) for a particular terminating TRS.



;;; REMARK: Note how this functions is admited: r-reduce is expressed in
;;; terms of eq-reduce-one-step and eq-reducible, using the two main
;;; properties about r-reduce proved above. Then the main property about 
;;; reduction orderings, proved above, is applied


;;; ·····································································
;;; 5.1.2 Properties of RN-normal-form
;;; ·····································································

;;; To verify RN-normal form, we must prove two properties:

;;; - (RN-normal-form term) returns an irreducible term.
;;; - (RN-normal-form term) is equivalent, w.r.t. to the equational
;;;   theory of (RN)

;;; Irreducibility
;;; ··············

(defthm RN-normal-form-irreducible
  (implies (term-s-p term)
	   (not (eq-legal (RN-normal-form term) op (RN)))))


;;; Normal form is an equivalent term
;;; ·································

;;; We show an equational proof justifying the equivalence of term and
;;; (RN-normal-form term):

(defun RN-proof-irreducible (term)
  (declare (xargs :measure (if (term-s-p term) term 0)
		  :well-founded-relation red0<))
  (if (term-s-p term)
      (let ((red (eq-reducible term (RN)))) 
	(if (not red)
	    nil
	  (let ((term2 (eq-reduce-one-step term red)))
	    (cons (make-r-step
		   :direct t :elt1 term :elt2 term2 
		   :operator red)
		  (RN-proof-irreducible term2)))))
     nil))


(defthm RN-normal-form-equivalent-term
  (implies (term-s-p term)
	   (eq-equiv-s-p term
			 (RN-normal-form term)
			 (RN-proof-irreducible term)
			 (RN))))

;;; ---------------------------------------------------------------------
;;; 5.2 Application of a finite number of reduction steps to compute
;;;     normal forms
;;; ---------------------------------------------------------------------

;;; An easy alternative (that will suffice in most practical cases to
;;; compute normal forms) is to apply r-reduce at most a given number of
;;; steps. 


;;; The function normal-form-n-steps receives as input a natural number
;;; n, a term and a term rewriting system and returns a multivalue of
;;; two values. If an irreducible elelemt is obtained in less than n
;;; steps, the second value returned is t and the first value is that
;;; irreducible element. Otherwise the second value is nil (and the
;;; first is irrelevant).



;;; ·····································································
;;; 5.1.1 Definition
;;; ·····································································

(defun normal-form-n-steps (n term R)
  (declare (xargs :guard (and (term-p term)
			      (system-p R)
			      (integerp n) (>= n 0))))
  (mv-let (reduced reducible)
	  (r-reduce term R)
	  (cond ((not reducible) (mv term t))
		((zp n) (mv nil nil))
		(t (normal-form-n-steps (- n 1) reduced R)))))


;;; REMARK: 
;;; Advantages of this definition:
;;; - It does not need to check noetherianity of the TRS.
;;; - It does not need to check that the term is in the signature. 
;;; Disadvantages:
;;; - One needs to know in advance the number of steps needed. But in
;;;   most practical case a big number suffices. 



;;; ·····································································
;;; 5.1.2 Relating normal-form-n-steps and RN-normal-form
;;; ·····································································


(defthm normal-form-n-steps-RN-normal-form-relation
  (implies (and (term-s-p term)
		(second (normal-form-n-steps n0 term (RN))))
	   (equal (first (normal-form-n-steps n0 term (RN)))
		  (RN-normal-form term))))