STOBJ-EXAMPLE-1-PROOFS.html -- ACL2 Version 6.3

STOBJ-EXAMPLE-1-PROOFS

some proofs involving the counters stobj

Major Section:  STOBJ

Consider again the event

(defstobj counters
  (NodeCnt     :type integer :initially 0)
  (TipCnt      :type integer :initially 0)
  (IntTipsSeen :type t       :initially nil))

discussed in stobj-example-1, followed by the definition

(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (seq counters
       (update-NodeCnt 0 counters)
       (update-TipCnt 0 counters)
       (update-IntTipsSeen nil counters)))

which, because of the seq macro in stobj-example-1, is just syntactic sugar for

(defun reset-counters (counters)
  (declare (xargs :stobjs (counters)))
  (let ((counters (update-NodeCnt 0 counters)))
    (let ((counters (update-TipCnt 0 counters)))
      (update-IntTipsSeen nil counters)))).

Here is a simple theorem about reset-counters.

(defthm reset-counters-is-constant
  (implies (countersp x)
           (equal (reset-counters x)
                  '(0 0 nil))))

Before we talk about how to prove this theorem, note that the theorem is unusual in two respects.

First, it calls reset-counters on an argument other than the variable counters! That is allowed in theorems; logically speaking, the stobj functions are indistinguishable from ordinary functions. Their use is syntactically restricted only in defuns, which might be compiled and run in raw Lisp. Those restrictions allow us to implement stobj modification destructively. But logically speaking, reset-counters and other stobj ``modifying'' functions just create new objects, constructively.

Second, the theorem above explicitly provides the hypothesis that reset-counters is being applied to an object satisfying countersp. Such a hypothesis is not always required: reset-counters is total and will do something no matter what x is. But in this particular case, the result is not '(0 0 nil) unless x is, at least, a true-list of length three.

To make a long story short, to prove theorems about stobj functions you behave in exactly the way you would to prove the same theorems about the same functions defined without the stobj features.

How can we prove the above theorem? Unfolding the definition of reset-counters shows that (reset-counters x) is equal to

(update-IntTipsSeen nil
  (update-TipCnt 0
    (update-NodeCnt 0 x)))

which in turn is

(update-nth 2 nil
 (update-nth 1 0
  (update-nth 0 0 x))).

Opening up the definition of update-nth reduces this to

(list* 0 0 nil (cdddr x)).

This is clearly equal to '(0 0 nil), provided we know that (cdddr x) is nil.

Unfortunately, that last fact requires a lemma. The most specific lemma we could provide is

(defthm special-lemma-for-counters
  (implies (countersp x)
           (equal (cdddr x) nil)))

but if you try to prove that lemma you will find that it requires some reasoning about len and true-listp. Furthermore, the special lemma above is of interest only for counters.

The following lemma about len is the one we prefer.

(defthm equal-len-n
  (implies (syntaxp (quotep n))
           (equal (equal (len x) n)
                  (if (integerp n)
                      (if (< n 0)
                          nil
                        (if (equal n 0)
                            (atom x)
                          (and (consp x)
                               (equal (len (cdr x)) (- n 1)))))
                    nil))))

This lemma will simplify any equality in which a len expression is equated to any explicitly given constant n, e.g., 3, reducing the equation to a conjunction of consp terms about the first n cdrs.

If the above lemma is available then ACL2 immediately proves

(defthm reset-counters-is-constant
  (implies (countersp x)
           (equal (reset-counters x)
                  '(0 0 nil))))

The point is presumably well made: proving theorems about single-threaded object accessors and updaters is no different than proving theorems about other recursively defined functions on lists.

As we have seen, operations on stobjs turn into definitions involving nth and update-nth in the logic. Here are two lemmas that are useful for simplifying terms involving nth and update-nth, which are therefore useful in reasoning about single-threaded objects.

(defthm update-nth-update-nth-same
  (implies (equal (nfix i1) (nfix i2))
           (equal (update-nth i1 v1 (update-nth i2 v2 l))
                  (update-nth i1 v1 l))))

(defthm update-nth-update-nth-diff
  (implies (not (equal (nfix i1) (nfix i2)))
           (equal (update-nth i1 v1 (update-nth i2 v2 l))
                  (update-nth i2 v2 (update-nth i1 v1 l))))
  :rule-classes ((:rewrite :loop-stopper ((i1 i2)))))

These lemmas are due to Matt Wilding. See nu-rewriter for a discussion of the efficient simplification of terms of the form (nth n (update-nth key val lst)), which can be critical in settings involving sequential bindings that commonly arise in operations involving stobjs.

We now recommend that you see stobj-example-2.