Stating and proving theorems about
In this topic we give some advice about how to state and prove
theorems involving
Just because you can write iterative computations inline, don't get carried away!
If you can think of a good name for the concept implemented by a
For example, rather than write instances of
(loop$ for a in x as b in y sum (* a b))
it is better to define
Basically, names are good as long as you can remember them. They give you
a place to hang lemmas and the lemmas match without you having to think about
how lambda objects rewrite, local variables, etc. Not all
Let's start with the most common issue raised by any inductive proof: the conjecture to be proved must be general enough to permit the provision of an appropriate inductive hypothesis.
Consider how you would prove the conjecture below after defining
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x))))) (defun rev1 (x a) (if (endp x) a (rev1 (cdr x) (cons (car x) a)))) (defthm rev1-is-rev (equal (rev1 x nil) (rev x)))
The experienced ACL2 user would not attempt to prove
(defthm rev1-is-rev-generalized (equal (rev1 x a) (append (rev x) a)))
The proof of the generalized theorem succeeds (though the prover must
“discover” and then prove that
With that theorem available, the proof of
Now consider defining reverse with a
(defun rev-loop$ (x) (loop$ with tail = x with a = nil do (if (endp tail) (return a) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail))))))
The experienced ACL2 user would not attept to prove that
(defthm rev-loop$-is-rev-generalized (equal (loop$ with tail = x with a = a do (if (endp tail) (return a) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail))))) (append (rev x) a))).
ACL2's prover can derive induction schemes suggested by some
ACL2 will prove the lemma above, if the associativity of
Lesson 1: If a
The lemma above,
(defthm rev-loop$-is-rev (equal (rev-loop$ x) (rev x))).
But as stated,
Recall that the prover always expands enabled functions that are not
explicitly recursive. And
Goal' (equal (loop$ with tail = x with a = nil do (if (endp tail) (return a) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail))))) (rev x))
If the
Goal'' (equal (append (rev x) nil) (rev x))
and the proof would be completed as before with the right-identity rule.
Indeed, this is what happens in this particular case, but the reason it
works is completely unrelated to
Let's suppose the generalized lemma did have some hypotheses or otherwise
failed to apply during preprocessing. You can cause this to happen by
restating the generalized lemma and the main theorem to have the (unnecessary
but easily dealt with) hypothesis
The reason it never fires is that it is not tried during prepreprocessing
(because preprocessing doesn't deal with conditional rules because
preprocessing doesn't support backchaining) and
This transforms
(loop$ with tail = x with a = nil do (if (endp tail) (return a) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail)))))
to
(loop$ with tail = x with a = nil do (if (consp tail) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail))) (return a)))
because
After this rewrite, our generalized lemma no longer matches.
Lesson 2: Do not prove rewrite rules that target
So for example, in addition to watching out for non-recursive functions in
the body, be alert for things like expressions that are rearranged by
associativity and commutativity rules. You wouldn't write a rewrite rule
containing a subterm like
The entire robust script for the
(defun rev (x) (if (endp x) nil (append (rev (cdr x)) (list (car x))))) (defun rev-loop$ (x) (loop$ with tail = x with a = nil do (if (endp tail) (return a) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail)))))) (defthm assoc-of-append (equal (append (append a b) c) (append a (append b c)))) (defthm rev-loop$-is-rev-generalized (equal (loop$ with tail = x with a = a do (if (consp tail) (progn (setq a (cons (car tail) a)) (setq tail (cdr tail))) (return a))) (append (rev x) a))) (defthm rev-loop$-is-rev (equal (rev-loop$ x) (rev x)))
The script is robust in the sense that even if you conditionalize the
generalized lemma with a hypothesis that can be relieved in the main theorem
the lemma will fire and rewrite the
Another issue that comes up when posing lemmas about
Define the following function.
(defun secret-setq-problem (k x) (loop$ with x = x with j = 0 do (cond ((endp x) (return 'bad)) ((equal j k) (return 'good)) (t (progn (setq x (cdr x)) (setq j (+ 1 j)))))))
The function counts
(defthm secret-setq-problem-main (implies (and (natp k) (< k (len x))) (equal (secret-setq-problem k x) 'good)))
While
(defthm secret-setq-problem-lemma (implies (and (natp j) (natp k) (< k (+ j (len x))) (<= j k)) (equal (loop$ with x = x with j = j do (if (consp x) (if (equal j k) (return 'good) (progn (setq x (cdr x)) (setq j (+ 1 j)))) (return 'bad))) 'good)))
Following Lesson 1, we generalized the initial value of
Following Lesson 2, we normalized the body. We replaced the
The lemma is proved automatically by ACL2, using the induction suggested
by the
However, the attempt to prove the main theorem above will fail! The lemma
doesn't fire because the
Sometimes to debug a failed proof it helps to compare the term that a
lemma targets with its intended target in the checkpoint of the failed proof.
This is especially true for
ACL2 !>:pr secret-setq-problem-lemma Rune: (:REWRITE SECRET-SETQ-PROBLEM-LEMMA) Enabled: T Hyps: (AND (NATP J) (NATP K) (< K (+ J (LEN X))) (<= J K)) Equiv: EQUAL Lhs: (DO$ (LAMBDA$ (ALIST) (ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'X ALIST)))) (LIST (CONS 'X X) (CONS 'J J) (CONS 'K K)) (LAMBDA$ (ALIST) (IF (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST))) (IF (EQUAL (CDR (ASSOC-EQ-SAFE 'J ALIST)) (CDR (ASSOC-EQ-SAFE 'K ALIST))) (LIST :RETURN 'GOOD (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))) (LIST NIL NIL (LIST (CONS 'X (CDDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (+ 1 (CDR (ASSOC-EQ-SAFE 'J ALIST)))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))) (LIST :RETURN 'BAD (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))) (LAMBDA$ (ALIST) (LIST NIL NIL (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))) (NIL) NIL) Rhs: 'GOOD Backchain-limit-lst: NIL Subclass: BACKCHAIN Loop-stopper: NIL
The actual
(DO$ (LAMBDA$ (ALIST) (ACL2-COUNT (CDR (ASSOC-EQ-SAFE 'X ALIST)))) (LIST (CONS 'X X) '(J . 0) (CONS 'K K)) (LAMBDA$ (ALIST) (IF (CONSP (CDR (ASSOC-EQ-SAFE 'X ALIST))) (IF (EQUAL (CDR (ASSOC-EQ-SAFE 'J ALIST)) (CDR (ASSOC-EQ-SAFE 'K ALIST))) (LIST :RETURN 'GOOD (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'J ALIST))))) (LIST NIL NIL (LIST (CONS 'X (CDDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (+ 1 (CDR (ASSOC-EQ-SAFE 'J ALIST)))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))) (LIST :RETURN 'BAD (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST))))))) (LAMBDA$ (ALIST) (LIST NIL NIL (LIST (CONS 'X (CDR (ASSOC-EQ-SAFE 'X ALIST))) (CONS 'J (CDR (ASSOC-EQ-SAFE 'J ALIST))) (CONS 'K (CDR (ASSOC-EQ-SAFE 'K ALIST)))))) (NIL) NIL)
Note that the
We could possibly fix this problem by changing how ACL2 stores lemmas or how the pattern matcher works. But such changes could have far reaching consequences across the entire ACL2 regression suite, so we have made no such changes.
Absent such changes, it's incumbent on the user to phrase the rewrite
rule appropriately. The question is, “How can you make that particular
One way would be to rephrase the rewrite rule by using the
Another way to accomplish the same effect is to rewrite the
(defthm secret-setq-problem-lemma (implies (and (natp j) (natp k) (< k (+ j (len x))) (<= j k)) (equal (loop$ with x = x with j = j with k = k ; ``new'' var do (if (consp x) (if (equal j k) (progn (setq k j) ; new setq! (return 'good)) (progn (setq x (cdr x)) (setq j (+ 1 j)))) (return 'bad))) 'good)))
You can use
Note that the inclusion of the new “
Because this matching problem can repaired by adding an unnecessary
Lesson 3: If the left-hand side of a rewrite rule contains an
Another issue you may occasionally confront when dealing with inductions
suggested by
From every
Those tests are not always sufficient to guarantee termination! If the
However, it is logically valid to condition the induction-time measure conjectures on hypotheses from the conjecture being proved — and it is often ineffective to include all of those hypotheses. So ACL2's induction mechanism chooses some of the available hypotheses and may not choose enough. This is the “hidden hypothesis problem.” An example is below.
The following function can be admitted and guard verified, meaning the termination obligation is proved as part of guard verification.
(defun hidden-hyp-problem (lo j) (declare (xargs :guard (and (natp lo) (natp j) (<= lo j)))) (loop$ with j = j do :guard (and (natp lo) (natp j) (<= lo j)) (if (equal lo j) (return 'good) (setq j (- j 1)))))
Since since
The derived recursive function corresponding to this
(defun derived-fn (lo j) (if (equal lo j) 'good (derived-fn lo (- j 1)))).
That derived function doesn't terminate.
Now let's try to prove that the
However, the following proof attempt fails. The prover chooses to induct
as suggested by the
ACL2 !>(defthm hidden-hyp-problem-main (implies (and (natp lo) (natp j) (<= lo j)) (equal (loop$ with j = j do :guard (and (natp lo) (natp j) (<= lo j)) (if (equal lo j) (return 'good) (setq j (- j 1)))) 'good))) ... This suggestion was produced using the :induction rule DO$. If we let (:P J LO) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (EQUAL LO J)) (:P (+ -1 J) LO) (INTEGERP J) (<= 0 J)) (:P J LO)) (IMPLIES (AND (NOT (EQUAL LO J)) (< (+ -1 J) 0) (INTEGERP J) (<= 0 J)) (:P J LO)) (IMPLIES (AND (NOT (EQUAL LO J)) (NOT (INTEGERP (+ -1 J))) (INTEGERP J) (<= 0 J)) (:P J LO)) (IMPLIES (AND (EQUAL LO J) (INTEGERP J) (<= 0 J)) (:P J LO)) (IMPLIES (AND (INTEGERP J) (<= 0 J) (NOT (EQUAL LO J))) (L< (LEX-FIX (ACL2-COUNT (+ -1 J))) (LEX-FIX (ACL2-COUNT J))))). Note that one or more measure conjectures included in the scheme above justify this induction if they are provable. When applied to the goal at hand the above induction scheme produces six nontautological subgoals. ...
The first four proof obligations, which are all proved by the prover,
implicitly include the hypotheses that
If the prover had just generated the measure conjecture from the
(IMPLIES (NOT (EQUAL LO J)) (L< (LEX-FIX (ACL2-COUNT (+ -1 J))) (LEX-FIX (ACL2-COUNT J)))).
But we see that the prover actually augmented the hypothesis from the body
with two literals it assumed were relevant from the conjecture being proved,
namely
You can fix this by providing an
(defthm hidden-hyp-problem-main (implies (and (natp lo) (natp j) (<= lo j)) (equal (loop$ with j = j do (if (equal lo j) (return 'good) (setq j (- j 1)))) 'good)) :hints (("Goal" :induct (loop$ with j = j do (IF (AND (NATP LO) (<= LO J)) (if (equal lo j) (return 'good) (setq j (- j 1))) (RETURN 'IRRELEVANT-BASE-CASE))))))
Lesson 4: You can use
Note that the derived function from the
Another lesson suggested by the example above is that you don't always
have to define a recursive function to suggest certain inductions. Here is
an example. Recall the function
(defun mark-all (x) (if (consp x) (cons (list 'mark (car x)) (mark-all (cdr x))) nil)) (defun all-markedp (x) (if (consp x) (and (consp (car x)) (eq (car (car x)) 'mark) (all-markedp (cdr x))) t)).
Now prove
(thm (implies (all-markedp a) (all-markedp (rev1 (mark-all x) a))))
No induction suggested by the functions in this theorem is appropriate.
The appropriate induction assumes the theorem for
(thm (implies (all-markedp a) (all-markedp (rev1 (mark-all x) a))) :hints (("Goal" :induct (loop$ with x = x with a = a do (if (consp x) (progn (setq a (cons (list 'mark (car x)) a)) (setq x (cdr x))) (return 'base-case)))))).
See lp-section-11 of the