GUARD-EXAMPLE

a brief transcript illustrating guards in ACL2 
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 (t) or go undetected (nil)? 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. 



  ACL2 !>    ; 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
Here are some examples with 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.


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
E0-ORD-< (which is known to be well-founded on the domain
recognized by E0-ORDINALP) 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))
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


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


ACL2 !>:set-guard-checking nil


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.



MUTUAL-RECURSION-PROOF-EXAMPLE

a small proof about mutually recursive functions 
Major Section:  TUTORIAL5-MISCELLANEOUS-EXAMPLES

Sometimes one wants to reason about mutually recursive functions. Although this is possible in ACL2, it can be a bit awkward. This example is intended to give some ideas about how one can go about such proofs.

For an introduction to mutual recursion in ACL2, see mutual-recursion.

We begin by defining two mutually recursive functions: one that collects the variables from a term, the other that collects the variables from a list of terms. We actually imagine the term argument to be a pseudo-termp; see pseudo-termp. 

(mutual-recursion


(defun free-vars1 (term ans)
  (cond ((atom term)
         (add-to-set-eq term ans))
        ((fquotep term) ans)
        (t (free-vars1-lst (fargs term) ans))))


(defun free-vars1-lst (lst ans)
  (cond ((atom lst) ans)
        (t (free-vars1-lst (cdr lst)
                           (free-vars1 (car lst) ans)))))


)
The idea of the following function is that it suggests a proof by induction in two cases, according to the top-level if structure of the body. In one case, (atom x) is true, and the theorem to be proved should be proved under no additional hypotheses except for (atom x). In the other case, (not (atom x)) is assumed together with three instances of the theorem to be proved, one for each recursive call in this case. So, one instance substitutes (car x) for x; one substitutes (cdr x) for x; and the third substitutes (cdr x) for x and (free-vars1 (car x) ans) for ans. If you think about how you would go about a hand proof of the theorem to follow, you'll come up with a similar scheme. 
(defun symbol-listp-free-vars1-induction (x ans)
  (if (atom x)
; then we just make sure x and ans aren't considered irrelevant
      (list x ans)
    (list (symbol-listp-free-vars1-induction (car x) ans)
          (symbol-listp-free-vars1-induction (cdr x) ans)
          (symbol-listp-free-vars1-induction
           (cdr x)
           (free-vars1 (car x) ans)))))
We now prove the two theorems together as a conjunction, because the inductive hypotheses for one are sometimes needed in the proof of the other (even when you do this proof on paper!). 
(defthm symbol-listp-free-vars1
  (and (implies (and (pseudo-termp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1 x ans)))
       (implies (and (pseudo-term-listp x)
                     (symbol-listp ans))
                (symbol-listp (free-vars1-lst x ans))))
  :hints
  (("Goal" :induct (symbol-listp-free-vars1-induction x ans))))
The above works, but let's try for a more efficient proof, which avoids cluttering the proof with irrelevant (false) inductive hypotheses. 
(ubt 'symbol-listp-free-vars1-induction)


(defun symbol-listp-free-vars1-induction (flg x ans)


; Flg is non-nil (or t) if we are ``thinking'' of a single term.


  (if (atom x)
      (list x ans)
    (if flg
        (symbol-listp-free-vars1-induction nil (cdr x) ans)
      (list (symbol-listp-free-vars1-induction t (car x) ans)
            (symbol-listp-free-vars1-induction
             nil
             (cdr x)
             (free-vars1 (car x) ans))))))
We now state the theorem as a conditional, so that it can be proved nicely using the induction scheme that we have just coded. The prover will not store an if term as a rewrite rule, but that's OK (as long as we tell it not to try), because we're going to derive the corollaries of interest later and make them into rewrite rules. 
(defthm symbol-listp-free-vars1-flg
  (if flg
      (implies (and (pseudo-termp x)
                    (symbol-listp ans))
               (symbol-listp (free-vars1 x ans)))
    (implies (and (pseudo-term-listp x)
                  (symbol-listp ans))
             (symbol-listp (free-vars1-lst x ans))))
  :hints
  (("Goal" :induct (symbol-listp-free-vars1-induction flg x ans)))
  :rule-classes nil)
And finally, we may derive the theorems we are interested in as immediate corollaries. 
(defthm symbol-listp-free-vars1
  (implies (and (pseudo-termp x)
                (symbol-listp ans))
           (symbol-listp (free-vars1 x ans)))
  :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                 (flg t)))))


(defthm symbol-listp-free-vars1-lst
  (implies (and (pseudo-term-listp x)
                (symbol-listp ans))
           (symbol-listp (free-vars1-lst x ans)))
  :hints (("Goal" :by (:instance symbol-listp-free-vars1-flg
                                 (flg nil)))))