Major Section: RULE-CLASSES
This documentation topic describes the syntactic form of ``tau-system'' rules; these rules extend ACL2's ``type checker.'' For an introduction to the tau system, see introduction-to-the-tau-system.
There happens to be a function named
tau-system, defined as the
identity function. Its only role is to provide the rune
(:EXECUTABLE-COUNTERPART TAU-SYSTEM), which is used to enable and disable
the tau system. Otherwise the function
tau-system has no purpose and we
recommend that you avoid using it so you are free to enable and disable the
When in the default (``greedy'') mode (see
defun and every
rule-classes) of every
defthm stored as a rule of any
:rule-class is inspected to
determine if it is of one of the forms below. Rules of these forms are added
to the tau database, even if they are not labeled as
rewrite rule might contribute to the tau database! To
add a rule to the tau database without adding any other kind of rule, tag it
:tau-system. If a theorem has
nil, it is not considered for the tau database.
General Forms: Boolean: (booleanp (p v)) Eval: (p 'const) or (p *const*) Simple: (implies (p v) (q v)) Conjunctive: (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1. Signature Form 1: (implies (and (p1 x1) (p2 x2) ...) (q (fn x1 x2 ...))) Signature Form 2: (implies (and (p1 x1) (p2 x2) ...) (q (mv-nth 'n (fn x1 x2 ...)))) Big Switch: (equal (fn . formals) body) MV-NTH Synonym: (equal (nth-alt x y) (mv-nth x y)) or (equal (mv-nth x y) (nth-alt x y))The symbols
p1, etc., denote monadic (one-argument) Boolean-valued function symbols, or equalities in which one argument is constant, arithmetic comparisons in which one argument is a rational or integer constant, or the logical negations of such terms. By ``equalities'' we allow
=. By ``arithmetic comparison'' we mean
>. Any of these tau predicates may appear negated.
(p v) above might stand for any one of:
(INTEGERP X) (EQUAL V 'MONDAY) (<= I 16) (NOT (EQUAL X 'SUNDAY))
The different rule forms above affect different aspects of the tau system. We discuss each form in more detail below.
The documentation below is written as though the tau system is in auto mode!
To insure that the only rules added to the tau system are those explicitly
:tau-system, you should use
set-tau-auto-mode to select manual mode.
General Form: Boolean: (booleanp (p v))Here
pmust be a function symbol and
vmust be a variable. Such a
pto the list of tau predicates. If
pwas recognized as Boolean when it was defined, there is no need to state this rule. This form is needed if you define a monadic Boolean function in such a way that the system does not recognize that it is Boolean.
General Form: Eval: (p 'const) or (p *const*)
p must be a function symbol. In addition, recall that these general
tau predicate forms may appear negated. So the form above includes such
(NOT (GOOD-STATEP *INITIAL-STATE*)). A theorem of this form thus
records whether a named predicate is true or false on the given constant.
Generally, when the tau system must determine whether an enabled tau
predicate is true or false on a constant, it simply evaluates the predicate
on the constant. This can be impossible or very inefficient if
p is not
defined but constrained, or if
p is defined in a hard-to-compute
(defun p (x) (evenp (ack x x))) where
ack is the Ackermann
function), or perhaps if the constant is very large. By proving a
:tau-system rule of Eval form, you cause the tau system to note the value
of the predicate on the constant and henceforth to look it up instead of
evaluating the definition.
A difficulty, however, is determining that a slow down is due to the
evaluation of tau predicates and not some other reason. The first step is
determining that tau is slowing the proof down. See
for an explanation of
TIME-TRACKER-NOTEs output during some proofs
involving tau reasoning. These notes can alert you to the fact that
significant amounts of time are being spent in the tau system.
Time-tracker-tau gives some ways of determining whether tau predicate
evaluation is involved. (If worse comes to worst, consider the following
hack: In the ACL2 source file
tau.lisp, immediately after the definition
of the system function
ev-fncall-w-tau-recog, there is a comment which
contains some raw Lisp code that can be used to investigate whether tau's use
of evaluation on constants is causing a problem.) However, once a recognizer
and the constants on which it is being evaluated are identified, the tau
system can be sped up by proving Eval rules to pre-compute and store the
values of the recognizer on those constants. Alternatively, at the possible
loss of some completeness in the tau system, the executable counterpart of
the recognizer can be disabled.
General Form: Simple: (implies (p v) (q v))Here
vmust be a variable symbol. This rule builds-in the information that anything satisfying
pmust also satisfy
q, i.e., the ``type''
qincludes the ``type''
p. Recall that the forms may be negated. Most of the time,
qwill be predicate symbols but it is possible they will be equalities- or inequalities-with-constants. Examples of Simple rules include the following, which are in fact built-in:
(implies (natp x) (integerp x)) (implies (integerp x) (rationalp x)) (implies (integerp x) (not (true-listp x))) (implies (natp x) (not (< x 0))) (implies (symbol-alistp x) (alistp x))Because the tau system records the transitive closure of the Simple rules, any time a term is known to satisfy
natpit is also known to satisfy
rationalp, and known not to satisfy
true-listp, and known to be non-negative.
General Form: Conjunctive: (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.The
qmay be any tau predicates or their negations,
vmust be a variable symbol, and
imust exceed 1 or else this is a Simple rule. An obvious operational interpretation of this rule is that if an object is known to satisfy all of the
pi, then it is known to satisfy
q. However, the actual interpretation is more general. For example, if an object is known to satisfy all but one of the
piand is known not to satisfy
q, then the object is known not to satisfy the ``missing''
For example, the following Conjunctive rule allows tau to conclude that if
D is not
FRI, then it is
(implies (and (weekdayp d) (not (eq d 'MON)) (not (eq d 'TUE)) (not (eq d 'WED)) (not (eq d 'THU))) (eq d 'FRI))The tau database is not closed under conjunctive rules; they are applied dynamically.
General Form: Signature Form 1: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (fn x1 x2 ... xn)))The
qmay be any tau predicates or their negations,
fnmust be a function symbol of arity
ximust be distinct variable symbols and
dep-hypmay be any term, provided it is not of the
(pi xi)shape and the only the variables in it are the
The Signature form actually allows multiple tau predicates to be applied to
each variable, e.g., x1 might be required to be both an
EVENP. The Signature form allows there to be multiple hypotheses
dep-hyps, i.e., not fitting any of the previous shapes, and
they are implicitly just conjoined. The name ``dep-hyp'' is an abbreviation
of ``dependent hypothesis'' and stems from the fact they often express
relations between several of the function's inputs rather than type-like
constraints on individual inputs.
A Signature rule informs tau that the function
fn returns an object
q provided that the arguments satisfy the respective
and provided that
dep-hyp occurs in the current context. Note: to be
precise, dependent hypotheses are relieved only by applying ACL2's most
primitive form of reasoning, type-set. In particular, tau reasoning is
not used to establish dependent hypotheses. The presence of a
a signature rule may severely restrict its applicability. We discuss this
after showing a few mundane examples.
An example Signature rule is
(implies (and (integer-listp x) (integer-listp y)) (integer-listp (append x y)))Of course, a function may have multiple signatures:
(implies (and (symbol-listp x) (symbol-listp y)) (symbol-listp (append x y)))Here is a Signature rule for the function
(implies (and (symbol-listp x) (integer-listp y)) (symbol-alistp (pairlis$ x y)))The tau system can consequently check this theorem by composing the last two rules shown and exploiting Simple rule stating that symbol-alists are also alists:
(thm (implies (and (symbol-listp a) (symbol-listp b) (integer-listp y)) (alistp (pairlis$ (append a b) y))))Since
bare known to be lists of symbols and a signature for
appendis that it preserves that predicate, the first argument to the
pairlis$expression is known to be a list of symbols. This means the Signature rule for
pairlis$tells us the result is a
symbol-alistp, but the previously mentioned Simple rule,
(implies (symbol-alistp x) (alistp x)), tells us the result is also an
When a Signature rule has an
dep-hyp, that hypothesis is not an expression
in the tau system. Tau is not used to check that hypothesis. Instead, tau uses the
more primitive type-set mechanism of ACL2. Here is an example of a Signature
rule with a
(implies (and (natp n) (integer-listp a) (< n (len a))) (integerp (nth n a)))
Note that the last hypothesis is a dependent hypothesis: it is not a tau
predicate but a relationship between
a. It is relieved by
type-set. If one is trying to compute the signature of an
(nth n a)
expression in a context in which
(< n (len a)) is explicitly assumed,
then this mechanism would establish the dependent hypothesis. But one can
easily imagine an almost identical context where, say
(< n (len (rev a)))
is explicitly assumed. In that context, the Signature rule would not be
type-set cannot establish
(< n (len a)) from
(< n (len (rev a))), even though it would be easily proved by rewriting
using the theorem
(equal (len (rev a)) (len a)).
Note also that if this signature could be phrased in a way that eliminates
the dependency between
a it would be more effective. For example,
here is a related Signature rule without a dependent hypothesis:
(implies (and (natp n) (register-filep a) (< n 16)) (integerp (nth n a)))In this theorem we require only that
nbe less than 16, which is a tau predicate and hence just an additional tau constraint on
General Form: Signature Form 2: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (mv-nth 'n (fn x1 x2 ... xn))))This form of signature rule is just like form 1 except that it is useful for functions that return multiple-values and allows us to ``type-check'' their individual outputs.
General Form: Big Switch: (equal (fn . formals) body)In the Big Switch form,
fnmust be a function symbol,
formalsmust be a list of distinct variable symbols, and
bodymust be a ``big switch'' term, i.e., one that case splits on tau predicates about a single variable and produces a term not involving that variable. An example of a Big Switch rule is
(equal (conditional-type x y) (if (consp x) (consp y) (integerp y)))The idea is that the tau system can treat calls of
conditional-typeas a tau-predicate after determining the tau of an argument.
Since equality-to-constants are tau predicates, a more common example of a Big Switch rule is
(equal (dtypep x expr) (case x (STMT (stmt-typep expr)) (EXPR (expr-typep expr)) (MODULE (module-typep expr)) (otherwise nil)))This is because
(case x (STMT ...) ...)macroexpands in ACL2 to
(if (eql x 'STMT) ... ...)and
(eql x 'STMT)is a tau predicate about
Big Switch rules are recognized when a function is defined (if tau is in
automatic mode). They generally do not have to be proved explicitly, though
they might be when mutual recursion is involved. Only the first detected Big
Switch rule about a function
fn is recognized.
General Form: MV-NTH Synonym: (equal (nth-alt x y) (mv-nth x y)) or (equal (mv-nth x y) (nth-alt x y))Rules of this form just tell the tau system that the user-defined function
nth-altis synonymous with the ACL2 primitive function
mv-nth. Because ACL2's rewriter gives special handling to
mv-nth, users sometimes define their own versions of that function so they can disable them and control rewriting better. By revealing to the tau system that such a synonym has been introduced you allow Signature rules of Form 2 to be used.