; (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.