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
tau system.

When in the default (``greedy'') mode (see `set-tau-auto-mode`

), every
`defun`

and every `:corollary`

(see `:`

`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 `:tau-system`

rules,
e.g., a `:`

`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
with `:`

`rule-classes`

`:tau-system`

. If a theorem has
`:`

`rule-classes`

`nil`

, it is not considered for the tau database.

General Forms:The symbolsBoolean: (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))

`p`

, `q`

, `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 `EQUAL`

, `EQ`

, `EQL`

, and `=`

. By ``arithmetic
comparison'' we mean `<`

, `<=`

, `>=`

, or `>`

. Any of
these tau predicates may appear negated. The notation `(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
assigned to `:rule-class`

`:tau-system`

, you should use
`set-tau-auto-mode`

to select manual mode.

General Form:HereBoolean: (booleanp (p v))

`p`

must be a function symbol and `v`

must be a variable. Such a
`:tau-system`

rule adds `p`

to the list of tau predicates. If `p`

was
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*)

Here `p`

must be a function symbol. In addition, recall that these general
tau predicate forms may appear negated. So the form above includes such
theorems as `(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
way (e.g., `(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 `time-tracker-tau`

for an explanation of `TIME-TRACKER-NOTE`

s 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:HereSimple: (implies (p v) (q v))

`v`

must be a variable symbol. This rule builds-in the information
that anything satisfying `p`

must also satisfy `q`

, i.e., the ``type''
`q`

includes the ``type'' `p`

. Recall that the forms may be negated.
Most of the time, `p`

and `q`

will 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

`natp`

it is also known to satisfy
`integerp`

and `rationalp`

, and known not to satisfy `true-listp`

,
and known to be non-negative.

General Form:TheConjunctive: (implies (and (p1 v) ... (pk v)) (q v)), ; Here k must exceed 1.

`pi`

and `q`

may be any tau predicates or their negations, `v`

must
be a variable symbol, and `i`

must 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 `pi`

and is known not to
satisfy `q`

, then the object is known not to satisfy the ``missing''
`pi`

.For example, the following Conjunctive rule allows tau to conclude that if
weekday `D`

is not `MON`

, `TUE`

, `THU`

or `FRI`

, then it is `WED`

:

(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:TheSignature Form 1: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (fn x1 x2 ... xn)))

`pi`

and `q`

may be any tau predicates or their negations, `fn`

must be a function symbol of arity `n`

, the `xi`

must be distinct
variable symbols and `dep-hyp`

may be any term, provided it is not of the
`(pi xi)`

shape and the only the variables in it are the `xi`

.The Signature form actually allows multiple tau predicates to be applied to
each variable, e.g., x1 might be required to be both an `INTEGERP`

and
`EVENP`

. The Signature form allows there to be multiple hypotheses
classified as `dep-hyp`

s, 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
satisfying `q`

provided that the arguments satisfy the respective `pi`

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 `dep-hyp`

in
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

`pairlis$`

:
(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

`a`

and `b`

are known to be lists of symbols and a signature for
`append`

is 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 `alistp`

.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 `dep-hyp`

:

(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 `n`

and `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
fired because `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 `n`

and `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

`n`

be less than 16, which is a tau
predicate and hence just an additional tau constraint on `n`

.

General Form: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.Signature Form 2: (implies (and (p1 x1) (p2 x2) ... (pn xn) dep-hyp) (q (mv-nth 'n (fn x1 x2 ... xn))))

General Form:In the Big Switch form,Big Switch: (equal (fn . formals) body)

`fn`

must be a function symbol, `formals`

must be
a list of distinct variable symbols, and `body`

must 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-type`

as
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 `x`

.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:Rules of this form just tell the tau system that the user-defined functionMV-NTH Synonym: (equal (nth-alt x y) (mv-nth x y)) or (equal (mv-nth x y) (nth-alt x y))

`nth-alt`

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