; (certify-book "perm-quicksort-via-congruence")
(in-package "ACL2")
(include-book "quicksort")
(defun rm (e x)
(if (consp x)
(if (equal e (car x))
(cdr x)
(cons (car x) (rm e (cdr x))))
nil))
(defun memb (e x)
(if (consp x)
(or (equal e (car x))
(memb e (cdr x)))
nil))
(defun perm (x y)
(if (consp x)
(and (memb (car x) y)
(perm (cdr x) (rm (car x) y)))
(not (consp y))))
; Perm is an equivalence relation, that is, it is reflexive, symmetric, and
; transitive. We prove those three lemmas and then ask ACL2 (in the
; ``defequiv'' below) to treat perm as an equivalence. I hide the ``junk
; lemmas'' I used to prove each of the three main lemmas. I'll talk about this
; in class. But basically I don't want my data base of known lemmas to get
; cluttered up with special-purpose rules I proved for particular main goals.
; That way you can focus on the proof of each main goal separately rather than
; trying to keep in mind a rewriting strategy that proves all three of them.
(defthm perm-reflexive
(perm x x))
(encapsulate
nil
(local
(defthm perm-symmetric-lemma ; Subgoal *1/2'''
(IMPLIES (AND (MEMB X1 Y)
(PERM (RM X1 Y) X2)
; (PERM X2 (RM X1 Y))
)
(PERM Y (CONS X1 X2)))
:hints (("Goal" :induct (perm y x2)))))
(defthm perm-symmetric
(implies (perm x y)
(perm y x))))
(encapsulate
nil
(local
(defthm memb-rm
(implies (memb a (rm b x)) (memb a x))))
(local
(defthm perm-memb
(implies (and (perm x y)
(memb a x))
(memb a y))))
(local
(defthm comm-rm
(equal (rm a (rm b x)) (rm b (rm a x)))))
(local
(defthm perm-rm
(implies (perm x y)
(perm (rm a x) (rm a y)))))
; We now prove transitivity, by giving a hint.
(defthm perm-transitive
(implies (and (perm x y) (perm y z)) (perm x z))
:hints (("Goal" :induct (and (perm x y) (perm x z))))))
(defequiv perm)
; Next, we prove that perm is congruence relation for certain functions. See
; doc congruence. A ``congruence rule'' is a formula of the form
; (implies (equiv1 x y)
; (equiv2 (fn x a b)
; (fn y a b))).
; where equiv1 and equiv2 are known equivalence relations.
; This congruence rule tells us that the x in (fn x a b) can be replaced by y
; and the result is equiv2 to (fn x a b), provided y is equiv2 to x.
; Practically speaking it means that when ACL2 rewrites an (fn x a b)
; expression while trying to ensure that the equiv2 is preserved, it can
; rewrite x while ensuring that equiv1 is preserved.
; This idea is so basic to congruence-based reasoning that ACL2 provides
; a macro for it. The above congruence rule can be abbreviated:
; (defcong equiv1 equiv2 (fn x a b) 1)
; The ``1'' tells us which argument can be replaced.
; Here are some ``obvious'' perm congruences.
(defcong perm perm (cons x y) 2)
(defcong perm perm (append x y) 1)
(defcong perm perm (append x y) 2)
(defcong perm equal (memb e x) 2)
(defcong perm perm (rm e x) 2)
(defcong perm perm (remove-gt e x) 2)
(defcong perm perm (remove-lte e x) 2)
; We've now got the fundamentals in place to think about quicksort's perm
; property. We want to prove that (quicksort x) is a perm of x. If we attack
; that following The Method we see the need for the lemma append-removes, and
; if we attack that with The Method we see the need for append-cons.
; It is helpful to think of perm the way way you probably think of EQUAL. For
; example, the lemma below means (append a (cons e b)) CAN BE REPLACED BY (cons
; e (append a b)) -- in positions where perm is a congruence.
(defthm append-cons
(perm (append a (cons e b))
(cons e (append a b))))
(defthm append-removes
(perm (append (remove-gt e a)
(cons e
(remove-lte e a)))
(cons e a)))
(defthm perm-quicksort
(perm (quicksort x) x))
; Note that this last theorem tells ACL2 that (quicksort x) CAN BE REPLACED BY
; x, in positions where perm is a congruence. That is, it's a very powerful
; rewrite rule that eliminates quicksort.