That completes the proof of *1.Summary Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...) Rules: ((:REWRITE CDR-CONS) (:REWRITE CAR-CONS) (:DEFINITION NOT) (:DEFINITION ENDP) (:FAKE-RUNE-FOR-TYPE-SET NIL) (:DEFINITION APP)) Warnings: None Time: 0.27 seconds (prove: 0.10, print: 0.05, other: 0.12) ASSOCIATIVITY-OF-APP

This completes the Walking Tour.

We intend to document many other parts of the system this way, but we just haven't gotten around to it.

If you feel like reading more, see tutorial-examples in the documentation. There you will find several challenging but simple applications. At the conclusion of the examples is a simple challenge to try.

We hope you enjoy ACL2. We do.

Matt Kaufmann and J Strother Moore

At the conclusion of most events (click here for a
brief discussion of events or see events ), ACL2 prints a
summary. The summary for `app`

is:

Summary Form: ( DEFUN APP ...) Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL)) Warnings: None Time: 0.03 seconds (prove: 0.00, print: 0.00, other: 0.03) APP

The ``rules'' listed are those used in function admission or proof summarized. What is actually listed are ``runes'' (see rune) ) which are list-structured unique names for rules in the ACL2 data base or ``world'' . Using theories you can ``enable'' and ``disable'' rules so as to make them available (or not) to the ACL2 theorem prover.

The ``warnings'' mentioned (none are listed for `app`

) remind the
reader whether the event provoked any warnings. The warnings
themselves would have been printed earlier in the processing and
this part of the summary just names the earlier warnings printed.

The ``time'' indicates how much processing time was used and is
divided into three parts: the time devoted to proof, to printing,
and to syntactic checks, pre-processing and data base updates.
Despite the fact that ACL2 is an applicative language it is possible
to measure time with ACL2 programs. The `state`

contains a
clock. The times are printed in decimal notation but are actually
counted in integral units.

The final `APP`

is the value of the `defun`

command and was
printed by the read-eval-print loop. The fact that it is indented
one space is a subtle reminder that the command actually returned an
``error triple'', consisting of a flag indicating (in this case)
that no error occurred, a value (in this case the symbol `APP`

),
and the final `state`

). See ld-post-eval-print
for some details. If you really want to follow that link,
however, you might see ld first.

You should now return to the Walking Tour.

Subgoal *1/2 (IMPLIES (AND (NOT (ENDP A)) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))).

Click on the link above (the open parenthesis before `ENDP`

)
to replace `(ENDP A)`

by its definition.

Subgoal *1/2 (IMPLIES (AND (NOT(NOT (CONSP A))) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))).

The **bold** text is the instantiated definition of `ENDP`

.

Now click on the link above to simplify (NOT (NOT (CONSP A)))

Subgoal *1/2' (IMPLIES (AND(CONSP A)(EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))).

Note that this is `Subgoal *1/2'.`

You may click here to return to the main proof.

One particularly famous and very simple model is the equation of a falling body: the distance d an object falls is proportional to the square of the time t. If the time is measured in seconds and the distance in feet, the equation relating these two is

2 d = 16t

This equation is a **model** of falling objects. It can be used to
predict how long it takes a cannonball to fall from the top of a 200
foot tower (3.5 seconds). This might be important if your product
is designed to drop cannonballs on moving targets.

Click here to continue

Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP (APP A B) C) (APP A (APP B C)))).

Click on the link above to replace `(APP A B)`

by its definition.
Note that the hypothesis `(NOT (CONSP A))`

allows us to simplify
the `IF`

in `APP`

to its **false branch** this time.

Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APPBC)`(`

APP A (APP B C)))).

Click on the link above to expand the definition of `APP`

. Again,
we come out through the false branch because of the hypothesis.

Subgoal *1/1' (IMPLIES (NOT (CONSP A)) (EQUAL (APP B C)(APP B C))).

Click on the link above to use the Axiom `(EQUAL x x) = t`

Subgoal *1/1' (IMPLIES (NOT (CONSP A))T)

Now that its conclusion is identically `T`

the `IMPLIES`

will simplify to `T`

(not shown) and we are done with `Subgoal *1/1'`

.

You may click here to return to the main proof.

So here we see our associativity rule being used!

The rewriter sweeps the conjecture in a **leftmost innermost** fashion,
applying rewrite rules as it goes.

The associativity rule is used many times in this sweep. The first ``target'' is highlighted below. Click on it to see what happens:

Current Conjecture: (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))

(AND (IMPLIES (AND (NOT (ENDP A)) ; Induction Step: test (:P (CDR A) B C)) ; and induction hypothesis (:P A B C)) ; implies induction conclusion. (IMPLIES (ENDP A) (:P A B C))) ; Base Case

The formula beginning with this parenthesis is the induction scheme
suggested by `(APP A B)`

applied to `(P A B C)`

.

It is a **conjunction** (`AND`

) of two formulas.

The first is the **induction step** and the second is the **base case**.

This formula is the **Induction Step**. It basically consists of
three parts, a test identifying the inductive case, an induction
hypothesis and an induction conclusion.

(IMPLIES (AND (NOT (ENDP A))When we prove this we can assume; Test(:P (CDR A) B C)); Induction Hypothesis(:P A B C)); Induction Conclusion

*`A`

is not empty, and that* the associativity conjecture holds for a ``smaller'' version of

`A`

, namely,`(CDR A)`

.

Under those hypotheses we have to prove the associativity conjecture
for `A`

itself.

The induction scheme just shown is just an abbreviation for our real goal.

To obtain our actual goals we have to replace the schema `:P`

by
the associativity conjecture (instantiated as shown in the scheme).

This produces two actual goals, the induction step and the base case.

This paragraph explains why the induction selected is legal. The
explanation is basically the same as the explanation for why the
recursion in `(APP A B)`

terminates.

Here is the theorem prover's output when it processes the **defthm**
command for the associativity of `app`

. We have highlighted text
for which we offer some explanation, and broken the presentation into
several pages. Just follow the Walking Tour after exploring the
explanations.

ACL2!>(defthm associativity-of-app(equal (app (app a b) c)(app a (app b c))))Name the formula above *1.

Perhaps we can prove *1 by induction. Three induction schemes are suggested by this conjecture. Subsumption reduces that number to two. However, one of these is flawed and so we are left with one viable candidate.

We will induct according to a scheme suggested by (APP A B). If we let (:P A B C) denote *1 above then the induction scheme we'll use is (AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C)) (:P A B C)) (IMPLIES (ENDP A) (:P A B C))). This induction is justified by the same argument used to admit APP, namely, the measure (ACL2-COUNT A) is decreasing according to the relation E0-ORD-< (which is known to be well-founded on the domain recognized by E0-ORDINALP). When applied to the goal at hand the above induction scheme produces the following two nontautological subgoals.

**Q.E.D.** stands for ``quod erat demonstrandum'' which is
Latin for ``which was to be demonstrated'' and is the signal that
a proof is completely done.

Note that under **Rules** we list the runes of all
the rules used in the proof. This list says that we used the
rewrite rules `CAR-CONS`

and `CDR-CONS`

, the definitions of the
functions `NOT`

, `ENDP`

and `APP`

, and primitive type reasoning
(which is how we simplified the `IF`

and `EQUAL`

terms).

For what it is worth, `IMPLIES`

and `AND`

are actually
macros that are expanded into `IF`

expressions before the proof ever begins. The use of macros is not
reported among the rules.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP A B) C) (APP A (APP B C)))).

Click on the link above to replace `(APP A B)`

by its definition.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP(IF(CONSP A)(CONS (CAR A) (APP (CDR A) B))B)C) (APP A (APP B C)))).

Note that the `IF`

expression above is the simplified body of `APP`

.
But we know the test `(CONSP A)`

is true, by the first hypothesis.
Click on the link above to replace the test by `T`

. Actually
this step and several subsequent ones are done during the simplification
of the body of `APP`

but we want to illustrate the basic principles of
simplification without bothering with every detail.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (APP (CDR A) B) C)(APP (CDR A) (APP B C)))).

Click on the link above to use the Induction Hypothesis (which is the
second of the two hypotheses above and which is identical to the rewritten
conclusion).

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C))))T)

Click on the link above to use the definition of `IMPLIES`

. Since
the conclusion of the implication is now identically `T`

, the
implication simplifies to `T`.

Subgoal *1/2'T

So, indeed, `Subgoal *1/2'`

**does** simplify to T!

You can see that even in an example as simple as this one, quite a lot happens in simplification.

You may click here to return to the main proof.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (IFT(CONS (CAR A) (APP (CDR A) B)) B) C) (APP A (APP B C)))).

Click on the link above to apply the Axiom `(IF T x y) = x`

.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP(CONS (CAR A) (APP (CDR A) B))C) (APP A (APP B C)))).

Click on the link above to apply the expand the definition of `APP`

here.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF (CONSP (CONS (CAR A) (APP (CDR A) B)))(CONS (CAR (CONS (CAR A) (APP (CDR A) B)))(APP (CDR (CONS (CAR A) (APP (CDR A) B)))C))C)(APP A (APP B C)))).

Click on the link above to apply the Axiom `(CONSP (CONS x y)) = T`

.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IFT(CONS (CAR (CONS (CAR A) (APP (CDR A) B))) (APP (CDR (CONS (CAR A) (APP (CDR A) B))) C)) C) (APP A (APP B C)))).

Click on the link above to apply the Axiom `(CAR (CONS x y)) = x`

.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF T (CONS(CAR A)(APP (CDR (CONS (CAR A) (APP (CDR A) B))) C)) C) (APP A (APP B C)))).

Click on the link above to apply the Axiom `(CDR (CONS x y)) = y`

.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (IF T (CONS (CAR A) (APP(APP (CDR A) B)C)) C) (APP A (APP B C)))).

Click on the link above to apply the Axiom `(IF T x y) = x`

.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL(CONS (CAR A)(APP (APP (CDR A) B)C))(APP A (APP B C)))).

Click on the link above to expand the definition of `APP`

here.
This time, we'll do the whole expansion at once, including the
simplification of the resulting `IF`

. This is how ACL2 actually
does it.

Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (CONS (CAR A) (APP (APP (CDR A) B) C))(CONS (CAR A)(APP (CDR A) (APP B C))))).

Click on the link above to apply the Axiom that
`(EQUAL (CONS x y) (CONS u v))`

is equal to the conjunction of
`(EQUAL x u)`

and `(EQUAL y v)`

. In this case, `(EQUAL x u)`

is trivial, `(EQUAL (CAR A) (CAR A))`

.

Note that at the conclusion of the proof, the system reminds you
of the earlier **Warning**.

It is a good idea, when the **Q.E.D.** flys by, to see if there were
any Warnings.

ACL2!>(defthm associativity-of-app(equal (app (app a b) c)(app a (app b c))))

The formula above says `app`

is associative. The `defthm`

command instructs ACL2 to prove the formula and to name it
`associativity-of-app`

. Actually, the `defthm`

command also
builds the formula into the data base as a `rewrite`

rule,
but we won't go into that just yet.

What we will consider is how the ACL2 theorem prover proves this formula.

If you proceed you will find the actual output of ACL2 in response to the command above. Some of the text is highlighted for the purposes of the tour. ACL2 does not highlight its output.

You will note that we sometimes highlight a single open parenthesis. This is our way of drawing your attention to the subformula that begins with that parenthesis. By clicking on the parenthesis you will get an explanation of the subformula or its processing.

The time it took us to explain this proof may leave the impression that the proof is complicated. In a way, it is. But it happens quickly.

The time taken to do this proof is about 1/10 second. The rest of the time (about 2/10 seconds) is spent in pre- and post-processing.

Basically, this proof flashes across your screen before you can read
it; you see the **Q.E.D.** and don't bother to scroll back to
read it. You have more important things to do than read successful
proofs.

ACL2 is a very large, multipurpose system. You can use it as a programming language, a specification language, a modeling language, a formal mathematical logic, or a semi-automatic theorem prover, just to name its most common uses.

This home page includes all of ACL2's online documentation, which is quite extensive. To help ease your introduction to ACL2, we have built two tours through this documentation.

Newcomers to ACL2 should first take the ``Flying Tour.'' Then, if you want to know more, take the ``Walking Tour.''

To start a tour, click on the appropriate icon below.

For readers using Web browsers: This ``page'' actually contains many other pages of our documentation, organized alphabetically and separated by many blank lines. Be careful when using the scroll bar!

For readers using our :DOC or our TexInfo format in Emacs: The tours
will probably be unsatisfying because we use gif files and assume you
can navigate ``back.''

This **Warning** alerts us to the fact that when treated as a
**rewrite** rule, the new rule `TRIVIAL-CONSEQUENCE`

, rewrites
terms of the same form as a rule we have already proved, namely
`ASSOCIATIVITY-OF-APP`

.

When you see this warning you should **think about your rules**!

In the current case, it would be a good idea **not** to make
`TRIVIAL-CONSEQUENCE`

a rule at all. We could do this with
:`rule-classes`

nil.

ACL2 proceeds to try to prove the theorem, even though it printed
some warnings. The basic assumption in ACL2 is that the **user**
**understands what he or she is doing** but may need a little reminding
just to manage a complicated set of facts.

This topic has not yet been documented. Sorry

If we have proved the `associativity-of-app`

rule, then the
following theorem is trivial:

(defthm trivial-consequence (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))Below we show the proof

ACL2 is a **mathematical logic** together with a
**mechanical theorem prover** to help you reason in the logic.

The logic is just a subset of applicative Common Lisp.

The theorem prover is an ``industrial strength'' version of the Boyer-Moore theorem prover, Nqthm.

**Models** of all kinds of computing systems can be built in ACL2, just as
in Nqthm, even though the formal logic is Lisp.

Once you've built an ACL2 model of a system, you can run it.

You can also use ACL2 to prove theorems about the model.

It is not easy to build ACL2 models of complex systems. To do so, the
user must **understand**

* the system being modeled, and* ACL2, at least as a programming language.

It is not easy to get ACL2 to prove hard theorems. To do so, the user must
**understand**

* the model,ACL2 will help construct the proof but its primary role is to prevent logical mistakes. The creative burden -- the mathematical insight into* ACL2 as a mathematical logic, and

* be able to construct a proof (in interaction with ACL2).

A mathematical logic is a formal system of formulas (**axioms**) and
**rules** for deriving other formulas, called **theorems**.

A **proof** is a derivation of a theorem. To see a concrete proof
tree, click here.

Why should you care? The neat thing about Theorems is that they are ``true.'' More precisely, if all the axioms are valid and the rules are validity preserving, then anything derived from the axioms via the rules is valid.

So, if you want to determine if some formula is true, **prove it**.

A **mechanical theorem prover** is a computer program that finds
proofs of theorems.

The ideal mechanical theorem prover is **automatic**: you give
it a formula and it gives you a proof of that formula or tells you
there is no proof.

Unfortunately, automatic theorem provers can be built only for very
simple logics (e.g., **propositional calculus**) and even then
practical considerations (e.g., how many
centuries you are willing to wait) limit the problems they can solve.

To get around this, mechanical theorem provers often require help from
the **user**.

Click here to continue downward.

This is **good** and **bad**.

The good news is that you can **program** ACL2's simplifier.

The bad news is that when you command ACL2 to prove a theorem you must
give some thought to **how that theorem is to be used as a rule**!

For example, if you engaged in the mathematically trivial act of proving the associativity rule again, but with the equality reversed, you would have programmed ACL2's rewriter to loop forever.

You can avoid adding any rule by using the command:

(defthm associativity-of-app (equal (app (app a b) c) (app a (app b c))):rule-classes nil)