DEFSTRUCTURE
------------

ACL2 has a form called defstructure that behaves similiarly to DrScheme's define-struct.  To use it, you must include the following line at the top of your program:

(include-book "data-structures/structures" :dir :system)

`defstructure' generates functions just like `define-struct' but the names are a bit different.  Consider this nonsensical example:

  (defstructure moo foo bar)

This defines a structure called moo that has two fields:  foo and bar.  Several functions are defined automatically:

- moo (the constructor)
- moo-foo, moo-bar (selectors)
- moo-p (predicate)
- weak-moo-p (another predicate)

We will not use the weak predicates directly ourselves, but you should know it exists in case ACL2 has something to say about it during a proof.

Notice that the predicate end in `-p' instead of '?', and the constructor does not have a `make-' prefixed to the name.

The (defstructure moo foo bar) is essentially equivalent to the following sequence of definitions:

;; construct a moo
(defun moo (a-foo a-bar) (list 'moo a-foo a-bar))
;; select the foo field
(defun moo-foo (x) (cadr x))
;; select the bar field
(defun moo-bar (x) (caddr x))
;; check the shape of the list
(defun weak-moo-p (x)
  (and (true-listp x)
       (= (len x) 3)
       (equal (car x) 'moo)))
;; redundant for us.
(defun moo-p (x) (weak-moo-p x))

Notice the important difference between DrScheme's structures and ACL2's structures:  in ACL2, the representation as a list is exposed to the programmer.  For example,

  (car (make-foo 17 42)) = 'moo
  (cadr (make-foo 17 42)) = 17
  (caddr (make-foo 17 42)) = 42
  (true-listp (make-foo 17 42)) = t
  ...

Ordinarily you should never use this knowledge, and in fact defstructure generates additional code that causes this knowledge to be hidden from the theorem prover.  For example, the theorem prover cannot prove this theorem:

  (defthm obvious-but-fails
    (equal (len (moo X Y)) 3))

even though you can evaluate (len (moo 17 42)) and see that the result is 3 (try the proof and see what it says).  Even though you should never use the representation of a structure directly, you might need to recognize when the lack of knowledge is confusing ACL2.  We will see such a case later on.

Here is how we would use defstructure to define a datatype of binary trees of numbers:

(defstructure leaf)
(defstructure branch number left right)

;; BT ::= (leaf) | (branch Number BT BT)

Incidentally, we can always express the data definition as a predicate that recognizes elements of our data type:
;; bt? : Any -> Boolean
(defun bt? (x)
  (cond ((leaf-p x) t)
	((branch-p x) 
	 (and (acl2-number-p (branch-number x))
	      (bt? (branch-left x))
	      (bt? (branch-right x))))))
(Remember, in ACL2 when none of the cond-questions match, the answer is automatically nil instead of an error!)

This is often necessary because we are usually interested in theorems that hold only when the functions are used according to their contract:

;; mirror : BT -> BT
;; flip a BT about the root 
(defun mirror (x) 
  (cond ((leaf-p x) (leaf))
	((branch-p x) (branch (branch-value x)
			      (mirror (branch-right x))
			      (mirror (branch-left x))))))

Compare:

  (defthm bogus-theorem
    (equal (mirror (mirror x)) x))

  (defthm proper-theorem
    (implies (bt? x)
	     (equal (mirror (mirror x)) x)))

So get in the habit of expressing your data definitions as predicates that recognize the well-formed data.

There is another strange problem that the theorem prover runs into.  Suppose a proof fails and you see the following goal at a checkpoint:

(implies (and ...
	      (leaf-p (branch A B C))
	      ...)
	 ...)

That goal should immediately be validated because the implication contains a false hypothesis!  Clearly, leaves and branches are distinct and so (leaf-p (branch A B C)) = nil.  But recall that the representation of structures is hidden from ACL2 by default, and so it cannot tell that branch never produces a leaf.

Of course, the real solution here is to define datatypes in a way that tells ACL2 this fact automatically (instead of using defstructure).  But until we get around to implementing that, work around the problem manually by proving this theorem:

(defthm leaf-p-of-branch-is-nil
  (equal (leaf-p (branch X Y Z)) nil)
  :hints (("Goal" :in-theory (enable leaf-p weak-leaf-p branch))))

The theorem simply states the obvious, but what does the :hints line say?  That line just gives ACL2 temporary permission to look inside the structure representation.  In particular, it is allowed to know the definitions of leaf-p, weak-leaf-p, and branch.  That's enough to prove the theorem (try it on paper to see why, it's easy).  ACL2's permission to peek inside is revoked as soon as the theorem has been proved.

Except for corner cases like this, your theorems should never use hints!  More often than not, allowing ACL2 to see the representation of structures causes it to become severely confused.