#|

Author: Pete Manolios
Date:   9/28/2018

Code used in lecture 7 of Computer-Aided Reasoning.  

|#

(in-package "ACL2S")

(include-book "kestrel/utilities/proof-builder-macros" :dir :system)
(set-gag-mode nil)
(defmacro tlp (x) `(true-listp ,x))

#|

Topics:

  Macros 
  Books
  State/World
  Performance issues: accumulated persistence
  Libraries

|#

"We have seen that append is a macro that allows multiple arguments.
For example.
"

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

"Let's see how append is defined.
"

:pe append

"So notice what is reported. That append is a macro alias for 
the function binary-append. This allow us/ACL2 to use/display 
append instead of binary-append in certain contexts. For
example: notice the output below refers to append "

(thm (implies (and (tlp x) (tlp y) (or (null x) (null y)))
              (equal (append x y)
                     (append y x))))

"But if we define app as follows.
"

(defunc binary-app (x y)
  :input-contract (and (tlp x) (tlp y))
  :output-contract (tlp (binary-app x y))
  (if (endp x)
      y
    (cons (car x)
          (binary-app (cdr x) y))))

(defmacro app (&rest rst)
  (cond ((null rst) nil)
        ((null (cdr rst)) (car rst))
        (t (xxxjoin 'binary-app rst))))

"And now we try proving the same thms as before, notice the output
below refers to binary-app "

(thm (implies (and (tlp x) (tlp y) (or (null x) (null y)))
              (equal (app x y)
                     (app y x))))

"Let's look at the documentation for macro-aliases-table and 
add-macro-fn to see the append, binary-append thing works.
"

:doc acl2::macro-aliases-table
:doc acl2::add-macro-fn

(add-macro-fn app binary-app)

"Download a local copy of the ACL2 manual and you can use your browser
to search the documentation.
"

"And now we try proving the same thm as before,
notice the output below refers to app, not binary-app "

(thm (implies (and (tlp x) (tlp y) (or (null x) (null y)))
              (equal (app x y)
                     (app y x))))

"Let's do that for tlp too! And then try the thm again.
But first, let's write a macro to do this."

:ubt :x-1

(defmacro make-binary-macro (bin-fun macro id)
  `(progn
     (defmacro ,macro (&rest rst)
       (cond ((null rst) ,id)
             ((null (cdr rst)) (car rst))
             (t (xxxjoin ',bin-fun rst))))
     (add-macro-fn ,macro ,bin-fun)))
                                     
:trans1 (make-binary-macro binary-app app nil)
(make-binary-macro binary-app app nil)

(add-macro-fn tlp true-listp)

(thm (implies (and (tlp x) (tlp y) (or (null x) (null y)))
              (equal (app x y)
                     (app y x))))

"Notice that such macros are also supported in the proof builder
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions (pro bash pp p))

exit

"Let's say that we want to prove the conjecture using the proof
builder. We can use the powerful prove command.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions (prove))

exit

"Let's say that we want to have more control since prove can
generalize. We just want to use induction and simplification.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((do-all induct bash)))

goals
th
exit

"Since induction generated multiple subgoals, we may want to apply
bash to all of them.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((do-all induct (repeat bash))))

goals
th
exit

"But we still have another goal and that requires induction.
So, let's repeat once more.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((repeat (do-all induct (repeat bash)))))

exit

"Oops. Infinite loop.

It would be nice to have an instruction that allows us to repeatedly
apply instructions until all goals have been proved.

Here is how we can do that. We essentially define a macro, which
is a new tactic.

Macros are described in the reading material, CAR, but let's
use :doc to remind ourselves how to define macros.
"

:doc defmacro

"There is a lot of information about macros. See the following.
"

:doc acl2::macros

"There is support for defining proof builder macros. Here is a
documentation topic.
"

:doc define-pc-macro

(define-pc-macro repeat-until-done (&rest instrs)
  (value
   `(repeat (do-all
             ,@(append instrs 
                       `((negate (when-not-proved fail))))))))

"There is even a mechanism for creating documentation for the ACL2
manual.
"

(defxdoc acl2-pc::repeat-until-done
  :parents (proof-builder-commands)
  :short "(macro)
Repeat the given instructions until all goals have been proved"
  :long "@({
 Example:
 (repeat-until-done induct (repeat bash))

 General Form:
 (repeat-until-done instr1 ... instrk)
 })

 <p>where each @('instri') is a proof-builder instruction.</p>")


"Now use let's use our new macro.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((repeat-until-done induct (repeat bash))))

exit

"And if we want to generate a dummy defthm whose proof uses
the proof builder, we can do this.
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((repeat-until-done induct (repeat bash))
                (exit t)))

"If we want to generate a defthm, named my-thm, with rule-classes nil,
we can do this. 
"

(verify
 (implies (and (tlp x) (tlp y) (or (null x) (null y)))
          (equal (app x y)
                 (app y x)))
 :instructions ((repeat-until-done induct (repeat bash))
                (exit my-thm nil)))

y

"Let's look at some other examples of macros. Here is an example when
we discussed defdata. Defdata is a macro, so let's see what it
translates into."

:trans1
(defdata file (list string nat))

"Notice the with-output form.

It allows us to control how much output a user sees.

So, if something fails, or if we want to explore, we can strip that
out.

Next, let's look at the defdata::defdata-events form.
"

(DEFDATA::DEFDATA-EVENTS
  (DEFDATA::PARSE-DEFDATA '(FILE (LIST STRING NAT))
    (CURRENT-PACKAGE STATE)
    (W STATE))
  (W STATE))

"First, notice state and (w state), the world.

The ACL2 logical world is a data structure that includes all logical
content resulting from the commands evaluated.  The world includes a
representation of the current logical theory, as well as some
extra-logical information such as the values of ACL2 tables.

Let's look at the documentation on state.
"

"Back to the defdata.
Again, we can pull out the with-output body, which is a progn and we
can submit each argument to the progn to ACL2 to see what happens.  We
won't do that, but notice the definitions of the recognizer, the
enumerator and a version of the enumerator that takes a seed:

     (DEFUN FILEP (DEFDATA::V1)
     (DEFUN NTH-FILE-BUILTIN (DEFDATA::I1)
     (DEFUN NTH-FILE/ACC-BUILTIN (DEFDATA::SIZE1 DEFDATA::_SEED)

Let's submit this.
"

(defdata file (list string nat))

"Now, the more interesting form.
"

:trans1
(defdata 
  (dir (list string dir-file-list))
  (dir-file-list (listof file-dir))
  (file-dir (oneof file dir)))

"As before, let's look at the defdata::defdata-events form.
"

(DEFDATA::DEFDATA-EVENTS
  (DEFDATA::PARSE-DEFDATA '((DIR (LIST STRING DIR-FILE-LIST))
                            (DIR-FILE-LIST (LISTOF FILE-DIR))
                            (FILE-DIR (ONEOF FILE DIR)))
    (CURRENT-PACKAGE STATE)
    (W STATE))
  (W STATE))


"I bring your attention to the following form that shows how to
define mutually recursive functions. I remove package names
to make this more readable.

(MUTUAL-RECURSION
 (DEFUN DIRP (V1)
   (DECLARE (XARGS :GUARD T))
   (AND (CONSP V1)
        (STRINGP (CAR V1))
        (AND (CONSP (CDR V1))
             (DIR-FILE-LISTP (CAR (CDR V1)))
             (EQUAL (CDR (CDR V1)) NIL))))
 (DEFUN DIR-FILE-LISTP (V1)
   (DECLARE (XARGS :GUARD T))
   (OR (EQUAL V1 NIL)
       (AND (CONSP V1)
            (FILE-DIRP (CAR V1))
            (DIR-FILE-LISTP (CDR V1)))))
 (DEFUN FILE-DIRP (V1)
   (DECLARE (XARGS :GUARD T))
   (OR (FILEP V1)
       (DIRP V1))))

Notice that we need to prove termination to show that this
defdata makes sense.
"

"Let's submit it.
"

(defdata 
  (dir (list string dir-file-list))
  (dir-file-list (listof file-dir))
  (file-dir (oneof file dir)))

"Can you write defdatas that don't make sense?

Sure. Here is an example that differs from the above by a few
characters.
"

:u

(defdata 
  (dir (list string dir-file-list))
  (dir-file-list (listof file-dir))
  (file-dir (oneof file file-dir)))

"Here is simpler example.
"

(defdata 
  (foo (oneof string bar))
  (bar (oneof nat foo)))


"Let's discuss libraries and books.
"

:pbt -7

"Let's look at some of the books that are included.

Let's start with base-theory.
"

"Next, let's look at std/lists/top.
"

"Notice that there are lots of libraries (books) that are used to
reason about true-lists, append, len, rev, etc. So, example, we can
see what rules are available for reasoning about true-listp, as
follows.
"

:pl append
:pl true-listp
:pl (rev (append x y))

"Especially with all of these theorems pre-loaded,
you may want to figure out why something is taking so long.
A really useful utility is accumulated-persistence."

(defdata if-expr (oneof symbol (list 'if if-expr if-expr if-expr)))

(defthm if-expr-args-b
  (implies (if-exprp (list* a b c))
           (if-exprp b))
  :rule-classes :forward-chaining)

(defthm if-expr-args-c
  (implies (if-exprp (list* a b c d))
           (if-exprp c))
  :rule-classes :forward-chaining)

(defthm if-expr-args-d
  (implies (if-exprp (list* a b c d e))
           (if-exprp d))
  :rule-classes :forward-chaining)

(defun if-flat-measure (x)
  (declare (xargs :guard (if-exprp x)
                  :verify-guards nil
                  :normalize nil))
  (mbe :logic (if (if-exprp x)
                  (if (symbolp x)
                      0
                      (+ (* 3 (if-flat-measure (second x)))
                         (max (if-flat-measure (third x))
                              (if-flat-measure (fourth x)))
                         1))
                  (acl2s-undefined 'if-flat-measure
                                   (list x)))
       :exec (if (symbolp x)
                 0
                 (+ (* 3 (if-flat-measure (second x)))
                    (max (if-flat-measure (third x))
                         (if-flat-measure (fourth x)))
                    1))))


(defthm if-flat-measure-contract
  (implies (if-exprp x)
           (natp (if-flat-measure x))))

(verify-guards if-flat-measure
               :guard-debug t
               :hints (("goal" :do-not-induct t
                        :do-not '(generalize
                                  fertilize))))


:u
(accumulated-persistence :all)
(verify-guards if-flat-measure
               :guard-debug t
               :hints (("goal" :do-not-induct t
                        :do-not '(generalize
                                  fertilize))))


(show-accumulated-persistence)

(in-theory
 (disable (:REWRITE ACL2::ALISTP-OF-CDR)
          (:REWRITE ACL2::CONSP-OF-CAR-WHEN-ALISTP)
          (:REWRITE RATIONALP-IMPLIES-ACL2-NUMBERP2)
          (:DEFINITION RTL::ARCDP)))

(accumulated-persistence nil)

(verify-guards if-flat-measure
               :guard-debug t
               :hints (("goal" :do-not-induct t
                        :do-not '(generalize
                                  fertilize))))

"Next, we'll look at designing a library, say for set 
theory.
"