Illustration using tracing, comments and Essays to explore ACL2 behaviors

This topic grew out of a discussion on the acl2-devel mailing list in which some relevant background had already been presented. It illustrates how one might go about learning about specific features of ACL2, in this case aspects of the tau-system.

First,

(include-book ``tau/bounders/elementary-bounders'' :dir :system)

and

(trace$ tau-term)

and then submit the non-theorem:

(thm (implies (and (natp x)(<= 0 x) (<= x 15)) (equal xxx (+ 3 x))))

The objective is to see what the tau of

If you search the failed proof for the first call of

<2 (TAU-TERM ((NIL) (INTEGERP (NIL . 3) NIL . 18) ((166 . FILE-CLOCK-P) (155 . 32-BIT-INTEGERP) (20 . O-FINP) (19 . POSP) (17 . NATP) (9 . EQLABLEP) (5 . RATIONALP) (4 . INTEGERP) (0 . ACL2-NUMBERP)) (192 . BAD-ATOM) (182 . ZPF) (176 . WRITABLE-FILE-LISTP1) (173 . READ-FILE-LISTP1) (170 . WRITTEN-FILE) (167 . READABLE-FILE) (163 . OPEN-CHANNEL1) (137 . KEYWORDP) (129 . LOWER-CASE-P) (128 . UPPER-CASE-P) (127 . ALPHA-CHAR-P) (124 . STANDARD-CHAR-P) (118 . IMPROPER-CONSP) (117 . PROPER-CONSP) (104 . WEAK-ABSSTOBJ-INFO-P) (72 . WEAK-CURRENT-LITERAL-P) (34 . WEAK-IO-RECORD-P) (31 . BOOLEANP) (27 . MINUSP) (18 . BITP) (16 . ZIP) (15 . ZP) (7 . SYMBOLP) (6 . STRINGP) (3 . CONSP) (2 . COMPLEX-RATIONALP) (1 . CHARACTERP)) ...)

The

You can decode it with

(decode-tau '((NIL) (INTEGERP (NIL . 3) NIL . 18) ((166 . FILE-CLOCK-P) (155 . 32-BIT-INTEGERP) (20 . O-FINP) (19 . POSP) (17 . NATP) (9 . EQLABLEP) (5 . RATIONALP) (4 . INTEGERP) (0 . ACL2-NUMBERP)) (192 . BAD-ATOM) (182 . ZPF) (176 . WRITABLE-FILE-LISTP1) (173 . READ-FILE-LISTP1) (170 . WRITTEN-FILE) (167 . READABLE-FILE) (163 . OPEN-CHANNEL1) (137 . KEYWORDP) (129 . LOWER-CASE-P) (128 . UPPER-CASE-P) (127 . ALPHA-CHAR-P) (124 . STANDARD-CHAR-P) (118 . IMPROPER-CONSP) (117 . PROPER-CONSP) (104 . WEAK-ABSSTOBJ-INFO-P) (72 . WEAK-CURRENT-LITERAL-P) (34 . WEAK-IO-RECORD-P) (31 . BOOLEANP) (27 . MINUSP) (18 . BITP) (16 . ZIP) (15 . ZP) (7 . SYMBOLP) (6 . STRINGP) (3 . CONSP) (2 . COMPLEX-RATIONALP) (1 . CHARACTERP)) '(binary-+ '3 x))

If

(AND (ACL2-NUMBERP (BINARY-+ '3 X)) (INTEGERP (BINARY-+ '3 X)) ; <--- (RATIONALP (BINARY-+ '3 X)) (EQLABLEP (BINARY-+ '3 X)) (NATP (BINARY-+ '3 X)) (POSP (BINARY-+ '3 X)) (O-FINP (BINARY-+ '3 X)) (32-BIT-INTEGERP (BINARY-+ '3 X)) (FILE-CLOCK-P (BINARY-+ '3 X)) (<= 3 (BINARY-+ '3 X)) ; <--- (<= (BINARY-+ '3 X) 18) ; <--- (NOT (CHARACTERP (BINARY-+ '3 X))) (NOT (COMPLEX-RATIONALP (BINARY-+ '3 X))) (NOT (CONSP (BINARY-+ '3 X))) (NOT (STRINGP (BINARY-+ '3 X))) (NOT (SYMBOLP (BINARY-+ '3 X))) (NOT (ZP (BINARY-+ '3 X))) (NOT (ZIP (BINARY-+ '3 X))) (NOT (BITP (BINARY-+ '3 X))) (NOT (MINUSP (BINARY-+ '3 X))) (NOT (BOOLEANP (BINARY-+ '3 X))) (NOT (WEAK-IO-RECORD-P (BINARY-+ '3 X))) (NOT (WEAK-CURRENT-LITERAL-P (BINARY-+ '3 X))) (NOT (WEAK-ABSSTOBJ-INFO-P (BINARY-+ '3 X))) (NOT (PROPER-CONSP (BINARY-+ '3 X))) (NOT (IMPROPER-CONSP (BINARY-+ '3 X))) (NOT (STANDARD-CHAR-P (BINARY-+ '3 X))) (NOT (ALPHA-CHAR-P (BINARY-+ '3 X))) (NOT (UPPER-CASE-P (BINARY-+ '3 X))) (NOT (LOWER-CASE-P (BINARY-+ '3 X))) (NOT (KEYWORDP (BINARY-+ '3 X))) (NOT (OPEN-CHANNEL1 (BINARY-+ '3 X))) (NOT (READABLE-FILE (BINARY-+ '3 X))) (NOT (WRITTEN-FILE (BINARY-+ '3 X))) (NOT (READ-FILE-LISTP1 (BINARY-+ '3 X))) (NOT (WRITABLE-FILE-LISTP1 (BINARY-+ '3 X))) (NOT (ZPF (BINARY-+ '3 X))) (NOT (BAD-ATOM (BINARY-+ '3 X))))

Another way of thinking about a tau,

`(lambda (zzz) ,(decode-tau <tau> 'zzz))

Of course, a tau is very redundant. There is no reason to say that something's NOT a bad-atom if you say it IS a NATP! But by encoding everything the tau system knows about a term it's easy to answer questions about what we know.

Now, going back to that call of

(TAU-TERM '(BINARY-+ '3 X) <tau-alist> '(((EQUAL (BINARY-+ '3 X) XXX) ; type-alist 128 (LEMMA (:FAKE-RUNE-FOR-TYPE-SET NIL))) ((< '15 X) 128) ((< X '0) 128) (X 7) (X 23)) '(((0 (((((X . -1)) NIL) 15 <= T))) ; linear pot list X (((((X . 1)) NIL) 0 <= T)))) <ens> <w> <calist>)

Let's assume that we already know about the type-alist and the
linear pot (see linear-arithmetic); they're set up when

The

When playing with

It is also acceptable to use

The general lesson here is simple: if you want to try to understand some
part of the prover, `trace$` it and give the prover a formula that will
exercise the part in question and look at how it's called and what it
returns.

Of course, you can also read the comments! There is a good essay on the tau system that is well worth reading if you're interested.

; Essay on the Tau System ; This essay touches on a wide variety of topics in the design of the tau ; system. It is consequently divided into many subsections with the following ; headers. We recommend scanning this list for subsections of interest; an ; introduction to tau is provided by the first six or so, in order. ; On Tau-Like Terms ; On the Name ``tau'' ; On Some Basic Ideas ; On Tau Recognizers -- Part 1 ; On the Tau Database and General Design ; On Tau Recognizers -- Part 2 ; On Tau Intervals and < versus <= ; On the Tau Data Structure ; On the Built-in Tau and the Abuse of Tau Representation ; On the Additional Restrictions on Tau Fields ; On the Use of ENS by Function Evaluation in the Tau System ; On the Most Basic Implications of Being in an Interval ; On Firing Signature Rules ; On Comparing Bounds ; On the Proof of Correctness of upper-bound-< ; On the Near-Subset Relation for Intervals ; On the Tau Database ; On Closing the Database under Conjunctive Rules ; On Converting Theorems in the World to Tau Rules ; On Tau-Like Terms ; On Loops in Relieving Dependent Hyps in Tau Signature Rules ; On the Tau Msgp Protocol ; On Removal of Ancestor Literals -- The Satriani Hack Prequel ; On the Motivation for Tau-Subrs ; On the Tau Completion Alist (calist) ; On Disjoining Tau ; On the Role of Rewriting in Tau ; On Tau-Clause -- Using Tau to Prove or Mangle Clauses ; On Tau Debugging Features

NEXT SECTION: developers-guide-build