Tips and tricks for ACL2 - acl2/acl2 GitHub Wiki

#DRAFT

#Introduction

Random "gotchas" that Rager has discovered while using ACL2 at an intermediate level. These could be folded into the ACL2 documentation topics TIPS or TIDBITS at some point, but I'm just writing them here for now.

#Tips

  • When you have the desire to trace ACL2's rewriter and look through the output, you probably really want to use :brr and brr commands (see doc topic "brr-commands") like :path. Also, consider using the brr@ macro (which is documented under topic 'brr@'). Also consider Jared's "why" macro (found in books/centaur/jared-customization.lsp) to help you see what rules are being tried. Not including the ":go" portion of that macro will cause :brr to break whenever the provided rule is tried.

  • To set the width of the text before carriage returns occur, use something like the following:

(set-fmt-soft-right-margin 190 state) (set-fmt-hard-right-margin 205 state)

  • When making theory changes in books that you expect to prevent your later books from completing, the following can be helpful.

  • Make a copy of all .cert.out files for reference

  • When a theorem fails in the later book, examine the appropriate .cert.out file to see why it passed under the original theory.

  • Here's a command to substitute the "$@" that appears in saved_acl2 with a flag that lowers the initial requested heap size in CCL:

    perl -i -pe 's/"\$@"/--heap-reserve 158G "\$@"/' saved_acl2

  • Here's some discussion of induction in ACL2

https://utlists.utexas.edu/sympa/arc/acl2-help/2014-01/msg00033.html

  • When making rewrite rules, worry about canonicalizing the lhs more than canonicalizing the rhs. The rhs will be rewritten anyway, but the lhs has to match the checkpoint ACL2 (and the current set of rules) generates.

  • Force the hypotheses of :type-prescription rules. This is because just using type-prescription reasoning to relieve hyps is often too weak. But the power of whole proof process is used during forcing. And in fact, sometimes the forcing round won't actually occur, because a little bit of rewriting occurs (which can rewrite to T) before the clause is saved for forcing.

  • When there are lots of case-splits because we're dealing with an or of an and, the prover may go out to lunch because of the case-splits. If possible, consider "controlling" the case-split, by converting the or to a cond in a lemma. And then one can :use the lemma in the minimal-theory to prove the original conjecture. E.g., convert the former to the latter, where the latter ends up being the "lemma".

             (or (and (equal out1 in)
                      (equal out2 in2)
                      (equal out3 in3)
                      (equal out4 in4))
                 (and (equal out2 in)
                      (equal out3 in2)
                      (equal out4 in3)
                      (equal out5 in4))
                 (and (equal out3 in)
                      (equal out4 in2)
                      (equal out5 in3)
                      (equal out6 in4))
                 (and (equal out4 in)
                      (equal out5 in2)
                      (equal out6 in3)
                      (equal out7 in4)))))

to

             (cond (;(atom fifo)
                    (equal (len fifo) 0)
                    (and (equal out1 in)
                         (equal out2 in2)
                         (equal out3 in3)
                         (equal out4 in4)))
                   (;(atom (cdr fifo))
                    (equal (len fifo) 1)
                    (and (equal out2 in)
                         (equal out3 in2)
                         (equal out4 in3)
                         (equal out5 in4)))
                   (;(atom (cddr fifo))
                    (equal (len fifo) 2)
                    (and (equal out3 in)
                         (equal out4 in2)
                         (equal out5 in3)
                         (equal out6 in4)))
                   (t ; (atom (cdddr fifo))
                    (and (equal out4 in)
                         (equal out5 in2)
                         (equal out6 in3)
                         (equal out7 in4))))))
  • Avoid :forward-chaining rules, except that "type-like" :forward-chaining rules are probably okay. For example, the following could be an okay :forward-chaining rule:
(defrule unsigned-5-p-implies-natp
  (implies (unsigned-5-p x)
           (natp x))
  :rule-classes :forward-chaining)

#Gotchas

  • :use hints only add the instance of the theorem being used to the hypotheses of the subgoal you're trying to prove. They do not tell the prover to actually use to substitute the LHS of the instantiation for the RHS (provided its an equals relation). The hypothesis will only help rewrite the conclusion of the subgoal if the RHS of the instantiated theorem (what becomes the additional hypothesis) is "less complex" (determined via some implementation-specific heuristics) than the LHS.

A potential work-around is to write a rewrite-rule that is basically the instantiation of the lemma you want, but due to the theorem prover only using rewrite-rules in a relatively strict manner (compared to if the instantiation was part of the hypotheses, where it can be used in the context of the conclusion, etc.).

  • When writing rewrite rules that use arithmetic (e.g., using +), you probably want your arguments to arithmetic "functions" (like +) to match the term order of the checkpoints that you're seeing. It's unlikely that you will see a checkpoint like the following (where a, b, and c represent terms themselves where the correct "term order" (see :DOC topic term order) indicates that a < b < c):

(equal (+ c b a) ...)

Presuming associativity-of-+ and commutativity-of-+ are enabled (which they typically are), it's more likely you will see this checkpoint:

(equal (+ a b c) ...)

This is because ACL2 (even with most any arithmetic libraries) tends to canonicalize the order of arguments to arithmetic "functions" (like +). So, unless you disable associativity-of-+ and commutativity-of-+, any checkpoint you're likely to see will probably present the arithmetic term that ACL2 is "stuck on" in term order. Thus, you should write your rewrite rules with the term order of the arithmetic expressions that you're likely to see in checkpoints in mind.

Here is some further paraphrased discussion from Davis on the matter:

It doesn't really make sense to worry about term-order when writing the LHS of a rule. The term-order matters in the subgoal and you have to have general enough rules to match whatever order you happen to encounter. There isn't a "correct" way to write your rewrite rule that will solve the general problem. It's the term order of the terms you're matching that matters, and you generally (there are a couple exceptions) don't have any control over that when you're writing the rule.

Rager follow-up:

Suppose you have a rule for the addition of calls of bar and foo. Assuming that the bar call is < the foo call, the rule should be written with the lhs as (+ (bar x y) (foo w z)), not (+ (foo w z) (bar x y)).