Major Section: TUTORIAL5-MISCELLANEOUS-EXAMPLES
This note addresses the question: what is the use of guards in ACL2? Although we recommend that beginners try to avoid guards for a while, we hope that the summary here is reasonably self-contained and will provide a reasonable introduction to guards in ACL2. For a more systematic discussion, see guard. For a summary of that topic, see guard-quick-reference.
Before we get into the issue of guards, let us note that there are two important ``modes'':
defun-mode -- ``Does this defun add an axiom (`:logic mode') or not
(`:program mode')?'' (See defun-mode.) Only :logic mode
functions can have their ``guards verified'' via mechanized proof;
see verify-guards.
set-guard-checking -- ``Should runtime guard violations signal an
error (:all, and usually with t or :nowarn) or go undetected
(nil, :none)? Equivalently, are expressions evaluated in Common Lisp
or in the logic?'' (See set-guard-checking.)
Prompt examples
Here some examples of the relation between the ACL2 prompt and the
``modes'' discussed above. Also see default-print-prompt. The
first examples all have ld-skip-proofsp nil; that is, proofs are
not skipped.
Here are some examples withACL2 !> ; logic mode with guard checking on ACL2 > ; logic mode with guard checking off ACL2 p!> ; program mode with guard checking on ACL2 p> ; program mode with guard checking off
default-defun-mode of :logic.
ACL2 > ; guard checking off, ld-skip-proofsp nil ACL2 s> ; guard checking off, ld-skip-proofsp t ACL2 !> ; guard checking on, ld-skip-proofsp nil ACL2 !s> ; guard checking on, ld-skip-proofsp t
Sample session
ACL2 !>(+ 'abc 3)ACL2 Error in TOP-LEVEL: The guard for the function symbol BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (+ 'ABC 3).
ACL2 !>:set-guard-checking nil ;;;; verbose output omitted here ACL2 >(+ 'abc 3) 3 ACL2 >(< 'abc 3) T ACL2 >(< 3 'abc) NIL ACL2 >(< -3 'abc) T ACL2 >:set-guard-checking t
Turning guard checking on, value T.
ACL2 !>(defun sum-list (x) (declare (xargs :guard (integer-listp x) :verify-guards nil)) (cond ((endp x) 0) (t (+ (car x) (sum-list (cdr x))))))
The admission of SUM-LIST is trivial, using the relation O< (which is known to be well-founded on the domain recognized by O-P) and the measure (ACL2-COUNT X). We observe that the type of SUM-LIST is described by the theorem (ACL2-NUMBERP (SUM-LIST X)). We used primitive type reasoning.
Summary Form: ( DEFUN SUM-LIST ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, proof tree: 0.00, other: 0.03) SUM-LIST ACL2 !>(sum-list '(1 2 3))
ACL2 Warning [Guards] in TOP-LEVEL: Guard-checking will be inhibited on recursive calls of the executable counterpart (i.e., in the ACL2 logic) of SUM-LIST. To check guards on all recursive calls: (set-guard-checking :all) To leave behavior unchanged except for inhibiting this message: (set-guard-checking :nowarn)
6 ACL2 !>(sum-list '(1 2 abc 3))
ACL2 Error in TOP-LEVEL: The guard for the function symbol BINARY-+, which is (AND (ACL2-NUMBERP X) (ACL2-NUMBERP Y)), is violated by the arguments in the call (+ 'ABC 3).
ACL2 !>:set-guard-checking nil ;;;; verbose output omitted here ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >(defthm sum-list-append (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))))
<< Starting proof tree logging >>
Name the formula above *1.
Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate.
...
That completes the proof of *1.
Q.E.D.
Guard verification vs. defun
Declare Form Guards Verified?
(declare (xargs :mode :program ...)) no (declare (xargs :guard g)) yes (declare (xargs :guard g :verify-guards nil)) no (declare (xargs ...<no :guard>...)) no
ACL2 >:pe sum-list l 8 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) (COND ((ENDP X) 0) (T (+ (CAR X) (SUM-LIST (CDR X)))))) ACL2 >(verify-guards sum-list) The non-trivial part of the guard conjecture for SUM-LIST, given the :type-prescription rule SUM-LIST, is
Goal (AND (IMPLIES (AND (INTEGER-LISTP X) (NOT (CONSP X))) (EQUAL X NIL)) (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X))) (INTEGER-LISTP (CDR X))) (IMPLIES (AND (INTEGER-LISTP X) (NOT (ENDP X))) (ACL2-NUMBERP (CAR X)))).
...
ACL2 >:pe sum-list lv 8 (DEFUN SUM-LIST (X) (DECLARE (XARGS :GUARD (INTEGER-LISTP X) :VERIFY-GUARDS NIL)) ACL2 >:set-guard-checking t Turning guard checking on, value T. ACL2 !>(sum-list '(1 2 abc 3))
ACL2 Error in TOP-LEVEL: The guard for the function symbol SUM-LIST, which is (INTEGER-LISTP X), is violated by the arguments in the call (SUM-LIST '(1 2 ABC ...)). See :DOC wet for how you might be able to get an error backtrace.
ACL2 !>:set-guard-checking nil ;;;; verbose output omitted here ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >:comp sum-list Compiling gazonk0.lsp. End of Pass 1. End of Pass 2. Finished compiling gazonk0.lsp. Loading gazonk0.o start address -T 1bbf0b4 Finished loading gazonk0.o Compiling gazonk0.lsp. End of Pass 1. End of Pass 2. Finished compiling gazonk0.lsp. Loading gazonk0.o start address -T 1bc4408 Finished loading gazonk0.o SUM-LIST ACL2 >:q
Exiting the ACL2 read-eval-print loop. ACL2>(trace sum-list) (SUM-LIST)
ACL2>(lp)
ACL2 Version 1.8. Level 1. Cbd "/slocal/src/acl2/v1-9/". Type :help for help. ACL2 >(sum-list '(1 2 abc 3)) 6 ACL2 >(sum-list '(1 2 3)) 1> (SUM-LIST (1 2 3))> 2> (SUM-LIST (2 3))> 3> (SUM-LIST (3))> 4> (SUM-LIST NIL)> <4 (SUM-LIST 0)> <3 (SUM-LIST 3)> <2 (SUM-LIST 5)> <1 (SUM-LIST 6)> 6 ACL2 >:pe sum-list-append 9 (DEFTHM SUM-LIST-APPEND (EQUAL (SUM-LIST (APPEND A B)) (+ (SUM-LIST A) (SUM-LIST B)))) ACL2 >(verify-guards sum-list-append)
The non-trivial part of the guard conjecture for SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST, is
Goal (AND (TRUE-LISTP A) (INTEGER-LISTP (APPEND A B)) (INTEGER-LISTP A) (INTEGER-LISTP B)).
...
****** FAILED ******* See :DOC failure ****** FAILED ****** ACL2 >(defthm common-lisp-sum-list-append (if (and (integer-listp a) (integer-listp b)) (equal (sum-list (append a b)) (+ (sum-list a) (sum-list b))) t) :rule-classes nil)
<< Starting proof tree logging >>
By the simple :rewrite rule SUM-LIST-APPEND we reduce the conjecture to
Goal' (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (EQUAL (+ (SUM-LIST A) (SUM-LIST B)) (+ (SUM-LIST A) (SUM-LIST B)))).
But we reduce the conjecture to T, by primitive type reasoning.
Q.E.D. ;;;; summary omitted here ACL2 >(verify-guards common-lisp-sum-list-append)
The non-trivial part of the guard conjecture for COMMON-LISP-SUM-LIST-APPEND, given the :type-prescription rule SUM-LIST, is
Goal (AND (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (TRUE-LISTP A)) (IMPLIES (AND (INTEGER-LISTP A) (INTEGER-LISTP B)) (INTEGER-LISTP (APPEND A B)))).
...
Q.E.D.
That completes the proof of the guard theorem for COMMON-LISP-SUM-LIST-APPEND. COMMON-LISP-SUM-LIST-APPEND is compliant with Common Lisp. ;;;; Summary omitted here. ACL2 >(defthm foo (consp (mv x y)))
...
Q.E.D.
ACL2 >(verify-guards foo)ACL2 Error in (VERIFY-GUARDS FOO): The number of values we need to return is 1 but the number of values returned by the call (MV X Y) is 2.
> (CONSP (MV X Y))
ACL2 Error in (VERIFY-GUARDS FOO): The guards for FOO cannot be verified because the theorem has the wrong syntactic form. See :DOC verify-guards.
