		Search-engine friendly clone of the ACL2 documentation.

Reference

Def-gl-thm

Prove a theorem using GL symbolic simulation.

Usage:

(def-gl-thm <theorem-name>
  :hyp <hypothesis term>
  :concl <conclusion term>
  :g-bindings <shape spec binding alist>

  :rule-classes <rule classes expression>

  :hyp-clk <number> :concl-clk <number>
  :clause-proc <clause processor name>

  :n-counterexamples <number>
  :abort-indeterminate <t or nil>

  ;; Hints for coverage goals:
  :cov-theory-add <theory expression>
  :do-not-expand <list of functions>
  :cov-hints <computed hints>
  :cov-hints-position <:replace, :before, or :after>

  :test-side-goals <t or nil>)

This form submits a defthm event for the theorem

(implies <hyp> <concl>)

and the specified rule-classes, and gives a hint to attempt to prove it by symbolic execution using a GL clause processor.

Out of the list of keyword arguments recognized by this macro, three are necessary: :hyp, :concl, and :g-bindings. As noted, the theorem to be proved takes the form (implies <hyp> <concl>). The hyp is also used in proving coverage, explained below.

The :g-bindings must be a term evaluating to an alist formatted as follows:

((<var-name1>  <shape-spec1>)
 (<var-name2>  <shape-spec2>)
 ...)

The shape specs must be well-formed as described in shape-specs; notably, they must not reuse BDD variable numbers or unconstrained variable names. Note also that this is not a dotted alist; the shape spec is the cadr, not the cdr, of each entry. If any variables mentioned in the theorem are not bound in this alist, they will be given an unconstrained variable binding.

The symbolic objects used as the inputs to the symbolic simulation are obtained by translating each shape spec into a symbolic object. The hyp is symbolically executed on these symbolic inputs. Parametrizing the symbolic objects by the resulting predicate object yields (absent any G-APPLY or G-VAR objects) symbolic objects with coverage restricted to only inputs satisfying the hyp.

Here is a simple example theorem:

(def-gl-thm commutativity-of-+-up-to-16
   :hyp (and (natp a) (natp b)
             (< a 16) (< b 16))
   :concl (equal (+ a b) (+ b a))
   :g-bindings '((a (:g-number (0 2 4 6 8)))
                 (b (:g-number (1 3 5 7 9)))))

This theorem binds its free variables a and b to symbolic numbers of five bits. Note that integers are two's-complement, so to represent natural numbers one needs one more bit than in the unsigned representation. Therefore, these shape specs cover negative numbers down to -16 as well as naturals less than 16. However, parametrization by the hypotheses will yield symbolic objects that only cover the specified range.

The coverage obligation for a theorem will be a goal like this:

(implies <hyp>
         (shape-spec-obj-in-range
          (list <shape-spec1> <shape-spec2> ...)
          (list <var-name1> <var-name2> ...)))

In the example above:

(implies (and (natp a) (natp b)
              (< a 16) (< b 16))
         (shape-spec-obj-in-range
          '((:g-number (0 2 4 6 8)) (:g-number (1 3 5 7 9)))
          (list a b)))

It is often convenient to work out the coverage theorem before running the symbolic simulation, since the symbolic simulation may take a very long time even when successful. The keyword argument :test-side-goals may be given a value of T in order to attempt the coverage proof on its own; if successful, no theorem will be stored by ACL2, but one can then be fairly sure that the coverage proof will go through in the real theorem.

Several hints are given by default for proving coverage; see shape-specs for details. The keyword arguments :cov-theory-add, :do-not-expand, :cov-hints, and :cov-hints-position affect the coverage proof.

When proof by symbolic simulation fails, the clause processor will print randomized counterexamples. The keyword argument :n-counterexamples determines how many it prints. The default is 3. (For SAT-based proofs, likely only one counterexample is available, so it may print the same counterexample each time.)

By default, the clause processor will execute conclusion on the counterexamples that it finds; this is useful for printing debugging information. However, sometimes the conclusion is not executable; in that case, you may turn off execution of counterexamples using :exec-ctrex nil.

A symbolic simulation may result in a symbolic object that can't be syntactically determined to be non-nil; for example, the result may contain a :G-APPLY object. In these situations, the proof attempt will abort, and an example will be shown of inputs for which the symbolic result's value could not be determined. To debug this type of problem, see false-counterexamples.

The symbolic interpreter and all symbolic counterpart functions take a clock argument to ensure termination. The starting clocks for the symbolic executions of the hyp (for parametrization) and the conclusion may be set using the keyword arguments :hyp-clk and :concl-clk; the defaults are both 1000000.

The keyword argument :clause-proc can be used to select the clause processor to be used; see def-gl-clause-processor. By default, the latest clause processor introduced is used. If no :clause-proc keyword argument is given, then this macro expands to a make-event, which in turn expands to the defthm event; otherwise, this expands directly to the defthm.

The keyword argument :rule-classes can be used to select the rule-classes for the theorem produced, as in defthm; the default is :rewrite.

Subtopics

Def-gl-rule: A slightly enhanced version of def-gl-thm
Defthm-using-gl: Prove a theorem using GL, including GL only locally.
Gl-thm: Prove a theorem using GL symbolic simulation, but don't store it, like with thm.