#|

Author: Pete Manolios
Date:   9/30/2021

Code used in lecture 11 of Computer-Aided Reasoning.  

|#

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

#|

Topics:

  Macros 
  Books
  State/World
  Performance issues: accumulated persistence
  Libraries

|#

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

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

"Let's see how app is defined.
"

:pe app

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

(property (x :tl y :tl)
  :hyps (or (null x) (null y))
  :body (== (bin-app x y)
            (bin-app y x)))

"
Notice that the output also says app here.
"

(property (x :tl y :tl)
  :hyps (or (null x) (null y))
  :body (== (append x y x)
            (append y x x)))

"
You have to be somewhat careful because app is a macro that
expands into bin-app.
"

:pe app

:trans1 (app x y)

"
And, bin-app is a non-recursive definition, so 
the theorem prover will use rewriting to expand it
into its body.

   (app x y)
-> { macro expansion }
   (bin-app x y)
-> { rewriting }
   (append x y)
-> { macro expansion }
   (binary-append x y)
"

:trans1 (append x y)

"
The way I defined app is good, for several reasons:

1. It allows me to use the previous definition of 
   append, but with different contracts.

So, I really want app and append to be different. 

"

(property (x :tl y :all)
  (== (append x y)
      (append x y)))

(property (x :tl y :all)
  (== (app x y)
      (app x y)))

"
2. I can use all the previous theorems for append, for free.
   How? By just expanding app into append.

But, there is a price.

I have to be aware that the rewriter will do what I told
it and my rewrite strategy is to turn app into append.

So, if I write rewrite rules where the pattern is 

(app ...)

That's a bad idea and I should instead use the pattern

(append ...)

So, if you prove a theorem of the form
(=> ... (== (app x y) ...))

this will probably never match.

Instead, you should prove
(=> ... (== (append x y) ...))

Using macros in rewrite rules is fine, as they get expanded
away, i.e., the above is equivalent to

(=> ... (== (binary-append x y) ...))
"



"
Let's define our own append as follows.
"

(definec binary-ap (x :tl y :tl) :tl
  (match x
    (() y)
    ((a . as) (cons a (binary-ap as y)))))

"
It would be nice to have a macro, say ap, that can take
an arbitrary number of arguments.

This is syntactic sugar that is easy to add with lisp-based
languages, but hard to do in most languages. 

There is a utility ACL2s provides for doing this.
"

:doc make-n-ary-macro

:trans1 (make-n-ary-macro ap binary-ap nil t)

(make-n-ary-macro ap binary-ap nil t)

"
So, make-n-ary-macro defines the macro ap and adds it to the
macro-aliases-table. Let's look at the documentation.
"

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

"
REMINDER:
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 ap, not binary-ap "

(property ap-lemma (x :tl)
  (== (ap x nil) x)
  :hints (("goal" :induct (tlp x))))

(property (x :tl y :tl)
  :hyps (or (null x) (null y))
  :body (== (ap x y)
            (ap y x)))

"
In ACL2s, tlp is a macro alias for true-listp and so on."


"
Notice that such macros are also supported in the proof builder.
The proof builder is a low-level theorem prover where you can
complete control what ACL2 does. It can be useful for understanding
what is going on in a failed proof.

You have to write conjecture in expanded form as shown below.
"

(verify
 (=> (and (tlp x) (tlp y) (or (null x) (null y)))
     (equal (ap x y)
            (ap y x))))
th
(help th)
pro
(help pro)
(help split)
th
split
th
bash
th
pp
(help pp)
p
(help p)
(help exit)
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 (ap x y)
                 (ap y x)))
 :instructions (prove))

(help 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 (ap x y)
                 (ap y x)))
 :instructions ((do-all induct bash)))

(help induct)
(help bash)
goals
th
pro
th
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 (ap x y)
                 (ap y x)))
 :instructions ((do-all induct (repeat bash))))

(help repeat)
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 (ap x y)
                 (ap 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 (ap x y)
                 (ap 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 (ap x y)
                 (ap 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 (ap x y)
                 (ap y x)))
 :instructions ((repeat-until-done induct (repeat bash))
                (exit my-thm nil)))

y

(definec rv (x :tl) :tl
  (match x
    (() ())
    ((a . as) (ap (rv as) `(,a)))))

(definec rvt (x :tl acc :tl) :tl
  (match x
    (() acc)
    ((a . as) (rvt as (cons a acc)))))

(definec rv* (x :tl) :tl
  (rvt x nil))

(property david-lemma (x :tl y :tl z :tl)
  (equal (ap (ap x y) z)
         (ap x (ap y z))))

(property rvt-thm (x :tl acc :tl)
  (== (rvt x acc)
      (ap (rv x) acc)))

"
We stopped here.
Add enough lemmas to prove the following property.
Use the method.
"

(property rv-prop (x :tl y :tl z :tl)
  (== (rv* (ap x y (rv* z)))
      (ap z (rv* y) (rv* x))))

(defdata set tl)

(definec s<= (x :set y :set) :bool
  (match x
    (() t)
    ((e . xs) (and (in e y) (s<= xs y)))))

(definec s= (x :set y :set) :bool
  (^ (s<= x y) (s<= y x)))

"
Add enough lemmas to prove the following property.
Use the method.
"

(property (x :set)
  (s= (rv* x) x))