#|

Author: Pete Manolios
Date:   9/21/2018

Code used in lecture 5 of Computer-Aided Reasoning.

|#

(in-package "ACL2S")
(set-gag-mode nil)

"BEGIN DEMO 1
"

"Writing (true-listp x) is tedious. Let's use a macro.
"

(defmacro tlp (x)
  `(true-listp ,x))

"Append and rev are built-in to ACL2s, so let's define
new, equivalent functions.
"

(defunc app (a b)
  :input-contract (and (tlp a) (tlp b))
  :output-contract (tlp (app a b))
  (if (endp a)
      b
    (cons (car a) 
          (app (cdr a) b))))

(app '(1 2 3) '(4 5 6))

(defunc rv (x)
  :input-contract (tlp x)
  :output-contract (tlp (rv x))
  (if (endp x)
      nil
    (app (rv (cdr x))
         (list (car x)))))

(rv '(1 2 3))

#|

This is a classic example that shows ACL2 going through all of the
proof procedures.

|#

(defthm rev-rev
  (implies (tlp x)
           (equal (rv (rv x))
                  x)))