Some proofs involving the

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

(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

(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

Second, the theorem above explicitly provides the hypothesis that

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

(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

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

This is clearly equal to

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

The following lemma about

(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 *n*, e.g., *n*

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, both due to Matt Wilding, that are useful for simplifying terms
involving

(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)))))

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