(in-package "ACL2")

; See perm-rev.lisp for description of an interactive session.
; Here, we have taken the results of that session to create a
; certifiable book.  Normally, an ACL2 user would be developing
; this file during the session.

(defun mem (a lst)
; Return t if a is a member of the list, lst, else nil.
; This definition is typical in style for list processing.
; The termination proof obligation, important for
; soundness, is discharged automatically.
  (cond ((atom lst)
         nil)
        ((equal a (car lst))
         t)
        (t
         (mem a (cdr lst)))))

(defun del (a lst)
; This function deletes the first occurrence of a (if any)
; in the list, lst.
  (cond ((atom lst)
         nil)
        ((equal a (car lst))
         (cdr lst))
        (t
         (cons (car lst)
               (del a (cdr lst))))))

(defun perm (lst1 lst2)
; Given two lists, return t if lst1 is a permutation of lst2.
; An alternate approach uses "how-many"... for another demo.
  (cond ((atom lst1)
         (atom lst2))
        ((mem (car lst1) lst2)
         (perm (cdr lst1)
               (del (car lst1) lst2)))
        (t
         nil)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Prove that the permutation relation is an equivalence relation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defthm perm-reflexive
; We start with this, towards proving that perm is an
; equivalence relation.
  (perm x x))

(local
 (defthm perm-symmetric-lemma
   (implies (and (consp x)
                 (mem (car x) y)
                 (perm (del (car x) y) (cdr x)))
            (perm y x))))

(defthm perm-symmetric
  (implies (perm x y)
           (perm y x)))

(defthm mem-del ; for perm-del-del
  (implies (and (not (equal a b))
                (mem b z))
           (mem b (del a z))))

(defthm del-del ; for perm-del-del
  (equal (del a (del b x))
         (del b (del a x))))

(defthm perm-del-del ; last lemma needed for perm-transitive
  (implies (perm y z)
           (perm (del a y) (del a z))))

(defthm mem-del-implies-mem ; for not-perm-if-different-members
; Contraposed form avoids free variables in the hypothesis.
  (implies (not (mem a z))
           (not (mem a (del b z)))))

(defthm not-perm-if-different-members
  (implies (and (not (mem a z))
                (mem a y))
           (not (perm y z))))

(defthm perm-transitive
  (implies (and (perm x y) (perm y z))
           (perm x z)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define a list reverse function and prove the reverse of a list
; is a permutation of that list.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(defun app (x y)
  (if (consp x)
      (cons (car x) (app (cdr x) y))
    y))

(defun rev (x)
  (if (consp x)
      (app (rev (cdr x)) (cons (car x) nil))
    nil))

(defthm rev-is-id-with-generalization
  (perm (rev x) x)
  :rule-classes nil) ; prevent this from being used below

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Prove rev-is-id without getting lucky with generalization, by
; using congruenced-based rewriting.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; We got lucky.  Let's try again without using generalization.

(defequiv perm) ; store rule that perm is an equivalence relation

(defthm mem-app
  (equal (mem a (app x y))
         (or (mem a x)
             (mem a y))))

(defcong perm perm (app x y) 1)

(defthm app-commutative
   (perm (app x y)
         (app y x))
   :rule-classes nil)

(local
 (defthm rev-is-id-lemma
   (implies (consp x)
            (perm (app (cdr x) (list (car x)))
                  x))
   :hints (("Goal" :use ((:instance
                          app-commutative
                          (x (cdr x))
                          (y (list (car x)))))))))

(defthm rev-is-id
  (perm (rev x) x)
  :hints (("Goal" :do-not '(generalize))))