(+ 3 4) ; starting example: read-eval-print loop

; This demo illustrates typical ACL2 interaction by showing the
; development of a proof that the reverse of a list is a
; permutation of that list.  We accomplish this in the following
; steps:

; Define a permutation relation

; Prove that the permutation relation is an equivalence relation

; Define a list reverse function

; Show how an attempt to prove our main goal leads to a desire to
; use congruence-based reasoning

; Prove the main goal, that the reverse a list is a permutation
; of that list

; Clean up and certify a book

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Define a permutation relation
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; Our first goal is to define a permutation relation, perm, and
; prove that it is an equivalence relation.  First we define
; functions for deleting an element of a list and membership in a
; list.  Notice that because these three functions are defined
; with recursion, there is a termination proof obligation for
; each --- without termination obligations one can get
; inconsistency, for example defining f(x) = not f(x).  ACL2
; discharges these termination proof obligations automatically.

(value-triple
 "Section: Define a permutation relation.")

; The following definition is typical in style for list
; processing.  The termination proof obligation, important for
; soundness, is discharged automatically.

(defun mem (a lst)
; Return t if a is a member of the list, lst, else nil.
  (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.
; NOTE! An alternate (easier?) approach uses "how-many".
  (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
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(value-triple
 "Section: Prove that perm is an equivalence relation.")

(defthm perm-reflexive
  (perm x x))

(defthm perm-symmetric ; FAILS!!
  (implies (perm x y)
           (perm y x)))

#||
We get this summary report:

  *** Key checkpoint at the top level: ***

  Goal
  (IMPLIES (PERM X Y) (PERM Y X))

  *** Key checkpoint under a top-level induction: ***

  Subgoal *1/3''
  (IMPLIES (AND (CONSP X)
                (MEM (CAR X) Y)
                (PERM (DEL (CAR X) Y) (CDR X))
                (PERM (CDR X) (DEL (CAR X) Y)))
           (PERM Y X))

If we omit the last hypothesis we have a plausible lemma, which we
hope can be proved by induction.  The proof does in fact succeed.

||#

(set-gag-mode :goals) ; eliminate unnececessary output

(defthm perm-symmetric ; FAILS!! --- quicker, less output
  (implies (perm x y)
           (perm y x)))

(defthm perm-symmetric-lemma
  (implies (and (consp x)
                (mem (car x) y)
                (perm (del (car x) y) (cdr x)))
           (perm y x))) ; i.e., (iff (perm y x) t)

; And now the proof of perm-symmetric succeeds.

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

(defthm perm-transitive ; FAILS!!
  (implies (and (perm x y) (perm y z))
           (perm x z)))

#||
We get the following key checkpoints:

  Subgoal *1/5''
  (IMPLIES (AND (CONSP X)
                (NOT (MEM (CAR X) Z))
                (MEM (CAR X) Y)
                (PERM (CDR X) (DEL (CAR X) Y)))
           (NOT (PERM Y Z)))

  Subgoal *1/3''
  (IMPLIES (AND (CONSP X)
                (MEM (CAR X) Z)
                (NOT (PERM (DEL (CAR X) Y) (DEL (CAR X) Z)))
                (MEM (CAR X) Y)
                (PERM (CDR X) (DEL (CAR X) Y))
                (PERM Y Z))
           (PERM (CDR X) (DEL (CAR X) Z)))

Let's start with the second one.  Notice the contradiction
between its third and final hypotheses.  So we try to prove:

||#

(defthm perm-del-del ; FAILS!!
  (implies (perm y z)
           (perm (del a y) (del a z))))

#||
But we get these key checkpoints, which respectively suggest the
two lemmas following just below.  Notice that the second is)
"permutative" --- ACL2 will use it to put terms (del a (del b x))
in normal form based on a syntactic term-order between (the
instances at hand of) a and b.

  Subgoal *1/4.2
  (IMPLIES (AND (CONSP Y)
                (NOT (EQUAL A (CAR Y)))
                (PERM (DEL A (CDR Y))
                      (DEL A (DEL (CAR Y) Z)))
                (MEM (CAR Y) Z)
                (PERM (CDR Y) (DEL (CAR Y) Z)))
           (MEM (CAR Y) (DEL A Z)))

  Subgoal *1/4.1
  (IMPLIES (AND (CONSP Y)
                (NOT (EQUAL A (CAR Y)))
                (PERM (DEL A (CDR Y))
                      (DEL A (DEL (CAR Y) Z)))
                (MEM (CAR Y) Z)
                (PERM (CDR Y) (DEL (CAR Y) Z)))
           (PERM (DEL A (CDR Y))
                 (DEL (CAR Y) (DEL A Z))))
||#

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

:pl mem

:pl (mem x (del y z))

:pl (mem x (mem y z))

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

(defthm perm-del-del
  (implies (perm y z)
           (perm (del a y) (del a z))))

; Now we try again:

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

; We get the checkpoint "Subgoal *1/5''" shown earlier.
; Inspection suggests this lemma, which fails.

; The following is stored as though its conclusion had been
; (equal (perm x y) nil).
(defthm not-perm-if-different-members ; FAILS!!
  (implies (and (not (mem a z))
                (mem a y))
           (not (perm y z))))

#||
Fails with this key checkpoint:

  Subgoal *1/2''
  (IMPLIES (AND (CONSP Y)
                (MEM (CAR Y) Z)
                (MEM A (DEL (CAR Y) Z))
                (NOT (MEM A Z))
                (MEM A (CDR Y)))
           (NOT (PERM (CDR Y) (DEL (CAR Y) Z))))

Clearly the third and fourth hypotheses are contradictory.  So we
formulate the following lemma stating that as a conditional
rewrite rule, where ACL2 actually interprets the conclusion as
rewriting instances of (mem a (del b z)) to nil (false) when it
can establish the corresponding instance of the hypothesis.  If
we instead had
  (implies (not (mem a (del b z)))
           (not (mem a z)))
then ACL2 would have to search for a suitable b.

||#

; The following is stored as though its conclusion had been
; (equal (mem a (del b z)) nil).
(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))))

; Finally we can prove:

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

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

(value-triple
 "Section: Define rev and prove (rev x) is a perm of x.")

(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
  (perm (rev x) x))

:pso ; We got lucky, as generalization actually worked!

:pbt 0 ; Where are we?

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

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

; First, undo:

:u ; undo last command

:pbt 0 ; Where are we?

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

#||
Key checkpoint:

  Subgoal *1/1'
  (IMPLIES (AND (CONSP X)
                (PERM (REV (CDR X)) (CDR X)))
           (PERM (APP (REV (CDR X)) (LIST (CAR X)))
                 X))
||#

; Our strategy now has two parts:
; (1) Substitute the second hypothesis into the conclusion, by
;     ``treating PERM as equality'' in the first argument of a
;     call of APP.
; (2) Commute the arguments of PERM.

(value-triple
 "Plan:
  (1) substitute hypothesis into conclusion;
  (2) commute arguments of PERM.")

; Let's start with (1).

(defequiv perm) ; store rule: perm is an equiv. relation

:trans1 (defcong perm perm (app x y) 1) ; our next step

(defcong perm perm (app x y) 1) ; FAILS!! - must interrupt

(skip-proofs ; defer proof until we see if this helps
 (defcong perm perm (app x y) 1))

(defthm rev-is-id ; FAILS!! - but did desired substitution
  (perm (rev x) x)
  :hints (("Goal" :do-not '(generalize))))

#||
We see the following key checkpoint from the latest attempt above
at rev-is-id:

  Subgoal *1/1'
  (IMPLIES (AND (CONSP X)
                (PERM (REV (CDR X)) (CDR X)))
           (PERM (APP (CDR X) (LIST (CAR X))) X))
||#

; So now we move to (2):

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

(skip-proofs ; defer proof
 (defthm app-commutative
   (perm (app x y)
         (app y x))
   :rule-classes nil))

(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))))

:pbt 0 ; Where are we?

:ubt 16 ; Undo the defcong.

(defcong perm perm (app x y) 1) ; FAILS!! --- must interrupt

#||
Key checkpoint:

  Subgoal *1/2.2
  (IMPLIES (AND (CONSP X)
                (PERM (APP (CDR X) Y)
                      (APP (DEL (CAR X) X-EQUIV) Y))
                (MEM (CAR X) X-EQUIV)
                (PERM (CDR X) (DEL (CAR X) X-EQUIV)))
           (MEM (CAR X) (APP X-EQUIV Y)))
||#

(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 ; succeeds; uses mem-app
   (perm (app x y)
         (app y x))
   :rule-classes nil)

(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))))

(value-triple
 "DONE!  Now certify a book.
  Normally, an ACL2 user would be developing this file
  during the session.")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Clean up and certify a book
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

; See file perm-rev-book.lisp for a corresponding book that can
; be processed by certify-book.  It adds an initial in-package
; event (needed by the host Lisp compiler) and make a couple of
; events LOCAL.

; Then this book could be part of a library for reasoning about
; the functions it defines.  Including the book is typically much
; faster than doing the proofs, and it also loads compiled code.