Logical Considerations

This Developer's Guide may give the impression that ACL2
maintenance is primarily a programming exercise, and that is probably true.
However,

**Note:**

An ACL2 session has at least three logical interpretations, as follows.

- The corresponding
, which is the sequence of all*history**axiomatic events*from the session: this includes`defun`,`defchoose`, and`defaxiom`events, as well as`encapsulate`events with non-empty signatures. It does not include`defthm`events. - The corresponding
, which is the sequence of all events from the session with logical content. Thus the history is a subsequence of the chronology, but the chronology also includes*chronology*defthm events. - The corresponding
of the session, which is the first-order theory of its history, that is, axiomatized by the formulas in its history. (Careful: This theory is not sensitive to which runes are enabled, unlike the macro,*theory*`current-theory`.) A basic property of ACL2 is that all formulas in the session's chronology are provable in the session's theory. In particular, by restricting to the chronology of events up to and including a givendefthm event, we see that the formula of that event is provable from the axiomatic events that precede it.

When a session *conservative
extension* of the theory

Note that `defattach` events are ignored for all three notions listed
above. There is also a notion of *evaluation theory*, which is the
extension of the session's theory by the equations that equate each function
with its attachment. A basic property is that every evaluation theory built
from a session free of

There is also a logical explanation for `apply$`, which is based on
the notion of evaluation theory mentioned above for

IN THIS SECTION WE CAN FOCUS MAINLY ON THE DISPLAYS.

Many soundness bugs in past versions of ACL2 — indeed, perhaps the
majority of them — can be attributed to a subtle mishandling of `local` events. Perhaps the only advice possible in this regard is the
following: Think carefully about the effects of

Consider for example the following, seemingly innocuous ``enhancement'':
allow `verify-guards` to comprehend macro-aliases (see macro-aliases-table). Such an ``enhancement'' would be unsound! Instead, a
similar but sound enhancement, `encapsulate` and `local`, for why such an enhancement to

We turn now to discuss a key mechanism for avoiding potential soundness
issues caused by `ACL2-defaults-table`. Because of the
logical information stored in this table, it is prohibited to modify
this table locally, as we illustrate with a couple of examples. First
consider the following introduction of a program-mode function,

(encapsulate () (program) (defun f () (not (f))))

If the

A slightly more subtle example is the following.

(encapsulate () (set-ruler-extenders :all) (defun foo (x) (cons (if (consp x) (foo (cdr x)) x) 3)))

The induction scheme stored for

ACL2 !>(getpropc 'foo 'induction-machine) ((TESTS-AND-CALLS ((CONSP X)) (FOO (CDR X))) (TESTS-AND-CALLS ((NOT (CONSP X))))) ACL2 !>

The

(skip-proofs (defun foo (x) (declare (xargs :measure (acl2-count x))) (cons (if (consp x) (foo (cdr x)) x) 3)))

But that induction-machine is unsound!

(thm nil :hints (("Goal" :induct (foo x))))

The two examples above illustrate the importance of thinking about whether
an event can soundly be local. If not, then it may be best for that event to
be one that sets the `ACL2-defaults-table`, like `program` and
`set-ruler-extenders`, since `table` events that set the

IN THE WORKSHOP THE FOCUS WILL BE ONLY ON THE LOGICAL DIFFERENCE.

There is a fundamental logical difference between wrapping `skip-proofs` around a `defthm` event and using `defaxiom`. When
using

Since the use of `skip-proofs` carries an implicit promise of
provability, the implementation can largely ignore the question of whether an
event was, or was not, introduced using `certify-book` when the use of keyword
argument

On the other hand, it is critical for soundness to track the use of `defaxiom`. In particular, it is unsound to allow local

(encapsulate () (local (defaxiom bad-axiom nil :rule-classes nil)) (defthm bad-theorem nil :hints (("Goal" :use bad-axiom)) :rule-classes nil))

That event is, of course, rejected by ACL2. The following, on the other hand, is accepted; but this does not demonstrate unsoundness of ACL2, because the user violated the implied promise that, quoting from above, ``the ensuing proof obligations are indeed theorems of the theory of the current ACL2 session.''

(encapsulate () (local (skip-proofs (defthm bad-axiom nil :rule-classes nil))) (defthm bad-theorem nil :hints (("Goal" :use bad-axiom)) :rule-classes nil))

We conclude this section by noting that there are different ``levels'' of

Every proposed definition with recursion generates two related artifacts: a
proof obligation that is generally described as the termination proof
obligation, and an induction scheme to be stored if the definition is
admitted.

(defun f (x) (if (consp x) (cons (if (consp (car x)) (f (car x)) x) x) x))

The generated induction is displayed symbolically just below: when proving
a proposition

ACL2 !>(getpropc 'f 'induction-machine) ((TESTS-AND-CALLS ((CONSP X)) (F (CAR X))) (TESTS-AND-CALLS ((NOT (CONSP X))))) ACL2 !>

There is a comment just above the

<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X)) (F (CAR X)))))

What this means is that ACL2 must prove that under the hypothesis

But let us try an experiment in which ACL2 is instructed to consider, for
termination and induction, any

(defun f (x) (declare (xargs :ruler-extenders (cons))) (if (consp x) (cons (if (consp (car x)) (f (car x)) x) x) x))

The induction machine produced this time includes the extra

ACL2 !>(getpropc 'f 'induction-machine) ((TESTS-AND-CALLS ((CONSP X) (CONSP (CAR X))) (F (CAR X))) (TESTS-AND-CALLS ((CONSP X) (NOT (CONSP (CAR X))))) (TESTS-AND-CALLS ((NOT (CONSP X))))) ACL2 !>

This time there is a different termination proof obligation as well,
stating that

<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X) (CONSP (CAR X))) (F (CAR X)))))

Now suppose that the implementation is careless, by making the ruler-extenders affect the termination proof obligations but not the induction scheme. Consider the following example.

(defun g (x) (declare (xargs :ruler-extenders (cons))) (cons (if (consp x) (g (car x)) x) x))

This produces the termination proof obligation represented as follows
(again from a trace), which says that assuming

<1 (TERMINATION-MACHINE ((TESTS-AND-CALL ((CONSP X)) (G (CAR X)))))

To see what the induction scheme would be if we ignored the ruler-extenders, we submit the following.

(skip-proofs (defun g (x) (declare (xargs :measure (acl2-count x))) (cons (if (consp (car x)) (g (car x)) x) x)))

The corresponding induction machine states that to prove

ACL2 !>(getpropc 'g 'induction-machine) ((TESTS-AND-CALLS NIL (G (CAR X)))) ACL2 !>

If we let

(thm (consp x) :hints (("Goal" :induct (g x))))

This induction scheme is thus clearly unsound.

The moral of the story is this: As the termination machine is modified to accommodate the ruler-extenders, the induction machine must be modified accordingly. More generally, and as already noted: The termination machine must justify the induction machine.

The logical underpinnings of ACL2 can be a bit overwhelming when considered
together, so the following paragraphs should be taken as a suggestion for what
to explore only when you're in the mood for some logic, and also as an
acknowledgment that many subtle logical issues exist. It is *NOT* meant
as a prescription for what you need to explore! Moreover, it is far from
complete.

The foundations of metatheoretic reasoning can be challenging. If you
tags-search for ``; Essay on Metafunction Support'', you'll see two relevant
essays. But a much longer essay is the ``Essay on Correctness of Meta
Reasoning''. That essay even ties into the ``Essay on Defattach'', at the
mention of the Attachment Restriction Lemma. If you decide to change the
handling of metafunctions or clause-processors or their corresponding rule-classes,

A few other features of ACL2 with interesting logical foundations are
`defchoose`, `defabsstobj`, and the interaction of packages with
`local` (see the ``Essay on Hidden Packages'').

NEXT SECTION: developers-guide-programming