diff options
Diffstat (limited to 'books/workshops/2007/rubio/support/abstract-reductions')
7 files changed, 2627 insertions, 0 deletions
diff --git a/books/workshops/2007/rubio/support/abstract-reductions/abstract-proofs.lisp b/books/workshops/2007/rubio/support/abstract-reductions/abstract-proofs.lisp new file mode 100644 index 0000000..fa3ee7a --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/abstract-proofs.lisp @@ -0,0 +1,302 @@ +;;; abstract-proofs.lisp +;;; Definition and properties of abstract proofs. +;;; Created: 10-6-99 Last Revision: 05-03-04 (v2-8) +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +;; Not for 2-8 or later +;; ;;; Replace this path for your own path where the structures book (which +;; ;;; comes with the ACL2 distribution) is located. + +;; (defconst *structures-book* + +;; ; "/usr/local/lib/acl2-2.6/books/data-structures/structures") + +;; "/usr/local/acl2/v2-6/acl2-sources/books/data-structures/structures") + +(certify-book "abstract-proofs") + +|# + +(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) + + +(include-book "data-structures/structures" :dir :system) + +;;; ******************************************* +;;; 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). +;;; Intuitively, an abstract proof is a sequence of elements, such that +;;; each element is obtained from one of its neighbors apply somo kind +;;; of abstract oparator. + +;;; In confluence.lisp, we will define abstract proofs. In this book, +;;; definitions and properties about manipulation of proofs and its form +;;; are given. + +;;; 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 (see +;;; confluence.lisp) 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))) + + +;;; Inverse proof + +(defun inverse-proof (p) + (if (atom p) + p + (append (inverse-proof (cdr p)) + (list (inverse-r-step (car p)))))) + +;;; 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 (if any) + +(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))) + + +;;; 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 +;;; ============================================================================ + +;;; All this theorems deal with the "shape" of abstract proofs. + +(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)))) + + + diff --git a/books/workshops/2007/rubio/support/abstract-reductions/confluence.acl2 b/books/workshops/2007/rubio/support/abstract-reductions/confluence.acl2 new file mode 100644 index 0000000..be7264f --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/confluence.acl2 @@ -0,0 +1,18 @@ +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "CNF" *cnf-package-exports*) + +(certify-book "confluence" ? t) diff --git a/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp b/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp new file mode 100644 index 0000000..1b1612e --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/confluence.lisp @@ -0,0 +1,511 @@ +;;; confluence.lisp +;;; Church-Rosser and normalizing abstract reductions. +;;; Created: 06-10-2000 Last Revision: 06-03-2001 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "CNF" *cnf-package-exports*) + +(certify-book "confluence" 3) + +|# + +(in-package "CNF") + +(include-book "abstract-proofs") + +;;; ******************************************************************** +;;; A FORMALIZATION OF NORMALIZING AND CHURCH-ROSSER ABSTRACT REDUCTIONS +;;; ******************************************************************** + +;;; See chapter 2 of the book "Term Rewriting and all that", Baader & +;;; Nipkow, 1998. + + +;;; ============================================================================ +;;; 1. Definition of a normalizing and (CR) abstract reduction +;;; ============================================================================ + + + +(encapsulate + ((q (x) boolean) + (legal (x u) boolean) + (reduce-one-step (x u) element) + (transform-to-valley (x) valley-proof) + (proof-irreducible (x) proof)) + +;;; We define an abstract reduction relation using three functions: +;;; - q is the predicate defining the set where the reduction relation +;;; is defined. +;;; - reduce-one-step is the function applying one step of reduction, +;;; given an element an an operator. Note that elements are reduced by +;;; means of the action of "abstract" operators. +;;; - legal is the function testing if an operator can be applied to a +;;; term. + + (local (defun q (x) (declare (ignore x)) t)) + (local (defun legal (x u) (declare (ignore x u)) nil)) + (local (defun reduce-one-step (x u) (+ x u))) + +;;; With these functions one can define what is a legal proof step: a +;;; r-step-p structure (see abstract-proofs.lisp) such that one the +;;; elements is obtained applying a reduction step to the other (using a +;;; legal operator). + + (defun proof-step-p (s) + (let ((elt1 (elt1 s)) (elt2 (elt2 s)) + (operator (operator s)) (direct (direct s))) + (and (r-step-p s) + (implies direct (and (legal elt1 operator) + (equal (reduce-one-step elt1 operator) + elt2))) + (implies (not direct) (and (legal elt2 operator) + (equal (reduce-one-step elt2 operator) + elt1)))))) + +;;; And now we can define the equivalence closure of the reduction +;;; relation, given by equiv-p: two elements are equivalent if there +;;; exists a list of concatenated legal proof-steps (a PROOF) connecting +;;; the elements, such that every element involved in the proof is in +;;; the set defined by q: + + (defun equiv-p (x y p) + (if (endp p) + (and (equal x y) (q x)) + (and + (q x) + (proof-step-p (car p)) + (equal x (elt1 (car p))) + (equiv-p (elt2 (car p)) y (cdr p))))) + + +;;; To state the Church-Rosser property of the reduction relation, we +;;; reformulate the propery in terms of proofs: "for every proof there +;;; is an equivalent valley proof". The function transform-to-valley is +;;; assumed to return this equivalente valley proof. + + (local (defun transform-to-valley (x) (declare (ignore x)) nil)) + + (defthm Chuch-Rosser-property + (let ((valley (transform-to-valley p))) + (implies (equiv-p x y p) + (and (steps-valley valley) + (equiv-p x y valley))))) + +;;; The normalizing property of the reduction relation is defined also +;;; in terms of proofs: for every element in the set defined by q there +;;; is a proof connecting it to an irreducible element (where +;;; irreducible means here that there is no legal operator which can be +;;; applied) + + (local (defun proof-irreducible (x) (declare (ignore x)) nil)) + + (defthm normalizing + (implies (q x) + (let* ((p-x-y (proof-irreducible x)) + (y (last-of-proof x p-x-y))) + (and (equiv-p x y p-x-y) + (not (legal y op))))))) + + + +;;; We think all these properties are a reasonable abstraction of every +;;; normalizing and Church-Rosser reduction relation. + +;;; ---------------------------------------------------------------------------- +;;; 1.1 Useful rules +;;; ---------------------------------------------------------------------------- + +;;; The following are two useful rewrite rules about the normalizing +;;; property. + +(local + (defthm normalizing-not-consp-proof-irreducible + (implies (and (q x) (not (consp (proof-irreducible x)))) + (not (legal x op))) + :hints (("Goal" :use normalizing)))) + +(local + (defthm normalizing-consp-proof-irreducible + (let ((p-x-y (proof-irreducible x))) + (implies (and (q x) (consp p-x-y)) + (and (equiv-p x (elt2 (last-elt p-x-y)) p-x-y) + (not (legal (elt2 (last-elt p-x-y)) op))))) + :hints (("Goal" :use normalizing)))) + + +;;; Since equiv-p is "infected" (see subversive-recursions in the ACL2 +;;; manual), we have to specify the induction scheme by means of a rule. + +;;; Suggested by M. Kaufman + +(local + (defun induct-equiv-p (x p) (declare (ignore x)) + (if (endp p) + t + (induct-equiv-p (elt2 (car p)) (cdr p))))) + +(local + (defthm equiv-p-induct t + :rule-classes + ((:induction :pattern (equiv-p x y p) + :condition t + :scheme (induct-equiv-p x p))))) + +;;; The first and the last element of a non-empty proof + +(local + (defthm first-element-of-equivalence + (implies (and (equiv-p x y p) (consp p)) + (equal (elt1 (car p)) x)))) + +(local + (defthm last-elt-of-equivalence + (implies (and (equiv-p x y p) (consp p)) + (equal (elt2 (last-elt p)) y)))) + +;;; If x and y are related by equiv-p, then they are in the set defined +;;; by q + +(local + (defthm equiv-p-is-in-p-f-c + (implies (equiv-p x y p) + (and (q x) (q y))) + :rule-classes :forward-chaining)) + +;;; --------------------------------------------------------------------------- +;;; 1.2 equiv-p is an equivalence relation (the least containing the reduction) +;;; --------------------------------------------------------------------------- + +;;; To be confident of the definition of equiv-p we show that equiv-p is +;;; the least equivalence relation (in the set defined by q) containing +;;; reduction steps. + +;;; REMARK: To say it properly, we show that for the relation +;;; "exists p such that (equiv-p x y p)". + +;;; REMARK: Note that in order to prove this property we do +;;; not need the properties confluence and normalizing: this is a +;;; general result that can be derived only from the definition of +;;; equiv-p and proof-step-p. + + +;;; An useful rule to deal with concatenation of proofs +(local + (defthm proof-append + (implies (equal z (last-of-proof x p1)) + (equal (equiv-p x y (append p1 p2)) + (and (equiv-p x z p1) + (equiv-p z y p2)))))) + +;;; 1.2.1. equiv-p is an equivalence relation +;;; ········································· + +;;; The properties of equivalence relations (in q) are met by equiv-p: + +(defthm equiv-p-reflexive + (implies (q x) + (equiv-p x x nil))) + +(defthm equiv-p-symmetric + (implies (equiv-p x y p) + (equiv-p y x (inverse-proof p)))) + +(defthm equiv-p-transitive + (implies (and (equiv-p x y p1) + (equiv-p y z p2)) + (equiv-p x z (append p1 p2))) + :rule-classes nil) + +;;; NOTE: We have an "algebra" of proofs: +;;; - append for the concatenation of proofs +;;; - inverse-proof is already defined in abstract-proofs.lisp +;;; - nil is the identity. + + +;;; 1.2.2. equiv-p contains the reduction relation +;;; ·············································· + +(defthm equiv-p-contains-reduction + (implies (and (q x) + (legal x op) + (q (reduce-one-step x op))) + (equiv-p x (reduce-one-step x op) + (list + (make-r-step + :elt1 x + :elt2 (reduce-one-step x op) + :direct t + :operator op))))) + + +;;; 1.2.3. equiv-p is the least equivalence relation with the above +;;; properties +;;; ································································ + +;;; Let us assume that we have a relation eqv of equivalence in the set +;;; defined by q, containing the reduction steps, and let us show that +;;; it contains equiv-p + +(encapsulate + ((eqv (t1 t2) boolean)) + + (local (defun eqv (t1 t2) (declare (ignore t1 t2)) t)) + + (defthm eqv-contains-reduction + (implies (and (q x) + (legal x op) + (q (reduce-one-step x op))) + (eqv x (reduce-one-step x op)))) + + (defthm eqv-reflexive + (implies (q x) (eqv x x))) + + (defthm eqv-symmetric + (implies (and (q x) (eqv x y) (q y)) + (eqv y x))) + + (defthm eqv-transitive + (implies (and (q x) (q y) (q z) (eqv x y) (eqv y z)) + (eqv x z)))) + +;;; Then eqv contains equiv-p + +(defthm equiv-p-the-least-equivalence-containing-reduction + (implies (equiv-p x y p) + (eqv x y)) + :hints (("Subgoal *1/3" + :use + (:instance eqv-transitive + (y (elt2 (car p))) (z y))))) + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 There are no equivalent and distinct normal forms +;;; ---------------------------------------------------------------------------- + +;;; Two lemmas + +(local + (defthm reducible-steps-up + (implies (and (consp p) (steps-up p) + (not (legal y (operator (last-elt p))))) + (not (equiv-p x y p))))) + + +(local + (defthm two-ireducible-connected-by-a-valley-are-equal + (implies (and (steps-valley p) + (equiv-p x y p) + (not (legal x (operator (first p)))) + (not (legal y (operator (last-elt p))))) + (equal x y)) + :rule-classes nil)) + +;;; And the theorem + +(local + (defthm if-CR--two-ireducible-connected-are-equal + (implies (and (equiv-p x y p) + (not (legal x (operator (first (transform-to-valley p))))) + (not (legal y (operator (last-elt (transform-to-valley p)))))) + (equal x y)) + :rule-classes nil + :hints (("Goal" :use (:instance + two-ireducible-connected-by-a-valley-are-equal + (p (transform-to-valley p))))))) + +;;; REMARK: although this lemma is weaker than the statement "every two +;;; equivalent normal forms are equal" (we cannot state this in our +;;; current language, see confluence-v0.lisp), it is a tool to show +;;; equality of every two particular elements known to be equivalent and +;;; irreducible, as we will see. + +;;; ============================================================================ +;;; 2. Decidability of Church-Rosser and normalizing redutions +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 2.1 Normal forms, definition and fundamental properties. +;;; ---------------------------------------------------------------------------- + + +;;; The normal form of an element is the las element in the proof +;;; obtained by the function proof-irreducible. + +(defun normal-form (x) (last-of-proof x (proof-irreducible x))) + + +;;; No operator can be applied to (normal-form x) (it is an irreducible +;;; element) + +(local + (defthm irreducible-normal-form + (implies (q x) + (not (legal (normal-form x) op))))) + +;;; And (normal-form x) is equivalent to x (the proof is given by +;;; proof-irreducible). +(local + (defthm equivalent-proof-n-f + (implies (q x) + (equiv-p x (normal-form x) (proof-irreducible x))))) + + +;;; And two useful rewrite rules, showing how normal-form is related to +;;; proof-irreducible. + +(local + (defthm proof-irreducible-atom-normal-form + (implies (atom (proof-irreducible x)) + (equal (normal-form x) x)))) + +(local + (defthm proof-irreducible-consp-normal-form + (implies (consp (proof-irreducible x)) + (equal (elt2 (last-elt (proof-irreducible x))) (normal-form x))))) + + +;;; We can disable normal-form (its fundamental properties are now +;;; rewrite rules): + +(local (in-theory (disable normal-form))) + + +;;; ---------------------------------------------------------------------------- +;;; 2.2 A decision algorithm for [<-reduce-one-step->]* +;;; ---------------------------------------------------------------------------- + +;;; We define a decision procedure for the equivalence closure of the +;;; reduction relation. The decision procedure (provided normal-form is +;;; computable) is: we simply test if normal-forms are equal. + +(defun r-equiv (x y) + (equal (normal-form x) (normal-form y))) + +;;; ············································································ +;;; 2.2.1 Completeness +;;; ············································································ + +;;; We want to show that if (equiv-p x y p) the the normal forms of x +;;; and y are the same. The idea is the following: if we have a proof +;;; between x and y, we can build a proof between (normal-form x) and +;;; (normal-form y). But then, from the theorem +;;; if-CR--two-ireducible-connected-are-equal and the fact that +;;; normal-forms are irreducible we can conclude that both normal-forms +;;; are equal. + +;;; This is the proof between (normal-form x) and (normal-form y). +(local + (defun make-proof-between-normal-forms (x y p) + (append (inverse-proof (proof-irreducible x)) + p + (proof-irreducible y)))) + +;;;; Some needed lemmas + +(local + (defthm consp-inverse-proof + (iff (consp (inverse-proof p)) + (consp p)))) + +(local + (defthm last-elt-append + (implies (consp p2) + (equal (last-elt (append p1 p2)) (last-elt p2))))) +(local + (defthm last-elt-inverse-proof + (implies (consp p) + (equal (last-elt (inverse-proof p)) + (inverse-r-step (car p)))))) + +(local + (defthm first-element-of-proof-irreducible + (implies (and (q x) (consp (proof-irreducible x))) + (equal (elt1 (car (proof-irreducible x))) x)) + :hints (("Goal" :use ((:instance + first-element-of-equivalence + (y (normal-form x)) (p (proof-irreducible + x)))))))) + +;;; The main lemma for completeness: the proof constructed is a proof +;;; indeed. + +(local + (defthm make-proof-between-normal-forms-indeed + (implies (equiv-p x y p) + (equiv-p (normal-form x) + (normal-form y) + (make-proof-between-normal-forms x y p))))) + +(local (in-theory (disable make-proof-between-normal-forms))) + +;;; And the intended theorem: +;;; COMPLETENESS + +(defthm r-equiv-complete + (implies (equiv-p x y p) + (r-equiv x y)) + :hints (("Goal" :use ((:instance + if-CR--two-ireducible-connected-are-equal + (x (normal-form x)) + (y (normal-form y)) + (p (make-proof-between-normal-forms x y p))))))) + + +;;; ············································································ +;;; 2.2.1 Soundness +;;; ············································································ + +;;; We want to prove that if x and y have common normal forms then there +;;; is a proof between x and y. + +;;; We build such proof between x and y (if their normal forms are +;;; equal), given by the following function: + +(defun make-proof-common-n-f (x y) + (append (proof-irreducible x) (inverse-proof (proof-irreducible y)))) + +;;; And the intended theorem. +;;; SOUNDNESS + +(defthm r-equiv-sound + (implies (and (q x) (q y) (r-equiv x y)) + (equiv-p x y (make-proof-common-n-f x y))) + :hints (("Subgoal 3" + :use ((:instance + equiv-p-symmetric + (x y) + (y (normal-form y)) + (p (proof-irreducible y))) + (:instance equivalent-proof-n-f + (x y)))))) + +;;; REMARK: :use is needed due to a weird behaviour that sometimes +;;; ACL2 has with equalities in hypotesis. + + + + + + + + diff --git a/books/workshops/2007/rubio/support/abstract-reductions/convergent.acl2 b/books/workshops/2007/rubio/support/abstract-reductions/convergent.acl2 new file mode 100644 index 0000000..54304ab --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/convergent.acl2 @@ -0,0 +1,22 @@ +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "CNF" *cnf-package-exports*) + +(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*)) + +(defpkg "CNV" (cons 'multiset-diff *cnf-package-exports*)) + +(certify-book "convergent" ? t) diff --git a/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp b/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp new file mode 100644 index 0000000..6229eed --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/convergent.lisp @@ -0,0 +1,643 @@ +;;; convergent.lisp +;;; Convergent reduction relations have a decidable equivalence closure +;;; Created: 1-11-99 Last modified: 11-10-00 +;;; ============================================================================= + +#| To certify this book: + +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "CNF" *cnf-package-exports*) + +(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*)) + +(defpkg "CNV" (cons 'multiset-diff *cnf-package-exports*)) + +(certify-book "convergent" 5) + +|# + +;;; +(in-package "CNV") + +(local (include-book "confluence")) + +(include-book "newman") + + +;;; **************************************************************************** +;;; LOCALLY CONFLUENT AND TERMINATING REDUCTION RELATIONS HAVE A +;;; DECIDABLE EQUIVALENCE CLOSURE +;;; **************************************************************************** + + +;;; We prove that every noetherian, locally confluent reduction relation +;;; has decidable equivalence closure. A good example of functional +;;; instantiation. This result can be easily proved by functional +;;; instantiation of the results in the books previously +;;; developed. Using confluence.lisp, we need to show that the reduction +;;; relation is normalizing and has the Church-Rosser property. And the +;;; Church-Rosser property can be proved by using Newman's lemma, proved +;;; in newman.lisp. The normalizing property is an easy consequence of +;;; noetherianity. + +;;; REMARK: To undersatand this book, you should read previously the +;;; books abstract-proofs.lisp, confluence.lisp and newman.lisp. + +;;; ============================================================================ +;;; 1. A Tool for functional instantation +;;; ============================================================================ + +;;; In this file we have to extensively use functional +;;; instantiation of results previously proved. The functional +;;; instantiations we have to carry out are always of the same kind: +;;; the functional substitution relates functions with the same symbol +;;; name but in different package and the same happen with individual +;;; variables. We define the following functions in :program +;;; mode to provide a tool to make this kind of functional-instance +;;; hints convenient. + +(local + (defun pkg-functional-instance-pairs (lemma-name symbols) + (declare (xargs :mode :program)) + (if (endp symbols) + nil + (cons (list (acl2::intern-in-package-of-symbol + (string (car symbols)) lemma-name) + (car symbols)) + (pkg-functional-instance-pairs lemma-name (cdr symbols)))))) + +(local + (defun pkg-functional-instance + (id lemma-name variable-symbols function-symbols) + (declare (xargs :mode :program)) + (if (equal id (acl2::parse-clause-id "Goal")) + (list :use (list* :functional-instance + (list* :instance + lemma-name + (pkg-functional-instance-pairs + lemma-name variable-symbols)) + (pkg-functional-instance-pairs + lemma-name function-symbols))) + nil))) + + +;;; The function pkg-functional-instance computes a hint (see +;;; computed-hints in the ACL2 manual) and is called +;;; in the following way: + +;;; (pkg-functional-instance id lemma-name variable-symbols +;;; function-symbols) + +;;; where: + +;;; id: is always the variable acl2::id +;;; lemma-name: the name of the lemma to be instantiated +;;; (including the package). +;;; variable-symbols: the list of symbol names of variables to be +;;; instantiated. +;;; function-symbols: the list of symbol names of functions to be +;;; instantiated. + +;;; The computed hint is the functional instantiation of the lemma-name, +;;; relating each variable name and function name (of the package where +;;; the lemma has been proved) to the same symbol name in the current +;;; package. + + +;;; ============================================================================ +;;; 2. Formalizing the hypothesis of the theorem +;;; ============================================================================ + +;;; REMARK: This section is the same as in newman.lisp: formalization of +;;; noetherianity and local confluence. Nevertheless, since we have to +;;; compute normal forms and the function proof-irreducible, we have to +;;; assume the existence of a reducibility test given by a function +;;; "reducible" with the following properties for every element x in the +;;; set defined by a predicate q: + +;;; 1) When "reducible" returns non-nil, it returns a legal operator for x. +;;; 2) When "reducible" returns nil, there are no legal operators for +;;; x. See newman.lisp and confluence-v0.lisp for more details + +;;; Furthermore, since "reducible" will be used to define a function +;;; proof-irreducible with the same properties as defined in +;;; confluence.lisp, we will also assume a "closure" property: + +;;; 3) For every x such that (q x) and (legal x op) the legal operator +;;; op appplied to x returns an element in q. + +;;; This assumptions on the function reducible are "reasonable" if we +;;; want to talk about computation of normal forms. + + +(encapsulate + ((rel (x y) boolean) + (q (x) boolean) + (q-w () elemement) + (fn (x) o-p) + (legal (x u) boolean) + (reducible (x) boolean) + (reduce-one-step (x u) element) + (transform-local-peak (x) proof)) + + +;;; A general noetherian partial order rel is (partially) defined. The +;;; function is well founded on the set defined by a predicate q, and fn +;;; is the order-preserving mapping from objects to ordinals. It will be +;;; used (see below) to justify noetherianity of the reduction relation, +;;; based on the following meta-theorem: "A reduction is noetherian iff +;;; it is contained in a noetherian partial order" (see newman.lisp for +;;; more information): + + (local (defun rel (x y) (declare (ignore x y)) nil)) + (local (defun q (x) (declare (ignore x)) t)) + (local (defun fn (x) (declare (ignore x)) 1)) + + (defthm rel-well-founded-relation-on-q + (and + (implies (q x) (o-p (fn x))) + (implies (and (q x) (q y) (rel x y)) + (o< (fn x) (fn y)))) + :rule-classes (:well-founded-relation + :rewrite)) + + (defthm rel-transitive + (implies (and (q x) (q y) (q z) (rel x y) (rel y z)) + (rel x z))) + + (in-theory (disable rel-transitive)) + +;;; For resons that will be clear later, we need to assume that the set +;;; defined by the predicate "q" is not empty (by the way, a reasonable +;;; assumption). We assume the existence of an element (q-w): + + (local (defun q-w () 0)) + + (defthm one-element-of-q (q (q-w))) + + +;;; As in confluence.lisp, we define an abstract reduction relation +;;; using three functions: +;;; - q is the predicate defining the set where the reduction relation +;;; is defined (introduced above). +;;; - reduce-one-step is the function applying one step of reduction, +;;; given an element and an operator. Note that elements are reduced by +;;; means of the action of "abstract" operators. +;;; - legal is the function testing if an operator can be applied to a +;;; term. + + + (local (defun legal (x u) (declare (ignore x u)) nil)) + (local (defun reduce-one-step (x u) (+ x u))) + + +;;; As in confluence.lisp, with these three functions one can define +;;; what is a legal proof step: a r-step-p structure (see +;;; abstract-proofs.lisp) such that one the elements is obtained +;;; applying a reduction step to the other (using a legal operator). + + (defun proof-step-p (s) + (let ((elt1 (elt1 s)) (elt2 (elt2 s)) + (operator (operator s)) (direct (direct s))) + (and (r-step-p s) + (implies direct (and (legal elt1 operator) + (equal (reduce-one-step elt1 operator) + elt2))) + (implies (not direct) (and (legal elt2 operator) + (equal (reduce-one-step elt2 operator) + elt1)))))) + +;;; As in confluence.lisp, now we can define the equivalence closure of +;;; the reduction relation, given by equiv-p: two elements are +;;; equivalent if there exists a list of concatenated legal proof-steps +;;; (a PROOF) connecting the elements, such that every element involved +;;; in the proof is in the set defined by q. In the book confluence.lisp +;;; is proved that equiv-p defines the least equivalence relation in the +;;; set defined by q, containing the reduction relation. + + (defun equiv-p (x y p) + (if (endp p) + (and (equal x y) (q x)) + (and + (q x) + (proof-step-p (car p)) + (equal x (elt1 (car p))) + (equiv-p (elt2 (car p)) y (cdr p))))) + +;;; We will assume also that for every x in q, application of legal +;;; operators is a closed operation in q. This property will be needed +;;; when we define the function proof-irreducible (the counterpart of +;;; proof-irreducible in confluence.lisp) + + (defthm legal-reduce-one-step-closure + (implies (and (q x) (legal x op)) + (q (reduce-one-step x op)))) + + +;;; As we said before, we assume the existence of a reducibility test (a +;;; function called "reducible") because we are going to define +;;; normal-form computation: + + (local (defun reducible (x) (declare (ignore x)) nil)) + +;;; These are the two properties required to "reducible" + + + (defthm legal-reducible-1 + (implies (and (q x) (reducible x)) + (legal x (reducible x)))) + + (defthm legal-reducible-2 + (implies (and (q x) (not (reducible x))) + (not (legal x u)))) + +;;; As in newman.lisp local confluence is reformulated in terms of +;;; proofs: "for every local-peak, there is an equivalente valley proof" +;;; This equivalent valley proof is returned by the function +;;; transform-local-peak: + + + (local (defun transform-local-peak (x) (declare (ignore x)) nil)) + + + (defthm local-confluence + (let ((valley (transform-local-peak p))) + (implies (and (equiv-p x y p) (local-peak-p p)) + (and (steps-valley valley) + (equiv-p x y valley))))) + +;;; As in newman.lisp, this is noetherianity of the reduction relation, +;;; justified by inclusion in the well founded relation rel: if we +;;; permorm one (legal) reduction step in the set defined by q, then we +;;; obtain a smaller element (with respect to rel): + + (defthm noetherian + (implies (and (q x) (legal x u)) + (rel (reduce-one-step x u) x)))) + +;;; We think all these properties are a reasonable abstraction of every +;;; concrete convergent reduction relation. + +;;; ============================================================================ +;;; 2. Theorem: The reduction relation has the Church-Rosser property +;;; ============================================================================ + + +;;; REMARK: We show that it is possible to define a function +;;; transform-to-valley with the property of transforming every proof +;;; in an equivalent valley proof. This is done as in newman.lisp, but +;;; now we can functionally instantiate the main results proved there. +;;; See newman.lisp for details. + +;;; Well-founded multiset extension of rel +;;; ······································ + +;(acl2::defmul-components rel) +;The list of components is: +; (REL REL-WELL-FOUNDED-RELATION-ON-Q T FN X Y) +(local + (acl2::defmul (rel rel-well-founded-relation-on-q q fn x y))) + + +;;; Auxiliary functions in the definition of transform-to-valley +;;; ···························································· + +(local + (defun exists-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and + (not (direct (car p))) + (direct (cadr p))) + (and (proof-step-p (car p)) + (proof-step-p (cadr p)) + (q (elt1 (car p))) (q (elt2 (car p))) + (q (elt1 (cadr p))) (q (elt2 (cadr p))) + (equal (elt2 (car p)) (elt1 (cadr p))))) + (t (exists-local-peak (cdr p)))))) + +(local + (defun replace-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and (not (direct (car p))) (direct (cadr p))) + (append (transform-local-peak (list (car p) (cadr p))) + (cddr p))) + (t (cons (car p) (replace-local-peak (cdr p))))))) + +(local + (defun steps-q (p) + (if (endp p) + t + (and (r-step-p (car p)) + (q (elt1 (car p))) + (q (elt2 (car p))) + (and (steps-q (cdr p))))))) + +;;; This property steps-q implies that proof-measure is an object +;;; representing a multiset where the well-founded relation is defined. + +(local + (defthm steps-q-implies-q-true-listp-proof-measure + (implies (steps-q p) + (q-true-listp (proof-measure p))))) + + +;;; transform-to-valley terminates +;;; ······························ + +;;; By functional instantiation of the same result in newman.lisp + +(local + (defthm transform-to-valley-admission + (implies (exists-local-peak p) + (mul-rel (proof-measure (replace-local-peak p)) + (proof-measure p))) + + :hints ((pkg-functional-instance + acl2::id + 'nwm::transform-to-valley-admission + '(p) '(q fn legal forall-exists-rel-bigger reduce-one-step + proof-step-p equiv-p rel mul-rel + exists-local-peak replace-local-peak + transform-local-peak exists-rel-bigger)) + ("Subgoal 7" ; changed by J Moore after v5-0, from "Subgoal 8", for tau + :use + (:instance rel-transitive + (x nwm::x) (y nwm::y) (z nwm::z)))))) + +;;; Additional technical lemmas: + +(local + (defthm mul-rel-nil + (implies (consp l) + (mul-rel nil l)))) + +(local + (defthm exists-local-peak-proof-measure-consp + (implies (exists-local-peak p) + (consp (proof-measure p))))) + + +;;; Definition of transform-to-valley +;;; ································· +(local + (defun transform-to-valley (p) + (declare (xargs :measure (if (steps-q p) (proof-measure p) nil) + :well-founded-relation mul-rel + :hints (("Goal" :in-theory (disable mul-rel))))) + (if (and (steps-q p) (exists-local-peak p)) + (transform-to-valley (replace-local-peak p)) + p))) + + +;;; Properties of transform-to-valley: the Church-Rosser property +;;; ····························································· + +;;; By functional instantiation of the same results in newman.lisp + + +(local + (defthm equiv-p-x-y-transform-to-valley + (implies (equiv-p x y p) + (equiv-p x y (transform-to-valley p))) + :hints ((pkg-functional-instance + acl2::id + 'nwm::equiv-p-x-y-transform-to-valley + '(p x y) + '(q fn transform-to-valley reduce-one-step legal + proof-step-p equiv-p rel exists-local-peak + steps-q replace-local-peak transform-local-peak))))) + +(local + (defthm valley-transform-to-valley + (implies (equiv-p x y p) + (steps-valley (transform-to-valley p))) + :hints ((pkg-functional-instance + acl2::id + 'nwm::valley-transform-to-valley + '(p x y) + '(q fn transform-to-valley reduce-one-step legal + proof-step-p equiv-p rel exists-local-peak + steps-q replace-local-peak transform-local-peak))))) + +;;; These two properties trivially implies the Church-Rosser-property: +; (defthm Chuch-Rosser-property +; (let ((valley (transform-to-valley p))) +; (implies (equiv-p x y p) +; (and (steps-valley valley) +; (equiv-p x y valley))))) + + +;;; ============================================================================ +;;; 3. Theorem: The reduction relation is normalizing +;;; ============================================================================ + +;;; To instantiate the results in confluence.lisp, we have to define a +;;; function proof-irreducible and prove the properties assumed there as +;;; axioms. Remember from confluence.lisp that proof-irreducible returns +;;; for every x in q, a proof showing the equivalence of x with an +;;; element in normal form (i.e. such that no operator is legal +;;; w.r.t. it). + +;;; Definition of proof-irreducible +;;; ······························· + +;;; REMARK: Iteratively apply reduction steps until an irreducible +;;; element is found, and collect all those proof steps. + +(defun proof-irreducible (x) + (declare (xargs :measure (if (q x) x (q-w)) + :well-founded-relation rel)) + (if (q x) + (let ((red (reducible x))) + (if red + (cons (make-r-step + :direct t :elt1 x :elt2 (reduce-one-step x red) + :operator red) + (proof-irreducible (reduce-one-step x red))) + nil)) + nil)) + +;;; REMARKS: + +;;; - This proof-irreducible computation is only guaranteed to terminate +;;; when its input is an element such that (q x), since well-foundedness +;;; is only assumed in q. But ACL2 is a logic of total functions. Thus, +;;; we define as nil (the concrete value is irrelevant) the value of +;;; normal-form outside q. + +;;; - Note that to admit this function, we must provide a measure and a +;;; well-founded relation. The well-founded relation is rel, and the +;;; measure has to assign to every element x, an object in the set where +;;; rel is known to be well-founded (i.e. in the set defined by q). When +;;; x is in q, there is no problem (we assign x). But if x is not in q, +;;; we have to assign an arbitrary element in q. That's the reason why +;;; we defined before a witness element (q-w) in q. + + + +;;; Main property of proof-irreducible (normalizing property) +;;; ························································· + +;;; REMARK: This is the assumed property of proof-irreducible in +;;; confluence.lisp. + +(local + (defthm normalizing + (implies (q x) + (let* ((p-x-y (proof-irreducible x)) + (y (last-of-proof x p-x-y))) + (and (equiv-p x y p-x-y) + (not (legal y op))))))) + + +;;; Exactly as in confluence.lisp, we can express the normalizing +;;; property as two rewrite rules: + +(local + (defthm normalizing-not-consp-proof-irreducible + (implies (and (q x) (not (consp (proof-irreducible x)))) + (not (legal x op))) + :hints (("Goal" :use (:instance normalizing))))) + +(local + (defthm normalizing-consp-proof-irreducible + (let ((p-x-y (proof-irreducible x))) + (implies (and (q x) (consp p-x-y)) + (and (equiv-p x (elt2 (last-elt p-x-y)) p-x-y) + (not (legal (elt2 (last-elt p-x-y)) op))))) + :hints (("Goal" :use (:instance normalizing))))) + + +;;; ============================================================================ +;;; 4. Definition: normal form computation +;;; ============================================================================ + +;;; Normal-form computation + +(defun normal-form (x) + (declare (xargs :measure (if (q x) x (q-w)) + :well-founded-relation rel)) + (if (q x) + (let ((red (reducible x))) + (if red + (normal-form (reduce-one-step x red)) + x)) + x)) + +;;; REMARK: The same REMARKS as in proof-ireducible applies here. Here, +;;; the value returned for elements x outside q is irrelevant in +;;; principle. We return x to make it analogue to the definition of +;;; normal-form in confluence.lisp (since we are going to functionally +;;; instantiate). + +;;; ============================================================================ +;;; 5. Theorem: The equivalence closure is decidable +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 5.1 Definition of a decison procedure for <--*--reduce-one-step--*--> +;;; ---------------------------------------------------------------------------- + + +(defun r-equivalent (x y) + (equal (normal-form x) (normal-form y))) + + +;;; REMARK: Note that this is not exactly the same definition of the +;;; decision procedure given in confluence.lisp. The point is that in +;;; confluence.lisp the normal-form computation is through the proof +;;; given by proof-irreducible. In order to functionally instantiate the +;;; result of confluence.lisp, we show that it is the same function. + + +;;; This is the same function as r-equiv in confluence.lisp +;;; ······················································· + +;;; REMARK: normal-form-aux is analogue NWM::normal-form, but +;;; normal-form is more "eficcient". The same for r-equiv. + +(local + (defun normal-form-aux (x) + (last-of-proof x (proof-irreducible x)))) + + +(local + (defthm normal-form-aux-normal-form + (equal (normal-form x) + (normal-form-aux x)))) + +(local + (defun r-equiv (x y) + (equal (normal-form-aux x) (normal-form-aux y)))) + + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 Soundness and completeness +;;; ---------------------------------------------------------------------------- + +;;; Completeness +;;; ············ + +;;; By functional instantiation of the same results in confluence.lisp + +(defthm r-equivalent-complete + (implies (equiv-p x y p) + (r-equivalent x y)) + + :rule-classes nil + :hints ((pkg-functional-instance + acl2::id + 'cnf::r-equiv-complete + '(p x y) + '(q legal proof-step-p r-equiv + equiv-p reduce-one-step proof-irreducible + transform-to-valley normal-form)))) + + + +;;; Soundness +;;; ········· + +;;; By functional instantiation of the same results in confluence.lisp + +;;; Skolem function +(defun make-proof-common-n-f (x y) + (append (proof-irreducible x) (inverse-proof (proof-irreducible y)))) + + +(defthm r-equivalent-sound + (implies (and (q x) (q y) (r-equivalent x y)) + (equiv-p x y (make-proof-common-n-f x y))) + + :hints ((pkg-functional-instance + acl2::id + 'cnf::r-equiv-sound + '(x y) + '(q legal make-proof-common-n-f proof-step-p + r-equiv equiv-p + reduce-one-step proof-irreducible transform-to-valley + normal-form)))) + + + + + + + + diff --git a/books/workshops/2007/rubio/support/abstract-reductions/newman.acl2 b/books/workshops/2007/rubio/support/abstract-reductions/newman.acl2 new file mode 100644 index 0000000..88a8148 --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/newman.acl2 @@ -0,0 +1,18 @@ +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*)) + +(certify-book "newman" ? t) diff --git a/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp b/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp new file mode 100644 index 0000000..80ca739 --- /dev/null +++ b/books/workshops/2007/rubio/support/abstract-reductions/newman.lisp @@ -0,0 +1,1113 @@ +;;; newman.lisp +;;; A mechanical proof of Newman's lemma for abstract reduction relations +;;; Created: 6-8-99 Last revison: 07-03-2001 +;;; ============================================================================ + +#| To certify this book: + +(in-package "ACL2") + +(defconst *abstract-proofs-exports* + '(last-elt r-step direct operator elt1 elt2 r-step-p make-r-step + first-of-proof last-of-proof steps-up steps-down steps-valley + proof-before-valley proof-after-valley inverse-r-step inverse-proof + local-peak-p proof-measure proof-before-peak proof-after-peak + local-peak peak-element)) + +(defconst *cnf-package-exports* + (union-eq *acl2-exports* + (union-eq + *common-lisp-symbols-from-main-lisp-package* + *abstract-proofs-exports*))) + +(defpkg "NWM" (cons 'multiset-diff *cnf-package-exports*)) + +(certify-book "newman" 3) + +|# + + +(in-package "NWM") + +(include-book "../multisets/defmul") + +(include-book "abstract-proofs") + + +;;; ******************************************************************* +;;; A MECHANICAL PROOF OF NEWMAN'S LEMMA: +;;; For terminating relations, local confluence implies +;;; confluence [see "Term Rewriting and all that..." (Baader & Nipkow), +;;; chapter 2, pp. 28-29] +;;; ******************************************************************* + +;;; ============================================================================ +;;; 1. Formalizing the statement of the theorem +;;; ============================================================================ + + +;;; ---------------------------------------------------------------------------- +;;; 1.1 A noetherian and locally confluent reduction relation +;;; ---------------------------------------------------------------------------- + + +(encapsulate + ((rel (x y) booleanp) + (q (x) booleanp) + (fn (x) o-p) + (legal (x u) boolean) + (reduce-one-step (x u) element) + (transform-local-peak (x) proof)) + + +;;; A general noetherian partial order rel is (partially) defined. The +;;; function is well founded on the set defined by a predicate q, and fn +;;; is the order-preserving mapping from objects to ordinals. It will be +;;; used (see below) to justify noetherianity of the reduction relation, +;;; based on the following meta-theorem: "A reduction is noetherian iff +;;; it is contained in a noetherian partial order" + +;;; REMARK: Transitivity is required, but this is not a real +;;; restriction, since a reduction is noetherian iff its included in a +;;; transitive and noetherian relation. We need it because transitive +;;; closure, in general, is not decidable even if the relation is +;;; decidable, so we cannot define the transitive closure of a relation. + + (local (defun rel (x y) (declare (ignore x y)) nil)) + (local (defun fn (x) (declare (ignore x)) 1)) + (local (defun q (x) (declare (ignore x)) t)) + + (defthm rel-well-founded-relation-on-q + (and + (implies (q x) (o-p (fn x))) + (implies (and (q x) (q y) (rel x y)) + (o< (fn x) (fn y)))) + :rule-classes (:well-founded-relation :rewrite)) + + (defthm rel-transitive + (implies (and (q x) (q y) (q z) (rel x y) (rel y z)) + (rel x z)) + :rule-classes nil) + +;;; As in confluence.lisp, we define an abstract reduction relation +;;; using three functions: +;;; - q is the predicate defining the set where the reduction relation +;;; is defined (introduced above). +;;; - reduce-one-step is the function applying one step of reduction, +;;; given an element and an operator. Note that elements are reduced by +;;; means of the action of "abstract" operators. +;;; - legal is the function testing if an operator can be applied to a +;;; term. + + + (local (defun legal (x u) (declare (ignore x u)) nil)) + (local (defun reduce-one-step (x u) (+ x u))) + +;;; With these functions one can define what is a legal proof step: a +;;; r-step-p structure (see abstract-proofs.lisp) such that one the +;;; elements is obtained applying a reduction step to the other (using a +;;; legal operator). + + (defun proof-step-p (s) + (let ((elt1 (elt1 s)) (elt2 (elt2 s)) + (operator (operator s)) (direct (direct s))) + (and (r-step-p s) + (implies direct (and (legal elt1 operator) + (equal (reduce-one-step elt1 operator) + elt2))) + (implies (not direct) (and (legal elt2 operator) + (equal (reduce-one-step elt2 operator) + elt1)))))) + +;;; And now we can define the equivalence closure of the reduction +;;; relation, given by equiv-p: two elements are equivalent if there +;;; exists a list of concatenated legal proof-steps (a PROOF) connecting +;;; the elements, such that every element involved in the proof is in +;;; the set defined by q. In the book confluece.lisp is proved that +;;; equiv-p defines the least equivalence relation in the set defined by +;;; q, containing the reduction relation. + + + (defun equiv-p (x y p) + (if (endp p) + (and (equal x y) (q x)) + (and + (q x) + (proof-step-p (car p)) + (equal x (elt1 (car p))) + (equiv-p (elt2 (car p)) y (cdr p))))) + +;;; Local confluence is reformulated in terms of proofs: "for every +;;; local-peak, there is an equivalent valley proof" This equivalent +;;; valley proof is returned by a function transform-local-peak: + + (local (defun transform-local-peak (x) (declare (ignore x)) nil)) + + (defthm local-confluence + (let ((valley (transform-local-peak p))) + (implies (and (equiv-p x y p) (local-peak-p p)) + (and (steps-valley valley) + (equiv-p x y valley))))) + +;;; Noetherianity of the reduction relation, justified by inclusion in +;;; the well founded relation rel: if we permorm one (legal) reduction +;;; step in the set defined by q, then we obtain a smaller element +;;; (with respect to rel): + + (defthm noetherian + (implies (and (q x) (legal x u) (q (reduce-one-step x u))) + (rel (reduce-one-step x u) x)))) + + +;;; We think all these properties are a reasonable abstraction of every +;;; noetherian and locally confluent reduction relation. + + +;;; A first theorem: irreflexivity of rel + +;; Añadido para la 2.8 +(defthm o<-irreflexive + (not (o< x x))) + + +(local + (defthm rel-irreflexive + (implies (q x) (not (rel x x))) + :hints (("Goal" + :in-theory (disable rel-well-founded-relation-on-q) + :use (:instance rel-well-founded-relation-on-q + (y x)))))) + +;;; REMARK: e0-ord-irreflexive (in multiset.lisp) is needed + + +;;; ---------------------------------------------------------------------------- +;;; 1.3 Our goal +;;; ---------------------------------------------------------------------------- + +;;; REMARK: We will prove that the reduction relation has the +;;; Church-Rosser property, instead of showing confluence (which is +;;; equivalent). + +;;; Our definition of the Church-Rosser property (see confluence.lisp) is: +;;; (defthm Chuch-Rosser-property +;;; (let ((valley (transform-to-valley p))) +;;; (implies (equiv-p x y p) +;;; (and (steps-valley valley) +;;; (equiv-p x y valley))))) +;;; So our goal is to define transform-to-valley with these properties. + + +;;; ---------------------------------------------------------------------------- +;;; 1.4 Some useful stuff +;;; ---------------------------------------------------------------------------- + + +;;; Since equiv-p is "infected" (see subversive-recursions in the ACL2 +;;; manual), we have to specify the induction scheme. Suggested by +;;; M. Kaufman + +(local + (defun induct-equiv-p (x p) (declare (ignore x)) + (if (endp p) + t + (induct-equiv-p (elt2 (car p)) (cdr p))))) + +(local + (defthm equiv-p-induct t + :rule-classes + ((:induction :pattern (equiv-p x y p) + :condition t + :scheme (induct-equiv-p x p))))) + + +;;; Proof-p: sometimes it will be useful to talk about proofs without +;;; mentioning equiv-p. Proof-p recognizes sequences of legal +;;; concatenated steps without mentioning endpoints. + +(local + (defun proof-p (p) + (if (atom p) + t + (and (proof-step-p (car p)) (q (elt1 (car p))) (q (elt2 (car p))) + (if (atom (cdr p)) + t + (and (equal (elt2 (car p)) (elt1 (cadr p))) + (proof-p (cdr p)))))))) + +;;;; Relation between proof-p y equiv-p + +(local + (defthm equiv-p-proof-p + (implies (equiv-p x y p) + (proof-p p)))) + +;;; A rule without free variables (almost) expressing local conf. + +(local + (defthm local-confluence-w-f-v + (implies (and (proof-p p) (local-peak-p p)) + (and (steps-valley (transform-local-peak p)) + (proof-p (transform-local-peak p)))) + :hints (("Goal" :use (:instance local-confluence + (x (elt1 (car p))) + (y (elt2 (last-elt p)))) + :in-theory (disable local-confluence))))) + +;;; ============================================================================ +;;; 2. Towards the definition of transform-to-valley +;;; ============================================================================ + + +(defun exists-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and + (not (direct (car p))) + (direct (cadr p))) + (and (proof-step-p (car p)) + (proof-step-p (cadr p)) + (q (elt1 (car p))) + (q (elt2 (car p))) (q (elt2 (cadr p))) + (equal (elt2 (car p)) (elt1 (cadr p))))) + (t (exists-local-peak (cdr p))))) + +(defun replace-local-peak (p) + (cond ((or (atom p) (atom (cdr p))) nil) + ((and (not (direct (car p))) (direct (cadr p))) + (append (transform-local-peak (list (car p) (cadr p))) + (cddr p))) + (t (cons (car p) (replace-local-peak (cdr p)))))) + + +;;; The idea is to define a function like this (i.e. to replace local peaks +;;; iteratively until there are no local peaks left): + +;(defun transform-to-valley (p) +; (if (not (exists-local-peak p)) +; p +; (transform-to-valley (replace-local-peak p)))) + +;;; A minor modification has to be done to the condition of the base case +;;; of this definition, as we will see. But the main point here is that, +;;; as expected, this function is not admitted without help from the +;;; user (the length of the proof (replace-local-peak p) may be greater +;;; than the length of p). So the hard part of the theorem is to provide +;;; that help as a suitable set of rules and hints, to get the admission +;;; of transform-to-valley. + + +;;; ============================================================================ +;;; 3. Admission of transform-to-valley +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 3.1 A multiset measure +;;; ---------------------------------------------------------------------------- + + +;;; We will lead the prover to the admission of the theorem by means of +;;; a multiset measure (following a hand proof by Klop). The idea is to +;;; assign to every proof the multiset of elements involved in it. These +;;; multisets are compared w.r.t. the well-founded multiset relation +;;; induced by rel (mul-rel) + +;;; We define the well-founded extension of rel to multisets. +;;; See defmul.lisp + + +; (acl2::defmul-components rel) +;The list of components is: +; (REL REL-WELL-FOUNDED-RELATION-ON-Q Q FN X Y) + +(acl2::defmul (rel rel-well-founded-relation-on-q q fn x y) + :verify-guards t) + +;;; This defmul call defines the well-founded multiset relation mul-rel, +;;; defined on multisets of elements satisfying q (defined by +;;; q-true-listp), induced by the well-founded relation rel. + +;;; ---------------------------------------------------------------------------- +;;; 3.2 Proof steps in the set defined by q. +;;; ---------------------------------------------------------------------------- + +;;; Our measure hint for the admission of transform-to-valley will be +;;; (see the definition of proof-measure in abstract-proofs.lisp) the +;;; proof-measure of the proof, and the well founded relation will be +;;; mul-rel. Note that mul-rel is known to be well-founded ONLY on +;;; multisets of elements satisfying q, so the recursion has only to be +;;; called for proofs such that its proof-measure is a set of elements +;;; satisfying q. + +;;; With these considerations, our goal now is to define +;;; the following function, with the following measure and w.f. relation +;;; hints. + +;(defun transform-to-valley (p) +; (declare (xargs :measure (if (steps-q p) (proof-measure p) nil) +; :well-founded-relation mul-rel)) +; (if (and (steps-q p) (exists-local-peak p)) +; (transform-to-valley (replace-local-peak p)) +; p)) + +;;; where the function steps-q checks if we have a sequence of proof +;;; steps connecting elements satisfying q: + +(defun steps-q (p) + (if (endp p) + t + (and (r-step-p (car p)) + (q (elt1 (car p))) + (q (elt2 (car p))) + (steps-q (cdr p))))) + +;;; This property steps-q implies that proof-measure is an object +;;; representing a multiset where the well-founded relation is defined. + +(local + (defthm steps-q-implies-q-true-listp-proof-measure + (implies (steps-q p) + (q-true-listp (proof-measure p))))) + +;;; ---------------------------------------------------------------------------- +;;; 3.2 The proof of the main lemma for admission of transform-to-valley +;;; ---------------------------------------------------------------------------- + +;;; In order to admit transform-to-valley, our main goal is: + +;;; (defthm transform-to-valley-admission +;;; (implies (exists-local-peak p) +;;; (mul-rel (proof-measure (replace-local-peak p)) +;;; (proof-measure p))) +;;; :rule-classes nil) + +;;; REMARK: Note that we can even restrict p to be steps-q, but it is +;;; not needed, as we will see. + +;;; This conjecture generates the following two goals: + +;;; Subgoal 2 +;;; (IMPLIES (EXISTS-LOCAL-PEAK P) +;;; (CONSP (MULTISET-DIFF (PROOF-MEASURE P) +;;; (PROOF-MEASURE (REPLACE-LOCAL-PEAK P))))). +;;; Subgoal 1 +;;; (IMPLIES (EXISTS-LOCAL-PEAK P) +;;; (FORALL-EXISTS-REL-BIGGER +;;; (MULTISET-DIFF (PROOF-MEASURE (REPLACE-LOCAL-PEAK P)) +;;; (PROOF-MEASURE P)) +;;; (MULTISET-DIFF (PROOF-MEASURE P) +;;; (PROOF-MEASURE (REPLACE-LOCAL-PEAK P))))). + +;;; In the sequel, we build a collection of rules to prove these two goals. + +;;; ············································································ +;;; 3.2.1 Removing initial and final common parts +;;; ············································································ + + +(local + (defthm proof-peak-append + (implies (exists-local-peak p) + (equal + (append (proof-before-peak p) + (append (local-peak p) + (proof-after-peak p))) + p)) + :rule-classes (:elim :rewrite))) + +;;; REMARK: This decomposition only makes sense when (exists-local-peak +;;; p). The elim rule is for avoiding :use. + + +;;; We use a rewrite rule to decompose proof-measure of proofs with +;;; local peaks. This rule implements a rewriting rule strategy: every +;;; proof with a local peak can be divided into three pieces (w.r.t. its +;;; complexity) + +(local + (defthm proof-measure-with-local-peak + (implies (exists-local-peak p) + (equal (proof-measure p) + (append (proof-measure (proof-before-peak p)) + (proof-measure (local-peak p)) + (proof-measure (proof-after-peak p))))))) + + +(local (in-theory (disable proof-peak-append))) + +;;; The following rule helps to express the proof-measure of +;;; (replace-local-peak p) in a similar way than the previous rule does +;;; with the proof-measure of p + +(local + (defthm replace-local-peak-another-definition + (implies (exists-local-peak p) + (equal (replace-local-peak p) + (append (proof-before-peak p) + (append (transform-local-peak (local-peak p)) + (proof-after-peak p))))))) + + +;;; The above rules rewrite the proof-measure's of p and +;;; (replace-local-peak p) in a way such that the initial and final +;;; common parts are explicit. In this way the rules +;;; multiset-diff-append-1 and multiset-diff-append-2 rewrite the +;;; expression, simplifying the common parts (see multiset.lisp and +;;; defmul.lisp to read also the role of the congruence rules generated +;;; by the above defmul call). The simplified goals now are: + +;;; Subgoal 2' +;;; (IMPLIES +;;; (EXISTS-LOCAL-PEAK P) +;;; (CONSP +;;; (MULTISET-DIFF (PROOF-MEASURE (LOCAL-PEAK P)) +;;; (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))))). + +;;; Subgoal 1' +;;; (IMPLIES +;;; (EXISTS-LOCAL-PEAK P) +;;; (FORALL-EXISTS-REL-BIGGER +;;; (MULTISET-DIFF (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))) +;;; (PROOF-MEASURE (LOCAL-PEAK P))) +;;; (MULTISET-DIFF (PROOF-MEASURE (LOCAL-PEAK P)) +;;; (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))))). + + + + +;;; ············································································ +;;; 3.2.2 Removing the first element of the local peak +;;; ············································································ + +;;; First, let's prove that the local peak and the transformed are +;;; proofs with the same endpoints, so their proof measures have the +;;; same first element. This will be useful in 3.2.3 where we will look +;;; for an explicit reference to the peak-element of the local peak. + +(local + (defthm local-peak-equiv-p + (implies (exists-local-peak p) + (equiv-p (elt1 (car (local-peak p))) + (elt2 (cadr (local-peak p))) + (local-peak p))))) + +(local + (defthm transform-local-peak-equiv-p + (implies (exists-local-peak p) + (equiv-p (elt1 (car (local-peak p))) + (elt2 (cadr (local-peak p))) + (transform-local-peak (local-peak p)))))) + + +;;; Using the above, now we will see that we can simplify further the +;;; multiset difference of the measures of the the proofs, +;;; removing the first element. This is not so easy as one can think at +;;; first sight, since there is a subtle point: the transformed proof +;;; can be empty. + + +(local + (defthm consp-proof-measure + (equal (consp (proof-measure p)) + (consp p)))) + +(local + (defthm car-equiv-p-proof-measure + (implies (and (equiv-p x y p) + (consp p)) + (equal (car (proof-measure p)) x)))) + +;;; The main lemma of this sub-subsection. Note how we distinguish two +;;; cases: proofs empty or not. + +(local + (defthm multiset-diff-proof-measure + (implies (and (equiv-p x y p1) + (equiv-p x z p2)) + (equal (multiset-diff + (proof-measure p1) + (proof-measure p2)) + (if (consp p1) + (if (consp p2) + (multiset-diff (cdr (proof-measure p1)) + (cdr (proof-measure p2))) + (proof-measure p1)) + nil))) + :rule-classes nil)) + +(local + (defthm consp-local-peak + (implies (exists-local-peak p) + (consp (local-peak p))) + :rule-classes :type-prescription)) + +;;; And now the two rules needed for the intended simplification + +(local + (defthm multiset-diff-proof-measure-local-peak-transform-1 + (implies (exists-local-peak p) + (equal + (multiset-diff (proof-measure (transform-local-peak (local-peak p))) + (proof-measure (local-peak p))) + (if (consp (transform-local-peak (local-peak p))) + (multiset-diff + (cdr (proof-measure (transform-local-peak (local-peak p)))) + (cdr (proof-measure (local-peak p)))) + nil))) + :hints (("Goal" :use + (:instance multiset-diff-proof-measure + (x (elt1 (car (local-peak p)))) + (y (elt2 (cadr (local-peak p)))) + (z (elt2 (cadr (local-peak p)))) + (p1 (transform-local-peak (local-peak p))) + (p2 (local-peak p))))))) + + +(local + (defthm multiset-diff-proof-measure-local-peak-transform-2 + (implies (exists-local-peak p) + (equal + (multiset-diff + (proof-measure (local-peak p)) + (proof-measure (transform-local-peak (local-peak p)))) + (if (consp (transform-local-peak (local-peak p))) + (multiset-diff + (cdr (proof-measure (local-peak p))) + (cdr (proof-measure (transform-local-peak (local-peak p))))) + (proof-measure (local-peak p))))) + :hints (("Goal" :use + (:instance multiset-diff-proof-measure + (x (elt1 (car (local-peak p)))) + (y (elt2 (cadr (local-peak p)))) + (z (elt2 (cadr (local-peak p)))) + (p2 (transform-local-peak (local-peak p))) + (p1 (local-peak p))))))) + +;;; REMARK: it could seem that in the lemma multiset-diff-proof-measure +;;; variables x, y and z are not needed and that proof-p could be used +;;; instead of equiv-p. But we think that in that case, to deal with the +;;; empty proof would be somewhat unnatural. + + +;;; With the rules we have at this moment, our unresolved goals are +;;; simplified to: + +;;; Subgoal 2.2 +;;; (IMPLIES +;;; (AND (EXISTS-LOCAL-PEAK P) +;;; (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (CONSP (MULTISET-DIFF +;;; (CDR (PROOF-MEASURE (LOCAL-PEAK P))) +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). + +;;; Subgoal 1.2 +;;; (IMPLIES +;;; (AND (EXISTS-LOCAL-PEAK P) +;;; (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (FORALL-EXISTS-REL-BIGGER +;;; (MULTISET-DIFF (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (CDR (PROOF-MEASURE (LOCAL-PEAK P)))) +;;; (MULTISET-DIFF +;;; (CDR (PROOF-MEASURE (LOCAL-PEAK P))) +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). + + +;;; ············································································ +;;; 3.2.3 An explicit reference to the peak-element +;;; ············································································ + + +;;; Definition and properties of peak-element +;;; ········································· + +;;; See the definition in abstract-proofs.lisp + +(local + (defthm peak-element-member-proof-measure-local-peak + (implies (exists-local-peak p) + (member (peak-element p) (proof-measure (local-peak p)))))) + +(local + (defthm peak-element-rel-1 + (implies (exists-local-peak p) + (rel (elt1 (car (local-peak p))) + (peak-element p))))) + +(local + (defthm peak-element-rel-2 + (implies (exists-local-peak p) + (rel (elt2 (cadr (local-peak p))) + (peak-element p))))) + +(local + (defthm cdr-proof-measure-local-peak + (implies (exists-local-peak p) + (equal (cdr (proof-measure (local-peak p))) + (list (peak-element p)))))) +(local + (defthm p-local-peak + (implies (exists-local-peak p) + (q (peak-element p))))) + +(local (in-theory (disable peak-element))) + + +;;; Now our unresolved goals reduces to (note the explicit reference to +;;; the peak element): + +;;; Subgoal 2.2 +;;; (IMPLIES +;;; (AND (EXISTS-LOCAL-PEAK P) +;;; (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (CONSP (MULTISET-DIFF +;;; (LIST (PEAK-ELEMENT P)) +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). + +;;; Subgoal 1.2 +;;; (IMPLIES +;;; (AND (EXISTS-LOCAL-PEAK P) +;;; (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (FORALL-EXISTS-REL-BIGGER +;;; (ACL2::REMOVE-ONE +;;; (PEAK-ELEMENT P) +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))) +;;; (MULTISET-DIFF +;;; (LIST (PEAK-ELEMENT P)) +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P))))))). + + +;;; ············································································ +;;; 3.2.4 The peak element is bigger than any element of +;;; (transform-local-peak (local-peak p)) +;;; ············································································ + +;;; Definition of being bigger (w.r.t rel) than every element of a list +;;; ··································································· + +(local + (defun rel-bigger-than-list (x l) + (if (atom l) + t + (and (rel (car l) x) (rel-bigger-than-list x (cdr l)))))) + + +;;; Conditions assuring that an element m is rel-bigger-than-list than +;;; the elements of the proof-measure of a proof, when the proof is, +;;; respectively, steps-up or steps-down: +;;; ··································································· + +;;; A previous lemma: transitivity of rel is needed here + +(local + (defthm transitive-reduction + (implies (and + (legal e1 op) + (q e1) (q (reduce-one-step e1 op)) (q m) + (rel e1 m)) + (rel (reduce-one-step e1 op) m)) + :hints (("Goal" + :use (:instance rel-transitive + (x (reduce-one-step e1 op)) (y e1) (z m)))))) + +;;; And the two lemmas + +(local + (defthm steps-down-proof-measure-w-f-v + (implies (and (proof-p p) (steps-down p) (q m)) + (iff (rel-bigger-than-list m (proof-measure p)) + (if (consp p) + (rel (elt1 (car p)) m) + t))))) + +(local + (defthm steps-up-proof-measure-w-f-v + (implies (and (proof-p p) (steps-up p) (q m) + (if (consp p) (rel (elt2 (last-elt p)) m) t)) + (rel-bigger-than-list m (proof-measure p))))) + +;;; REMARKS: +;;; 1) The reverse implication in the steps-up case is not true as in +;;; the steps-down case. The reason is that the proof measure does not +;;; contain the final endpoint. + +;;; 2) The form of the rule allows one to distinguish between p empty or +;;; non-empty. + + +;;; In order to apply the two lemmas above we try to split +;;; (transform-local-peak (local-peak p)) in two proofs: the proof +;;; before the valley (steps-up) and the proof after the valley +;;; (steps-down). The following lemmas are needed for that purpose. +;;; ···································································· + +;;; If p is a proof, so they are the proofs after and before the +;;; valley. + +(local + (defthm proof-p-two-pieces-of-a-valley + (implies (proof-p p) + (and (proof-p (proof-before-valley p)) + (proof-p (proof-after-valley p)))))) + +;;; rel-bigger-than-list when the list is splitted in two pieces + +(local + (defthm rel-bigger-than-list-append + (equal + (rel-bigger-than-list x (append l1 l2)) + (and (rel-bigger-than-list x l1) + (rel-bigger-than-list x l2))))) + + + +;;; REMARK: In abstract-proofs.lisp it is also shown that +;;; (proof-before-valley p) is steps-up and that when p is a valley then +;;; (proof-after-valley p) is steps-down. And also the lemma +;;; proof-valley-append splits the proof in these two pieces. + + +;;; The transformed proof is a valley +;;; ································· + +(local + (defthm local-peak-local-peak-p + (implies (exists-local-peak p) + (local-peak-p (local-peak p))))) + + +(local + (defthm exists-local-peak-implies-proof-p-trasform-local-peak + (implies (exists-local-peak p) + (proof-p (local-peak p))))) + +(local + (defthm transform-local-peak-steps-valley + (implies (exists-local-peak p) + (steps-valley (transform-local-peak (local-peak p)))))) + +;;; We show a simplified expression of the endpoints of +;;; (transform-local-peak (local-peak p)) In this way, the lemmas +;;; peak-element-rel-1 and peak-element-rel-2 can be used to reveal the +;;; hypothesis of steps-down-proof-measure-w-f-v and +;;; steps-up-proof-measure-w-f-v (and then prove that the peak-element +;;; is bigger than every element of the complexities of the +;;; proof-after-valley and the proof-before-valley, respectively. +;;; ···································································· + + + +(local + (encapsulate + () + (local + (defthm endpoints-of-a-proof + (implies (and (equiv-p x y p) (consp p)) + (and (equal (elt1 (car p)) x) + (equal (elt2 (last-elt p)) y))))) + + (defthm endpoints-of-transform-of-a-local-peak + (implies (and (exists-local-peak p) + (consp (transform-local-peak (local-peak p)))) + (and (equal (elt1 (car (transform-local-peak (local-peak p)))) + (elt1 (car (local-peak p)))) + (equal (elt2 (last-elt (transform-local-peak (local-peak p)))) + (elt2 (cadr (local-peak p)))))) + :hints (("Goal" :use (:instance endpoints-of-a-proof + (x (elt1 (car (local-peak p)))) + (y (elt2 (cadr (local-peak p)))) + (p (transform-local-peak (local-peak p))))))))) + + +;;; Some technical lemmas +;;; ····················· + +(local + (defthm consp-proof-after-proof-instance + (let ((q (transform-local-peak (local-peak p)))) + (implies (consp (proof-after-valley q)) + (consp q))))) + +(local + (defthm consp-proof-before-proof-instance + (let ((q (transform-local-peak (local-peak p)))) + (implies (consp (proof-before-valley q)) + (consp q))))) + + +;;; And finally, the intended lemma +;;; ······························· + +(local + (defthm valley-rel-bigger-peak-lemma + (implies (exists-local-peak p) + (rel-bigger-than-list + (peak-element p) + (proof-measure (transform-local-peak (local-peak p))))) + :hints (("Goal" :use (:instance acl2::proof-valley-append + (acl2::p + (transform-local-peak (local-peak p)))))))) + + +;;; ············································································ +;;; 3.2.5 Using valley-rel-bigger-peak-lemma to simplify the goals +;;; ············································································ + +;;; The two unresolved goals, as stated at the end of 3.2.3, can be +;;; simplified to t by using the previously proved +;;; valley-rel-bigger-peak-lemma. This is lemma can be used for two +;;; purposes: + +;;; 1: Using multiset-diff-member (see multiset.lisp) and the +;;; following lemma (stating that the peak-element is not a member of +;;; the proof-meassure of the transformed proof), +;;; the calls to multiset-diff in the goals now disappear. +;;; ··································································· + +(local + (encapsulate + () + (local + (defthm rel-bigger-than-list-not-member + (implies (and (q x) (rel-bigger-than-list x l)) + (not (member x l))))) + + (defthm peak-element-not-member-proof-measure + (implies (exists-local-peak p) + (not (member (peak-element p) + (proof-measure (transform-local-peak + (local-peak p))))))))) + +;;; We are dealing with the cdr of the proof-measure: + +(local + (defthm not-member-cdr + (implies (not (member x l)) + (not (member x (cdr l)))))) + +;;; In this moment the only unresolved goal is: + +;;; Subgoal 1.2 +;;; (IMPLIES (AND (EXISTS-LOCAL-PEAK P) +;;; (CONSP (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (FORALL-EXISTS-REL-BIGGER +;;; (CDR (PROOF-MEASURE (TRANSFORM-LOCAL-PEAK (LOCAL-PEAK P)))) +;;; (LIST (PEAK-ELEMENT P)))). + + +;;; 2: Using the following lemma, the call to forall-exists-rel-bigger +;;; in the unresolved goal above, is reduced to a call to +;;; rel-bigger-than-list (and then valley-rel-bigger-peak-lemma will be +;;; applied) +;;; ··································································· + + +(local + (defthm rel-bigger-than-list-forall-exists-rel-bigger + (equal (forall-exists-rel-bigger l (list x)) + (rel-bigger-than-list x l)))) + +;;; We are dealing with the cdr of the proof-measure: +(local + (defthm rel-bigger-than-list-cdr + (implies (rel-bigger-than-list x l) + (rel-bigger-than-list x (cdr l))))) + +;;; With this two rules altogether with valley-rel-bigger-peak-lemma our +;;; unresolved goal becomes T, so we have: + +;;; ············································································ +;;; 3.2.6 The main lemma of this book +;;; ············································································ + +(defthm transform-to-valley-admission + (implies (exists-local-peak p) + (mul-rel (proof-measure (replace-local-peak p)) + (proof-measure p)))) + +;;; ············································································ +;;; 3.2.7 Some final technical events +;;; ············································································ + +;;; Needed in the admission proof of transform-to-valley + +(local + (defthm mul-rel-nil + (implies (consp l) + (mul-rel nil l)))) + +(local + (defthm exists-local-peak-proof-measure-consp + (implies (exists-local-peak p) + (consp (proof-measure p))))) + +(local (in-theory (disable mul-rel + proof-measure-with-local-peak + replace-local-peak-another-definition))) + + +;;; ---------------------------------------------------------------------------- +;;; 3.3 The definition of transform-to-valley +;;; ---------------------------------------------------------------------------- + + +(defun transform-to-valley (p) + (declare (xargs :measure (if (steps-q p) (proof-measure p) nil) + :well-founded-relation mul-rel)) + (if (and (steps-q p) (exists-local-peak p)) + (transform-to-valley (replace-local-peak p)) + p)) + + + + +;;; ============================================================================ +;;; 4. Properties of transform-to-valley (Newman's lemma) +;;; ============================================================================ + +;;; ---------------------------------------------------------------------------- +;;; 4.1 Some previous events +;;; ---------------------------------------------------------------------------- + +;;; ············································································· +;;; 4.1.1 Previous rules needed to show that (transform-to-valley p) is eqv. to p +;;; ············································································· + + +;;; We have to see that (replace-local-peak p) is equivalent to p +;;; ····························································· + +;;; An useful rule to deal with concatenation of proofs +(local + (defthm proof-append + (implies (equal z (last-of-proof x p1)) + (equal (equiv-p x y (append p1 p2)) + (and (equiv-p x z p1) + (equiv-p z y p2)))))) + +;;; Last element of a local peak +(local + (defthm last-element-of-a-local-peak + (implies (local-peak-p p) + (equal (last-elt p) (cadr p))))) + +;;; The case where (transform-local-peak (local-peak p)) is empty: + +(local + (defthm atom-proof-endpoints-are-equal + (implies (and (equiv-p x y p) (atom p)) + (equal x y)) + :rule-classes nil)) + +(local + (defthm atom-transform-local-peak-forward-chaining-rule + (implies (and + (not (consp (transform-local-peak (local-peak p)))) + (exists-local-peak p) + (equiv-p x y (local-peak p))) + (equal x y)) + :hints (("Goal" :use ((:instance atom-proof-endpoints-are-equal + (p (transform-local-peak (local-peak p))))))) + :rule-classes :forward-chaining)) + +;;; REMARK: interesting use of forward-chaining. + +;;; In the following bridge lemma it is fundamental +;;; replace-local-peak-another-definition and the case distinction +;;; generated by proof-append: + +(local + (defthm equiv-p-x-y-replace-local-peak-bridge-lemma + (implies (and (exists-local-peak p) + (equiv-p x y (append + (proof-before-peak p) + (append (local-peak p) + (proof-after-peak p))))) + (equiv-p x y (replace-local-peak p))) + :hints (("Goal" + :in-theory (enable replace-local-peak-another-definition))))) + +;;; And finally the intended lemma: + +(local + (defthm equiv-p-x-y-replace-local-peak + (implies (and (equiv-p x y p) (exists-local-peak p)) + (equiv-p x y (replace-local-peak p))) + :hints (("Goal" :in-theory (enable proof-peak-append))))) + +;;; REMARK: It's interesting how we avoid explicit expansion of the +;;; three pieces of p (before, at and after the peak), using the +;;; previous bridge lemma. + +;;; ············································································· +;;; 4.1.2 A rule needed to show that (transform-to-valley p) is a valley +;;; ············································································· + + + +;;; If a proof does not have local peaks, then it is a valley: + +(local + (defthm steps-valley-not-exists-local-peak + (implies (equiv-p x y p) + (equal (steps-valley p) (not (exists-local-peak p)))))) + +;;; ············································································· +;;; 4.1.3 If equiv-p, then steps-q +;;; ············································································· + +(local + (defthm equiv-p-implies-stetps-q + (implies (equiv-p x y p) + (steps-q p)) + :rule-classes :forward-chaining)) + +;;; ············································································· +;;; 4.1.4 Disabling the induction rule for equiv-p +;;; ············································································· + + +(local (in-theory (disable equiv-p-induct))) + +;;; REMARK: It is important to disable the induction rule of equiv-p +;;; because we want the two main properties of transform-to-valley +;;; to be proved by the induction suggested by transform-to-valley +;;; (i.e. and induction based on the multiset relation mul-rel) + + +;;; ---------------------------------------------------------------------------- +;;; 4.2 The intended properties of transform-to-valley +;;; ---------------------------------------------------------------------------- + + +;;; It returns an equivalent proof +;;; ······························ + + +(defthm equiv-p-x-y-transform-to-valley + (implies (equiv-p x y p) + (equiv-p x y (transform-to-valley p)))) + + + + +;;; It returns a valley proof +;;; ························· + + +(defthm valley-transform-to-valley + (implies (equiv-p x y p) + (steps-valley (transform-to-valley p)))) + + +;;; CONCLUSION: +;;; The definition of transform-to-valley and the theorems +;;; equiv-p-x-y-transform-to-valley and valley-transform-to-valley prove +;;; the Newman's lemma + + + + + + + + + |