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
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
This is clearly equal to
Unfortunately, that last fact requires a lemma. The most specific lemma we could provide is
but if you try to prove that lemma you will find that it requires some
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
If the above lemma is available then ACL2 immediately proves
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
(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.