;;; confluence.lisp
;;; Church-Rosser and normalizing abstract reductions.
;;; Created: 06-10-2000 Last Revision: 06-10-2000
;;; =============================================================================
;;; 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
;;; ********************************************************************
;;; ********* IMPORTANT REMARK:
;;; See the comments in the book confluence-v0.lisp
;;; ============================================================================
;;; 1. Definition of a normalizing and (CR) abstract reduction
;;; ============================================================================
(encapsulate
((legal (x u) boolean)
(reduce-one-step (x u) element)
(transform-to-valley (x) valley-proof)
(proof-irreducible (x) proof))
(local (defun legal (x u) (declare (ignore x u)) nil))
(local (defun reduce-one-step (x u) (+ x u)))
(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))))))
(defun equiv-p (x y p)
(if (endp p)
(equal x y)
(and (proof-step-p (car p))
(equal x (elt1 (car p)))
(equiv-p (elt2 (car p)) y (cdr p)))))
(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)))))
(local (defun proof-irreducible (x) (declare (ignore x)) nil))
(defthm normalizing
(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))))))
;;; ----------------------------------------------------------------------------
;;; 1.1 Useful rules
;;; ----------------------------------------------------------------------------
;;; Two useful rewrite rules about normalizing
(local
(defthm normalizing-not-consp-proof-irreducible
(implies (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 (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)))))
;;; 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 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))))
;;; ---------------------------------------------------------------------------
;;; 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 containing reduction steps.
;;; REMARK: To say it properly, we show that for the relation
;;; "exists p such that (equiv-p x y 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))))))
;;; The properties of equivalence relations are met by equiv-p
(defthm equiv-p-reflexive
(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)
;;; REMARK: 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.
;;; Obviously, the reduction relaton is contained in equiv-p
(defthm equiv-p-contains-reduction
(implies (legal 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)))))
;;; Let us assume that we have a relation eqv of equivalence, 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 (legal x op)
(eqv x (reduce-one-step x op))))
(defthm eqv-reflexive
(eqv x x))
(defthm eqv-symmetric
(implies (eqv x y) (eqv y x)))
(defthm eqv-transitive
(implies (and (eqv x y) (eqv y z))
(eqv x z))))
(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 with 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.
;;; ============================================================================
;;; 2. Decidability of Church-Rosser and normalizing redutions
;;; ============================================================================
;;; ----------------------------------------------------------------------------
;;; 2.1 Normal forms, definition and fundamental properties.
;;; ----------------------------------------------------------------------------
(defun normal-form (x) (last-of-proof x (proof-irreducible x)))
(local
(defthm irreducible-normal-form (not (legal (normal-form x) op))))
(local
(defthm equivalent-proof
(equiv-p x (normal-form x) (proof-irreducible x))))
(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->]*
;;; ----------------------------------------------------------------------------
(defun r-equiv (x y)
(equal (normal-form x) (normal-form y)))
;;; ············································································
;;; 2.2.1 Completeness
;;; ············································································
;;; A proof between normal forms
(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 (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)))
;;; 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
;;; ············································································
;;; A proof between x and y (if their normal forms are equal)
(defun make-proof-common-n-f (x y)
(append (proof-irreducible x) (inverse-proof (proof-irreducible y))))
;;; SOUNDNESS
(defthm r-equiv-sound
(implies (r-equiv x y)
(equiv-p x y (make-proof-common-n-f x y)))
:hints (("Goal" :use (:instance
equiv-p-symmetric
(x y)
(y (normal-form y))
(p (proof-irreducible y))))))
;;; REMARK: :use is needed due to a weird behaviour that sometimes
;;; ACL2 has with equalities in hypotesis.