;;; newman.lisp
;;; A mechanical proof of Newman's lemma for abstract reduction relations
;;; Created: 6-8-99 Last revison: 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 "NWM" (cons 'multiset-diff *cnf-package-exports*))
(certify-book "newman" 3)
|#
(in-package "NWM")
(include-book "../../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 partial order
;;; ----------------------------------------------------------------------------
;;; A general noetherian partial order rel is defined.
;;; It will be used 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.
(encapsulate
((rel (x y) booleanp)
(fn (x) e0-ordinalp))
(local (defun rel (x y) (declare (ignore x y)) nil))
(local (defun fn (x) (declare (ignore x)) 1))
(defthm rel-well-founded-relation-on-mp
(and
(e0-ordinalp (fn x))
(implies (rel x y)
(e0-ord-< (fn x) (fn y))))
:rule-classes (:well-founded-relation
:rewrite))
(defthm rel-transitive
(implies (and (rel x y) (rel y z))
(rel x z))
:rule-classes nil))
;;; A theorem: irreflexivity of rel
(local
(defthm rel-irreflexive
(not (rel x x))
:hints (("Goal"
:use ((:instance rel-well-founded-relation-on-mp
(y x)))))))
;;; REMARK: e0-ord-irreflexive (in multiset.lisp) is needed
;;; ----------------------------------------------------------------------------
;;; 1.2 A noetherian locally confluent relation
;;; ----------------------------------------------------------------------------
;;; A general reduction is given by two functions: reduction-one-step
;;; and legal. Noetherianity is justified by inclusion in the previously
;;; defined well-founded relation on rel. Local confluence is defined by
;;; the existence of a function transform-local-peak, assumed to
;;; transform every local peak to an equivalent valley proof.
(encapsulate
((legal (x u) boolean)
(reduce-one-step (x u) element)
(transform-local-peak (x) proof))
(local (defun legal (x u) (declare (ignore x u)) nil))
(local (defun reduce-one-step (x u) (+ x u)))
(local (defun transform-local-peak (x) (declare (ignore x)) nil))
(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)))))
(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)))))
(defthm noetherian
(implies (legal x u) (rel (reduce-one-step x u) x))))
;;; ----------------------------------------------------------------------------
;;; 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
(local
(defun proof-p (p)
(if (atom p)
t
(and (proof-step-p (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))
(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))))
;;; 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. 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-MP T FN X Y)
(acl2::defmul (REL REL-WELL-FOUNDED-RELATION-ON-MP T FN X Y)
:verify-guards t)
;;; This defmul call define the well-founded multiset relation mul-rel,
;;; induced by the well-founded relation rel.
;;; So our admission hint will be (see the definition of proof-measure
;;; in abstract-proofs.lisp).
;(defun transform-to-valley (p)
; (declare (xargs :measure (proof-measure p)
; :well-founded-relation mul-rel))
; (if (not (exists-local-peak p))
; p
; (transform-to-valley (replace-local-peak 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)
;;; 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 measures 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 see 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 complexity of 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 (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)
(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))
(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)
(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 (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)))
:rule-classes nil)
;;; ----------------------------------------------------------------------------
;;; 3.3 The definition of transform-to-valley
;;; ----------------------------------------------------------------------------
(defun transform-to-valley (p)
(declare (xargs :measure (proof-measure p)
:well-founded-relation mul-rel
:hints (("Goal" :use
(:instance transform-to-valley-admission)))))
(if (not (exists-local-peak p))
p
(transform-to-valley (replace-local-peak 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)))))
(local (in-theory (disable 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 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