''. They lead out of
this linear tutorial and into ACL2's hypertext reference manual. We
recommend that you not visit any of these advanced links until you have
read the entire tutorial at least once.Major Section: ACL2-TUTORIAL
Software is complex, and ACL2 is a piece of software that is used to analyze software -- adding another layer of complexity. Furthermore, instead of being limited to static analysis for certain fixed properties, ACL2 allows you -- indeed, forces you -- to formalize the problem and the questions. It ``knows'' nothing inherent about your problem before you start to interact with it. But it can be used to help answer the most complicated questions you can ask about software.
All this is to say that it is not the kind of tool that you just install and then start to use effectively. So OK, you've installed it or confirmed that you can invoke it. Good for you. Now you have to learn how to use it! Your success ultimately comes down to your understanding of your problem domain and your appropriate exploitation of ACL2's strengths and avoidance of its weaknesses. So put aside the idea of sitting down and interacting with it. Instead, learn about it.
We assume you know some of the industrial applications of ACL2. Realizing that such things can be done may sustain you during the long learning curve! We also assume you have taken both the Flying Tour and the Walking Tour. The tours give you a good overview of the whole system where this tutorial focuses on how to use the prover itself.
If you haven't visited these links, please do so now.
This tutorial will take you several hours -- maybe several days -- to work through. Do not breeze through it as you might a blog. Think your way through it. Remember what you read. Do not take short cuts. If you start to use ACL2 before you really know how, it will only frustrate you.
We recommend that you read this tutorial with an HTML browser so that you can see which links you've followed and which you have not. To give you a sense of what is in store, here is a map of this document. But don't navigate through it from here! Read it linearly, following the links when the text directs you to.
INTRODUCTION-TO-THE-THEOREM-PROVER
INTRODUCTION-TO-REWRITE-RULES-PART-1
SPECIAL-CASES-FOR-REWRITE-RULES
EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES
INTRODUCTION-TO-KEY-CHECKPOINTS
DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS
GENERALIZING-KEY-CHECKPOINTS
POST-INDUCTION-KEY-CHECKPOINTS
INTRODUCTION-TO-REWRITE-RULES-PART-2
STRONG-REWRITE-RULES
PRACTICE-FORMULATING-STRONG-RULES
PRACTICE-FORMULATING-STRONG-RULES-1
PRACTICE-FORMULATING-STRONG-RULES-2
PRACTICE-FORMULATING-STRONG-RULES-3
PRACTICE-FORMULATING-STRONG-RULES-4
PRACTICE-FORMULATING-STRONG-RULES-5
PRACTICE-FORMULATING-STRONG-RULES-6
SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES
FURTHER-INFORMATION-ON-REWRITING
INTRODUCTION-TO-THE-DATABASE
INTRODUCTION-TO-HINTS
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS
INTRODUCTORY-CHALLENGES
INTRODUCTORY-CHALLENGE-PROBLEM-1
INTRODUCTORY-CHALLENGE-PROBLEM-2
INTRODUCTORY-CHALLENGE-PROBLEM-3
(there are others but at least do a few)
FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS
If any of the links above are marked as ``visited'' by your browser, use
your browser's tools menu to mark all links as unvisited. As you can see,
we really think you'll get the most out of this document if you take it
seriously. As you read, you will see some links to ``advanced'' topics.
These are marked with a tiny warning sign, ``''. They lead out of
this linear tutorial and into ACL2's hypertext reference manual. We
recommend that you not visit any of these advanced links until you have
read the entire tutorial at least once.
After you finish this tutorial material, we recommend that you look at the ACL2 Demos, at the ``Demos'' link of the ACL2 home page, http://www.cs.utexas.edu/users/moore/acl2.
Most users of ACL2 have bought the book
Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, and Moore, Kluwer Academic Publishers, June, 2000
which is available in paperback from Lulu for approximately $20 (as of 2010). See http://www.lulu.com/content/1746161. That book contains hundreds of exercises in programming, proof, and using The Method described here to prove theorems. Solutions to the exercises are online. For more information about the book and a companion one (also available on Lulu) about industrial applications of ACL2, see
http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books
Using ACL2 is akin to having a partner in the theorem proving enterprise. It will do some of the work and you will do some of the work. It can't really be any other way because theorem proving is undecidable. You bring a quirkly, error-prone, creative insight to the problem, and ACL2 brings accuracy, logic, and perserverance.
Here we describe a ``model'' of how the system works and introduce some of the ideas and terminology you'll use repeatedly when interacting with it.
This article is about the theorem prover itself, not the programming language and not the logic. We assume you know enough about the ACL2 programming language that you can define simple functions, run them, and read and write ACL2 constants and terms. For some examples of what we'll take for granted about ACL2 programming, see programming-knowledge-taken-for-granted.
We also assume you know enough about logic to understand, for example, the words we use to talk about formulas and proofs. To see some examples of what we'll take for granted about your knowledge of logic terminology, see logic-knowledge-taken-for-granted.
When you give the theorem prover a goal formula to prove, it tries to prove it by breaking it down into subgoals, each of which must be proved in order to prove the original goal. This breaking apart of the goal is done by various proof techniques built into ACL2. Different proof techniques break the formula apart in different ways. For example, the simplifier rips apart the propositional structure to isolate the various cases and applies rewrite rules to simplify the subterms of the formula, while the induction engine will attempt to break the goal into some base cases and some induction steps.
The theorem prover's behavior is affected by a database of rules derived from axioms, definitions, and previously proved theorems. The database also records the enabled status of each rule; only enabled rules are seen by the prover and you can set the status of a rule. There are many other user-settable switches and parameters affecting the behavior of the prover; you'll learn about some of them later.
You guide the theorem prover most of the time simply by identifying lemmas for it to prove. (A lemma is just a theorem that you think is useful in the proofs of other theorems.)
Why does this guide the theorem prover? Because every time you get the system to prove a theorem, it turns the theorem into a rule (unless you tell it not to) and stores the rule in the database. That changes how the prover behaves subsequently. But you determine the kind of rule ACL2 stores.
To learn to ``drive'' the theorem prover you have to learn how various rules affect the system's behavior and how it turns proved formulas into rules. But before we discuss this, we discuss a more mathematical activity: how do you figure out the lemmas ACL2 will need in order for it to prove interesting theorems? ACL2 can often help you in this activity, if you use it in the right way.
Here is the way we recommend you use ACL2.
The Method.
(1) you present ACL2 with the goal conjecture to prove
(2) typically, it fails to prove it (or you abort its attempt), but it prints some Key Checkpoints
(3) you look at the Key Checkpoints and decide that you know a fact that will help; this tutorial will present some helpful questions to keep in mind
(4) you formalize your knowledge as a formula, along with directions for how ACL2 should turn the formula into a rule; this tutorial will tell you about the most commonly used rule, the rewrite rule
(5) you recursively apply The Method to get ACL2 to prove your formula and to store it as the kind of rule you specified
(6) go to step (1)
Caveat: This approach simply won't work on some theorems! Basically, this is a ``troubleshooting'' approach, where you're letting ACL2 determine the basic strategy and you're just helping with the subgoals. But for some theorems, ACL2's approach will be misguided and no amount of troubleshooting will salvage its strategy. You'll have a sense that this is happening when it happens because the formulas ACL2 presents to you will raise issues that feel irrelevant to you. The basic truth is that if you think a formula is always true there are usually strong intuitive reasons behind your belief. If you were asked to defend your belief, you'd start to explain your reasons and with training you can turn that into a proof. So when ACL2's formulas present you with things you haven't thought of either (a) you'll have an ``Ah ha!'' moment when you realize you hadn't considered that case or (b) you'll realize that ACL2's approach is different from your intuitive ``proof.''
But, surprisingly often, the troubleshooting approach to finding proofs works quite well, especially as you rein in your expectations and develop a sense of what ACL2 can handle on its own. Of course, if you can decompose the proof into a couple of main lemmas before you start, so much the better: write down your sequence of lemmas, thinking about the rules you want them to generate, and get ACL2 to prove each of them before giving it the main theorem. This proof planning approach will gradually become an integral part of your use of The Method.
The only mechanized help we can offer with The Method, aside from the theorem prover itself, are tools to help you manage the stack of subgoals it generates when, in step (5) you recursively apply The Method to a lemma. There are both Emacs and Eclipse tools available.
To use The Method you have to read the Key Checkpoints printed at the very end of failed proof attempts, just after the line that reads:
The key checkpoint goals, below, may help you to debug this failure.Most users do not read the output from successful proofs and do not read the output during a proof -- they just let it stream by as a sort of gestalt meter on the theorem prover's progress or lack thereof. For example, you'll be able to tell it is in a loop and needs to be interrupted.
You will respond to most Key Checkpoints by formulating new lemmas for the system to prove and store as rules designed by you to alter ACL2's behavior so that it proves the Key Checkpoints. You will give each lemma a name and write some formula to express the mathematical idea. You'll command ACL2 to prove it by typing:
(defthm name
formula
...)
In the ``...'' you may provide two other kinds of information:
hints for how to prove formula and directives, called
rule-classes, for how to convert formula into a rule after it has
proved formula. Note that you are in charge of determining
what kind of rule ACL2 generates! There are over a dozen different
types of rules with many opportunities to specialize each type.
But the most common kind of rule you'll want to generate is a rewrite
rule.We recommend that you read the following topics in the following
order, without skipping anything but links into the reference
manual, which are marked by the little warning sign, ``''.
(1) See introduction-to-rewrite-rules-part-1 to read about the use and design of rewrite rules.
(2) See introduction-to-key-checkpoints to see how to use The Method to help you design rules.
(3) See introduction-to-rewrite-rules-part-2 for general guidance on how to turn formulas into effective rules.
(4) See introduction-to-the-database to see how to issue commands that build different kinds of rules and that affect the enabled status of existing rules.
(5) See introduction-to-hints to see how to give the prover hints for how to prove specific theorems or even subgoals of specific proof attempts.
(6) See introduction-to-a-few-system-considerations for a few words about system aspects of interacting with ACL2.
(7) See introductory-challenges for a graduated sequence of good challenge problems for the new user to tackle. Do not skip this section! It is here that you really learn how to use ACL2 -- by using it.
(8) See frequently-asked-questions-by-newcomers for a list of questions that new users frequently ask, answered mainly by providing links into the reference manual. We recommend that you skim through these questions and remember that you can find the answers here later. We are very interested in receiving suggestions for how to improve this FAQ and this tutorial. See the ACL2 home page, specifically the link ``Mailing Lists''.
Please read all of the material cited above (skipping only the
reference-manual links (``'')) before you try to use ACL2 on
problems of your own.
By this point you should have read, at least, the following topics from this tutorial introduction to the theorem prover:
INTRODUCTION-TO-THE-THEOREM-PROVER
INTRODUCTION-TO-REWRITE-RULES-PART-1
SPECIAL-CASES-FOR-REWRITE-RULES
EQUIVALENT-FORMULAS-DIFFERENT-REWRITE-RULES
INTRODUCTION-TO-KEY-CHECKPOINTS
DEALING-WITH-KEY-COMBINATIONS-OF-FUNCTION-SYMBOLS
GENERALIZING-KEY-CHECKPOINTS
POST-INDUCTION-KEY-CHECKPOINTS
INTRODUCTION-TO-REWRITE-RULES-PART-2
STRONG-REWRITE-RULES
PRACTICE-FORMULATING-STRONG-RULES
PRACTICE-FORMULATING-STRONG-RULES-1
PRACTICE-FORMULATING-STRONG-RULES-2
PRACTICE-FORMULATING-STRONG-RULES-3
PRACTICE-FORMULATING-STRONG-RULES-4
PRACTICE-FORMULATING-STRONG-RULES-5
PRACTICE-FORMULATING-STRONG-RULES-6
SPECIFIC-KINDS-OF-FORMULAS-AS-REWRITE-RULES
FURTHER-INFORMATION-ON-REWRITING
INTRODUCTION-TO-THE-DATABASE
INTRODUCTION-TO-HINTS
INTRODUCTION-TO-A-FEW-SYSTEM-CONSIDERATIONS
INTRODUCTORY-CHALLENGES
INTRODUCTORY-CHALLENGE-PROBLEM-1
INTRODUCTORY-CHALLENGE-PROBLEM-2
INTRODUCTORY-CHALLENGE-PROBLEM-3
(there are others but at least do a few)
FREQUENTLY-ASKED-QUESTIONS-BY-NEWCOMERS
We also recommend that you look at the ACL2 Demos, at the ``demos'' link of the ACL2 home page http://www.cs.utexas.edu/users/moore/acl2.
Most users of ACL2 have bought the book
Computer-Aided Reasoning: An Approach, Kaufmann, Manolios, and Moore, Kluwer Academic Publishers, June, 2000
which is available in paperback from Lulu for approximately $20 (as of 2010). See http://www.lulu.com/content/1746161. That book contains hundreds of exercises in programming, proof, and using The Method to prove theorems. Solutions to the exercises are online. For more information about the book and a companion one (also available on Lulu) about industrial applications of ACL2, see
http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html#Books
Thank you for spending the time to get acquainted with the basics of the ACL2 theorem prover. Don't hesitate to send further questions to the ACL2 Help address on the ``Mailing Lists'' link of the ACL2 home page.
End of Tutorial Introduction to the Theorem Prover
Below is a list of all of the topics cited on this page.
rev-rev proof -- Answer to Question 1
rev-rev proof -- Answer to Question 2
rev-rev proof -- Answer to Question 2
(TRUE-LISTP (APPEND (FOO A) (BAR B)))
(TRUE-LISTP (REV (FOO A)))
(MEMBER (FOO A) (APPEND (BAR B) (MUM C)))
(SUBSETP (APPEND (FOO A) (BAR B)) (MUM C))
(SUBSETP (FOO A) (APPEND (BAR B) (MUM C)))
(MEMBER (FOO A) (NATS-BELOW (BAR B)))
