This is acl2-doc-emacs.info, produced by makeinfo version 4.5 from
acl2-doc-emacs.texinfo.
This is documentation for ACL2 Version 3.1
Copyright (C) 2006 University of Texas at Austin
This program is free software; you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program; if not, write to the Free Software
Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
Written by: Matt Kaufmann and J Strother Moore
Department of Computer Sciences
University of Texas at Austin
Austin, TX 78712-1188 U.S.A.
INFO-DIR-SECTION Math
START-INFO-DIR-ENTRY
* acl2: (acl2-doc-emacs.info). Applicative Common Lisp
END-INFO-DIR-ENTRY
File: acl2-doc-emacs.info, Node: Numbers in ACL2, Next: On the Naming of Subgoals, Prev: Nontautological Subgoals, Up: Pages Written Especially for the Tours
Numbers in ACL2 Numbers in ACL2
The numbers in ACL2 can be partitioned into the following subtypes:
Rationals
Integers
Positive integers 3
Zero 0
Negative Integers -3
Non-Integral Rationals
Positive Non-Integral Rationals 19/3
Negative Non-Integral Rationals -22/7
Complex Rational Numbers #c(3 5/2) ; = 3+(5/2)i
Signed integer constants are usually written (as illustrated above) as
sequences of decimal digits, possibly preceded by + or -. Decimal
points are not allowed. Integers may be written in binary, as in
#b1011 (= 23) and #b-111 (= -7). Octal may also be used, #o-777 =
-511. Non-integral rationals are written as a signed decimal integer
and an unsigned decimal integer, separated by a slash. Complex
rationals are written as #c(rpart ipart) where rpart and ipart are
rationals.
Of course, 4/2 = 2/1 = 2 (i.e., not every rational written with a slash
is a non-integer). Similarly, #c(4/2 0) = #c(2 0) = 2.
The common arithmetic functions and relations are denoted by +, -, *,
/, =, <, <=, > and >=. However there are many others, e.g., floor,
ceiling, and lognot. We suggest you see *note PROGRAMMING:: <> where
we list all of the primitive ACL2 functions. Alternatively, see any
Common Lisp language documentation.
The primitive predicates for recognizing numbers are illustrated
below. The following ACL2 function will classify an object, x,
according to its numeric subtype, or else return 'NaN (not a number).
We show it this way just to illustrate programming in ACL2.
(defun classify-number (x)
(cond ((rationalp x)
(cond ((integerp x)
(cond ((< 0 x) 'positive-integer)
((= 0 x) 'zero)
(t 'negative-integer)))
((< 0 x) 'positive-non-integral-rational)
(t 'negative-non-integral-rational)))
((complex-rationalp x) 'complex-rational)
(t 'NaN)))
File: acl2-doc-emacs.info, Node: On the Naming of Subgoals, Next: Other Requirements, Prev: Numbers in ACL2, Up: Pages Written Especially for the Tours
On the Naming of Subgoals On the Naming of Subgoals
Subgoal *1/2 is the induction step from the scheme, obtained by
instantiating the scheme with our conjecture.
We number the cases "backward", so this is case "2" of the proof of
"*1". We number them backward so you can look at a subgoal number and
get an estimate for how close you are to the end.
File: acl2-doc-emacs.info, Node: Other Requirements, Next: Overview of the Expansion of ENDP in the Base Case, Prev: On the Naming of Subgoals, Up: Pages Written Especially for the Tours
Other Requirements Other Requirements
ACL2 is distributed on the Web without fee.
There is a License agreement, which is available via the ACL2 Home Page
link below.
ACL2 currently runs on Unix, Linux, Windows, and Macintosh operating
systems.
It can be built in any of the following Common Lisps:
* Allegro,
* GCL (Gnu Common Lisp),
* Lispworks,
* CLISP,
* CMU Common Lisp,
* SBCL,
* OpenMCL, and
* MCL (Macintosh Common Lisp).
Flying Tour: *note The End of the Flying Tour::
File: acl2-doc-emacs.info, Node: Overview of the Expansion of ENDP in the Base Case, Next: Overview of the Expansion of ENDP in the Induction Step, Prev: Other Requirements, Up: Pages Written Especially for the Tours
Overview of the Expansion of ENDP in the Base Case Overview of the Expansion of ENDP in the Base Case
Subgoal *1/1 is the Base Case of our induction. It simplifies to
Subgoal *1/1' by expanding the ENDP term in the hypothesis, just as we
saw in the earlier proof of Subgoal *1/2.
File: acl2-doc-emacs.info, Node: Overview of the Expansion of ENDP in the Induction Step, Next: Overview of the Final Simplification in the Base Case, Prev: Overview of the Expansion of ENDP in the Base Case, Up: Pages Written Especially for the Tours
Overview of the Expansion of ENDP in the Induction Step Overview of the Expansion of ENDP in the Induction Step
In this message the system is saying that Subgoal *1/2 has been
rewritten to the Subgoal *1/2', by expanding the definition of endp.
This is an example of simplification, one of the main proof techniques
used by the theorem prover.
See *Note The Expansion of ENDP in the Induction Step (Step 0):: if you
would like to step through the simplification of Subgoal *1/2.
File: acl2-doc-emacs.info, Node: Overview of the Final Simplification in the Base Case, Next: Overview of the Proof of a Trivial Consequence, Prev: Overview of the Expansion of ENDP in the Induction Step, Up: Pages Written Especially for the Tours
Overview of the Final Simplification in the Base Case Overview of the Final Simplification in the Base Case
The But is our signal that the goal is proved.
See *Note The Final Simplification in the Base Case (Step 0):: to step
through the proof. It is very simple.
File: acl2-doc-emacs.info, Node: Overview of the Proof of a Trivial Consequence, Next: Overview of the Simplification of the Base Case to T, Prev: Overview of the Final Simplification in the Base Case, Up: Pages Written Especially for the Tours
Overview of the Proof of a Trivial Consequence Overview of the Proof of a Trivial Consequence
ACL2 !>(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))))))
ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...): The previously
added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE
rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a
more general target. Because the new rule will be tried first, it
may nonetheless find application.
By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture
to
Goal'
(EQUAL (APP X1
(APP X2
(APP X3 (APP X4 (APP X5 (APP X6 X7))))))
(APP X1
(APP X2
(APP X3 (APP X4 (APP X5 (APP X6 X7))))))).
But we reduce the conjecture to T, by primitive type reasoning.
Q.E.D.
Summary
Form: ( DEFTHM TRIVIAL-CONSEQUENCE ...)
Rules: ((:REWRITE ASSOCIATIVITY-OF-APP)
(:FAKE-RUNE-FOR-TYPE-SET NIL))
Warnings: Subsume
Time: 0.20 seconds (prove: 0.02, print: 0.00, other: 0.18)
TRIVIAL-CONSEQUENCE
You might explore the links before moving on.
Walking Tour: *note The End of the Walking Tour::
File: acl2-doc-emacs.info, Node: Overview of the Simplification of the Base Case to T, Next: Overview of the Simplification of the Induction Conclusion, Prev: Overview of the Proof of a Trivial Consequence, Up: Pages Written Especially for the Tours
Overview of the Simplification of the Base Case to T Overview of the Simplification of the Base Case to T
Subgoal *1/1
(IMPLIES (ENDP A)
(EQUAL (APP (APP A B) C)
(APP A (APP B C)))).
By the simple :definition ENDP we reduce the conjecture to
Subgoal *1/1'
(IMPLIES (NOT (CONSP A))
(EQUAL (APP (APP A B) C)
(APP A (APP B C)))).
But simplification reduces this to T, using the :definition APP and
primitive type reasoning.
Walking Tour: *note The End of the Proof of the Associativity of App::
File: acl2-doc-emacs.info, Node: Overview of the Simplification of the Induction Conclusion, Next: Overview of the Simplification of the Induction Step to T, Prev: Overview of the Simplification of the Base Case to T, Up: Pages Written Especially for the Tours
Overview of the Simplification of the Induction Conclusion Overview of the Simplification of the Induction Conclusion
In this message the system is saying that Subgoal *1/2' has been
rewritten T using the rules noted. The word "But" at the beginning of
the sentence is a signal that the goal has been proved.
See *Note The Simplification of the Induction Conclusion (Step 0):: to
step through the proof of Subgoal *1/2'.
File: acl2-doc-emacs.info, Node: Overview of the Simplification of the Induction Step to T, Next: Perhaps, Prev: Overview of the Simplification of the Induction Conclusion, Up: Pages Written Especially for the Tours
Overview of the Simplification of the Induction Step to T Overview of the Simplification of the Induction Step to T
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)))).
By the simple :definition ENDP we reduce the conjecture to
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)))).
But simplification reduces this to T, using the :definition APP, the
:rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning.
Walking Tour: *note Overview of the Simplification of the Base Case to
T::
File: acl2-doc-emacs.info, Node: Perhaps, Next: Popping out of an Inductive Proof, Prev: Overview of the Simplification of the Induction Step to T, Up: Pages Written Especially for the Tours
Perhaps Perhaps
The theorem prover's proof is printed in real time. At the time it
prints "Perhaps" it does not know the proof will succeed.
File: acl2-doc-emacs.info, Node: Popping out of an Inductive Proof, Next: Proving Theorems about Models, Prev: Perhaps, Up: Pages Written Especially for the Tours
Popping out of an Inductive Proof Popping out of an Inductive Proof
Recall that our induction scheme (see *note The Proof of the
Associativity of App:: to revisit it) had two cases, the induction step
(Subgoal *1/2) and the base case (Subgoal *1/1). Both have been proved!
File: acl2-doc-emacs.info, Node: Proving Theorems about Models, Next: Revisiting the Admission of App, Prev: Popping out of an Inductive Proof, Up: Pages Written Especially for the Tours
Proving Theorems about Models Proving Theorems about Models
But ACL2 is a logic. We can prove theorems about the model.
Theorem. MC 'mult is a multiplier
(implies (and (natp x)
(natp y))
(equal (lookup 'z (mc (s 'mult x y) (mclk x)))
(* x y))).
This theorem says that a certain program running on the mc machine will
correctly multiply any two natural numbers.
It is a statement about an infinite number of test cases!
We know it is true about the model because we proved it.
Flying Tour: *note What is Required of the User(Q)::
File: acl2-doc-emacs.info, Node: Revisiting the Admission of App, Next: Rewrite Rules are Generated from DEFTHM Events, Prev: Proving Theorems about Models, Up: Pages Written Especially for the Tours
Revisiting the Admission of App Revisiting the Admission of App
Here is the definition of app again with certain parts highlighted. If
you are taking the Walking Tour, please read the text carefully and
click on each of the links below, except those marked <>. Then come
back here.
ACL2 !>(defun app (x y)
(cond ((endp x) y)
(t (cons (car x)
(app (cdr x) y)))))
The admission of APP is trivial, using the
relation O< <> (which is known to be well-founded on
the domain recognized by O-P <>) and the measure
(ACL2-COUNT <> X). We observe that the
type of APP is described by the theorem (OR
(CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive type
reasoning.
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
Walking Tour: *note Evaluating App on Sample Input::
File: acl2-doc-emacs.info, Node: Rewrite Rules are Generated from DEFTHM Events, Next: Running Models, Prev: Revisiting the Admission of App, Up: Pages Written Especially for the Tours
Rewrite Rules are Generated from DEFTHM Events Rewrite Rules are Generated from DEFTHM Events
By reading the documentation of defthm <> (and especially of its
:rule-classes <> argument) you would learn that when we submitted the
command
(defthm associativity-of-app
(equal (app (app a b) c)
(app a (app b c))))
we not only command the system to prove that app is an associative
function but
* we commanded it to use that fact as a rewrite rule.
That means that every time the system encounters a term of the form
(app (app x y) z)
it will replace it with
(app x (app y z))!
Walking Tour: *note You Must Think about the Use of a Formula as a
Rule::
File: acl2-doc-emacs.info, Node: Running Models, Next: Subsumption of Induction Candidates in App Example, Prev: Rewrite Rules are Generated from DEFTHM Events, Up: Pages Written Especially for the Tours
Running Models Running Models
Suppose the machine being modeled is some kind of arithmetic unit.
Suppose the model can be initialized so as to multiply x times y and
leave the answer in z. Then if we initialize s to multiply with x=5
and y=7 and run the machine long enough, we can read the answer 35 in
the final state.
Because ACL2 is a programming language, our model can be run or
executed.
If you defined the model in ACL2 and then typed
> (lookup 'z (mc (s 'mult 5 7) 29))
then ACL2 would compute 35. You can emulate or test the model of your
machine.
This is obvious because ACL2 is Common Lisp; and Common Lisp is a
programming language.
Flying Tour: *note Symbolic Execution of Models::
File: acl2-doc-emacs.info, Node: Subsumption of Induction Candidates in App Example, Next: Suggested Inductions in the Associativity of App Example, Prev: Running Models, Up: Pages Written Especially for the Tours
Subsumption of Induction Candidates in App Example Subsumption of Induction Candidates in App Example
After collecting induction suggestions from these three terms
(app a b)
(app b c)
(app a (app b c))
the system notices that the first and last suggest the same
decomposition of a. So we are left with two ideas about how to induct:
Decompose a as we would to unwind (app a b).
Decompose b as we would to unwind (app b c).
File: acl2-doc-emacs.info, Node: Suggested Inductions in the Associativity of App Example, Next: Symbolic Execution of Models, Prev: Subsumption of Induction Candidates in App Example, Up: Pages Written Especially for the Tours
Suggested Inductions in the Associativity of App Example Suggested Inductions in the Associativity of App Example
To find a plausible induction argument, the system studies the
recursions exhibited by the terms in the conjecture.
Roughly speaking, a call of a recursive function "suggests" an
induction if the argument position decomposed in recursion is occupied
by a variable.
In this conjecture, three terms suggest inductions:
(app a b)
(app b c)
(app a (app b c))
The variable recursively decomposed is indicated in bold.
File: acl2-doc-emacs.info, Node: Symbolic Execution of Models, Next: The Admission of App, Prev: Suggested Inductions in the Associativity of App Example, Up: Pages Written Especially for the Tours
Symbolic Execution of Models Symbolic Execution of Models
But ACL2 is more than a programming language.
Initialize x to 5 and let y be any legal value.
Because ACL2 is a mathematical language, we can simplify the expression
(lookup 'z (mc (s 'mult 5 y) 29))
and get (+ y y y y y). This is symbolic execution because not all of
the parameters are known.
Flying Tour: *note Proving Theorems about Models::
File: acl2-doc-emacs.info, Node: The Admission of App, Next: The Associativity of App, Prev: Symbolic Execution of Models, Up: Pages Written Especially for the Tours
The Admission of App The Admission of App
Here is what it looks like to submit the definition of app to ACL2:
ACL2 !>(defun app (x y)
(cond ((endp x) y)
(t (cons (car x)
(app (cdr x) y)))))
The admission of APP is trivial, using the relation O< (which
is known to be well-founded on the domain recognized by O-P)
and the measure (ACL2-COUNT X). We observe that the type of APP is
described by the theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)).
We used primitive type reasoning.
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 text between the lines above is one interaction with the ACL2
command loop.
Above you see the user's input and how the system responds. This
little example shows you what the syntax looks like and is a very
typical successful interaction with the definitional principle.
Let's look at it a little more closely.
Walking Tour: *note Revisiting the Admission of App::
File: acl2-doc-emacs.info, Node: The Associativity of App, Next: The Base Case in the App Example, Prev: The Admission of App, Up: Pages Written Especially for the Tours
The Associativity of App The Associativity of App
ACL2!>(let ((a '(1 2))
(b '(3 4))
(c '(5 6)))
(equal (app (app a b) c)
(app a (app b c))))
T
Observe that, for the particular a, b, and c above, (app (app a b) c)
returns the same thing as (app a (app b c)). Perhaps app is
associative. Of course, to be associative means that the above
property must hold for all values of a, b, and c, not just the ones
tested above.
Wouldn't it be cool if you could type
ACL2!>(equal (app (app a b) c)
(app a (app b c)))
and have ACL2 compute the value T? Well, you can't! If you try it,
you'll get an error message! The message says we can't evaluate that
form because it contains free variables, i.e., variables not given
values. See *Note Free Variables in Top-Level Input:: to see the
message.
We cannot evaluate a form on an infinite number of cases. But we can
prove that a form is a theorem and hence know that it will always
evaluate to true.
Walking Tour: *note The Theorem that App is Associative::
File: acl2-doc-emacs.info, Node: The Base Case in the App Example, Next: The End of the Flying Tour, Prev: The Associativity of App, Up: Pages Written Especially for the Tours
The Base Case in the App Example The Base Case in the App Example
This formula is the Base Case. It consists of two parts, a test
identifying the non-inductive case and the conjecture to prove.
(IMPLIES (ENDP A) ; Test
(:P A B C)) ; Conjecture
When we prove this we can assume
* A is empty
and we have to prove the conjecture for A.
File: acl2-doc-emacs.info, Node: The End of the Flying Tour, Next: The End of the Proof of the Associativity of App, Prev: The Base Case in the App Example, Up: Pages Written Especially for the Tours
The End of the Flying Tour The End of the Flying Tour
This completes the Flying Tour.
You may wish now to go back and revisit selected nodes of the Flying
Tour so that you can explore some of the branches not on the Tour. You
can do so via The Flight Plan. These branches mainly provide some
background and motivational material, rather than details of ACL2.
If you would like to learn more about ACL2 itself, we recommend that
you now take the walking Tour. You may do so by clicking on the
Walking Tour icon below.
Thanks.
Matt Kaufmann and J Moore
Walking Tour: *note A Walking Tour of ACL2::
File: acl2-doc-emacs.info, Node: The End of the Proof of the Associativity of App, Next: The End of the Walking Tour, Prev: The End of the Flying Tour, Up: Pages Written Especially for the Tours
The End of the Proof of the Associativity of App The End of the Proof of the Associativity of App
That completes the proof of *1.
Q.E.D.
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
Walking Tour: *note Guiding the ACL2 Theorem Prover::
File: acl2-doc-emacs.info, Node: The End of the Walking Tour, Next: The Event Summary, Prev: The End of the Proof of the Associativity of App, Up: Pages Written Especially for the Tours
The End of the Walking Tour The End of the Walking Tour
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 *note 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
File: acl2-doc-emacs.info, Node: The Event Summary, Next: The Expansion of ENDP in the Induction Step (Step 0), Prev: The End of the Walking Tour, Up: Pages Written Especially for the Tours
The Event Summary The Event Summary
At the conclusion of most events (see *note About the Prompt:: for a
brief discussion of events or see *note 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 *note RUNE::) <>)
which are list-structured 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
*Note LD-POST-EVAL-PRINT:: <> for some details. If you really want to
follow that link, however, you might see *note LD:: <> first.
You should now return to the Walking Tour.
File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 0), Next: The Expansion of ENDP in the Induction Step (Step 1), Prev: The Event Summary, Up: Pages Written Especially for the Tours
The Expansion of ENDP in the Induction Step (Step 0) The Expansion of ENDP in the Induction Step (Step 0)
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.
File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 1), Next: The Expansion of ENDP in the Induction Step (Step 2), Prev: The Expansion of ENDP in the Induction Step (Step 0), Up: Pages Written Especially for the Tours
The Expansion of ENDP in the Induction Step (Step 1) The Expansion of ENDP in the Induction Step (Step 1)
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)))
File: acl2-doc-emacs.info, Node: The Expansion of ENDP in the Induction Step (Step 2), Next: The Falling Body Model, Prev: The Expansion of ENDP in the Induction Step (Step 1), Up: Pages Written Especially for the Tours
The Expansion of ENDP in the Induction Step (Step 2) The Expansion of ENDP in the Induction Step (Step 2)
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 see *note Overview of the Simplification of the Induction Step
to T:: to return to the main proof.
File: acl2-doc-emacs.info, Node: The Falling Body Model, Next: The Final Simplification in the Base Case (Step 0), Prev: The Expansion of ENDP in the Induction Step (Step 2), Up: Pages Written Especially for the Tours
The Falling Body Model The Falling Body Model
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.
See *Note Corroborating Models:: to continue
File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 0), Next: The Final Simplification in the Base Case (Step 1), Prev: The Falling Body Model, Up: Pages Written Especially for the Tours
The Final Simplification in the Base Case (Step 0) the Final Simplification in the Base Case (Step 0)
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.
File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 1), Next: The Final Simplification in the Base Case (Step 2), Prev: The Final Simplification in the Base Case (Step 0), Up: Pages Written Especially for the Tours
The Final Simplification in the Base Case (Step 1) the Final Simplification in the Base Case (Step 1)
Subgoal *1/1'
(IMPLIES (NOT (CONSP A))
(EQUAL (APP B C)
(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.
File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 2), Next: The Final Simplification in the Base Case (Step 3), Prev: The Final Simplification in the Base Case (Step 1), Up: Pages Written Especially for the Tours
The Final Simplification in the Base Case (Step 2) the Final Simplification in the Base Case (Step 2)
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
File: acl2-doc-emacs.info, Node: The Final Simplification in the Base Case (Step 3), Next: The First Application of the Associativity Rule, Prev: The Final Simplification in the Base Case (Step 2), Up: Pages Written Especially for the Tours
The Final Simplification in the Base Case (Step 3) the Final Simplification in the Base Case (Step 3)
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 see *note Overview of the Simplification of the Base Case to
T:: to return to the main proof.
File: acl2-doc-emacs.info, Node: The First Application of the Associativity Rule, Next: The Induction Scheme Selected for the App Example, Prev: The Final Simplification in the Base Case (Step 3), Up: Pages Written Especially for the Tours
The First Application of the Associativity Rule The First Application of the Associativity Rule
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)))))
File: acl2-doc-emacs.info, Node: The Induction Scheme Selected for the App Example, Next: The Induction Step in the App Example, Prev: The First Application of the Associativity Rule, Up: Pages Written Especially for the Tours
The Induction Scheme Selected for the App Example The Induction Scheme Selected for the App Example
(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.
File: acl2-doc-emacs.info, Node: The Induction Step in the App Example, Next: The Instantiation of the Induction Scheme, Prev: The Induction Scheme Selected for the App Example, Up: Pages Written Especially for the Tours
The Induction Step in the App Example The Induction Step in the App Example
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)) ; Test
(:P (CDR A) B C)) ; Induction Hypothesis
(:P A B C)) ; Induction Conclusion
When we prove this we can assume
* 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.
File: acl2-doc-emacs.info, Node: The Instantiation of the Induction Scheme, Next: The Justification of the Induction Scheme, Prev: The Induction Step in the App Example, Up: Pages Written Especially for the Tours
The Instantiation of the Induction Scheme The Instantiation of the Induction Scheme
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.
File: acl2-doc-emacs.info, Node: The Justification of the Induction Scheme, Next: The Proof of the Associativity of App, Prev: The Instantiation of the Induction Scheme, Up: Pages Written Especially for the Tours
The Justification of the Induction Scheme The Justification of the Induction Scheme
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.
File: acl2-doc-emacs.info, Node: The Proof of the Associativity of App, Next: The Q.E.D. Message, Prev: The Justification of the Induction Scheme, Up: Pages Written Especially for the Tours
The Proof of the Associativity of App The Proof of the Associativity of App
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
O< (which is known to be well-founded on the domain recognized
by O-P). When applied to the goal at hand the above induction
scheme produces the following two nontautological subgoals.
Walking Tour: *note Overview of the Simplification of the Induction
Step to T::
File: acl2-doc-emacs.info, Node: The Q.E.D. Message, Next: The Rules used in the Associativity of App Proof, Prev: The Proof of the Associativity of App, Up: Pages Written Especially for the Tours
The Q.E.D. Message The Q.E.D. Message
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.
File: acl2-doc-emacs.info, Node: The Rules used in the Associativity of App Proof, Next: The Simplification of the Induction Conclusion (Step 0), Prev: The Q.E.D. Message, Up: Pages Written Especially for the Tours
The Rules used in the Associativity of App Proof The Rules used in the Associativity of App Proof
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 0), Next: The Simplification of the Induction Conclusion (Step 1), Prev: The Rules used in the Associativity of App Proof, Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 0) the Simplification of the Induction Conclusion (Step 0)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 1), Next: The Simplification of the Induction Conclusion (Step 10), Prev: The Simplification of the Induction Conclusion (Step 0), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 1) the Simplification of the Induction Conclusion (Step 1)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 10), Next: The Simplification of the Induction Conclusion (Step 11), Prev: The Simplification of the Induction Conclusion (Step 1), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 10) the Simplification of the Induction Conclusion (Step 10)
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).
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 11), Next: The Simplification of the Induction Conclusion (Step 12), Prev: The Simplification of the Induction Conclusion (Step 10), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 11) the Simplification of the Induction Conclusion (Step 11)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 12), Next: The Simplification of the Induction Conclusion (Step 2), Prev: The Simplification of the Induction Conclusion (Step 11), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 12) the Simplification of the Induction Conclusion (Step 12)
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 see *note Overview of the Simplification of the Induction Step
to T:: to return to the main proof.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 2), Next: The Simplification of the Induction Conclusion (Step 3), Prev: The Simplification of the Induction Conclusion (Step 12), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 2) the Simplification of the Induction Conclusion (Step 2)
Subgoal *1/2'
(IMPLIES (AND (CONSP A)
(EQUAL (APP (APP (CDR A) B) C)
(APP (CDR A) (APP B C))))
(EQUAL (APP (IF T
(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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 3), Next: The Simplification of the Induction Conclusion (Step 4), Prev: The Simplification of the Induction Conclusion (Step 2), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 3) the Simplification of the Induction Conclusion (Step 3)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 4), Next: The Simplification of the Induction Conclusion (Step 5), Prev: The Simplification of the Induction Conclusion (Step 3), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 4) the Simplification of the Induction Conclusion (Step 4)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 5), Next: The Simplification of the Induction Conclusion (Step 6), Prev: The Simplification of the Induction Conclusion (Step 4), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 5) the Simplification of the Induction Conclusion (Step 5)
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 (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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 6), Next: The Simplification of the Induction Conclusion (Step 7), Prev: The Simplification of the Induction Conclusion (Step 5), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 6) the Simplification of the Induction Conclusion (Step 6)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 7), Next: The Simplification of the Induction Conclusion (Step 8), Prev: The Simplification of the Induction Conclusion (Step 6), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 7) the Simplification of the Induction Conclusion (Step 7)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 8), Next: The Simplification of the Induction Conclusion (Step 9), Prev: The Simplification of the Induction Conclusion (Step 7), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 8) the Simplification of the Induction Conclusion (Step 8)
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.
File: acl2-doc-emacs.info, Node: The Simplification of the Induction Conclusion (Step 9), Next: The Summary of the Proof of the Trivial Consequence, Prev: The Simplification of the Induction Conclusion (Step 8), Up: Pages Written Especially for the Tours
The Simplification of the Induction Conclusion (Step 9) the Simplification of the Induction Conclusion (Step 9)
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)).
File: acl2-doc-emacs.info, Node: The Summary of the Proof of the Trivial Consequence, Next: The Theorem that App is Associative, Prev: The Simplification of the Induction Conclusion (Step 9), Up: Pages Written Especially for the Tours
The Summary of the Proof of the Trivial Consequence The Summary of the Proof of the Trivial Consequence
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.
File: acl2-doc-emacs.info, Node: The Theorem that App is Associative, Next: The Time Taken to do the Associativity of App Proof, Prev: The Summary of the Proof of the Trivial Consequence, Up: Pages Written Especially for the Tours
The Theorem that App is Associative The Theorem that App is Associative
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.
Walking Tour: *note The Proof of the Associativity of App::
File: acl2-doc-emacs.info, Node: The Time Taken to do the Associativity of App Proof, Next: The Tours, Prev: The Theorem that App is Associative, Up: Pages Written Especially for the Tours
The Time Taken to do the Associativity of App Proof The Time Taken to do the Associativity of App Proof
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.