{ "cells": [ { "cell_type": "markdown", "metadata": {}, "source": [ "# A Walking Tour of ACL2\n", "\n", "> COMMENT: This notebook is written in [ACL2 Kernel](https://github.com/tani/acl2-kernel) by TANIGUCHI Masaya, and copied from [A Walking Tour of ACL2](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____A_02Walking_02Tour_02of_02ACL2). The license of original text is described at the end of this note book.\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/large-walking.gif)\n", "\n", "On this tour you will learn a little more about the ACL2 logic, the theorem prover, and the user interface.\n", "\n", "This time we will stick with really simple things, such as the associativity of list concatenation.\n", "\n", "We assume you have taken the Flying Tour but that you did not necessarily follow all the “off-tour” links because we encouraged you not to. With the Walking Tour we encourage you to visit off-tour links — provided they are not marked with the tiny warning sign (\\*). But they are “branches” in the tour that lead to “dead ends.” When you reach a dead end, remember to use your browser’s Back Button to return to the Walking Tour to continue.\n", "\n", "When you get to the end of the tour we’ll give you a chance to repeat quickly both the Flying and the Walking Tours to visit any off-tour links still of interest.\n", "\n", "\n", "## Common Lisp\n", "\n", "![Common Lisp](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/common-lisp.gif)\n", "\n", "The logic of ACL2 is based on Common Lisp.\n", "\n", "Common Lisp is the standard list processing programming language. It is documented in: Guy L. Steele, [Common Lisp The Language](https://www.cs.cmu.edu/Groups/AI/html/cltl/cltl2.html), Digital Press, 12 Crosby Drive, Bedford, MA 01730, 1990.\n", "\n", "ACL2 formalizes only a subset of Common Lisp. It includes such familiar Lisp functions as cons, car and cdr for creating and manipulating list structures, various arithmetic primitives such as `+`, `*`, expt and `<=`, and intern and `symbol-name` for creating and manipulating symbols. Control primitives include `cond`, `case` and `if`, as well as function call, including recursion. New functions are defined with `defun` and macros with `defmacro`. See [programming](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____PROGRAMMING)\\* for a list of the Common Lisp primitives supported by ACL2.\n", "\n", "ACL2 supports five of Common Lisp’s datatypes:\n", "\n", "* the precisely represented, unbounded numbers (integers, rationals, and the complex numbers with rational components, called the “complex rationals” here),\n", "\n", "* the characters with ASCII codes between 0 and 255\n", "\n", "* strings of such characters\n", "\n", "* symbols (including packages)\n", "\n", "* conses\n", "\n", "ACL2 is a very small subset of full Common Lisp. ACL2 does not include the Common Lisp Object System (CLOS), higher order functions, circular structures, and other aspects of Common Lisp that are **non-applicative**. Roughly speaking, a language is applicative if it follows the rules of function application. For example, `f(x)` must be equal to `f(x)`, which means, among other things, that the value of `f` must not be affected by “global variables” and the object `x` must not change over time.\n", "\n", "## An Example Common Lisp Function Definition\n", "\n", "Consider the binary trees `x` and `y` below.\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/binary-trees-x-y.gif)\n", "\n", "In Lisp, `x` is written as the list `'(A B)` or, equivalently, as `'(A B . NIL)`. Similarly, `y` may be written `'(C D E)`. Suppose we wish to replace the right-most tip of `x` by the entire tree `y`. This is denoted `(app x y)`, where `app` stands for \"append\".\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/binary-trees-app.gif)\n", "\n", "We can define `app` with:\n", "\n", "```lisp\n", "(defun app (x y) ; Concatenate x and y. \n", " (declare (type (satisfies true-listp) x)); We expect x to end in NIL. \n", " (cond ((endp x) y) ; If x is empty, return y. \n", " (t (cons (car x) ; Else, copy first node \n", " (app (cdr x) y))))) ; and recur into next. \n", "```\n", "\n", "If you defined this function in some Common Lisp, then to run app the `x` and `y` above you could then type\n", "\n", "```lisp\n", "(app '(A B) '(C D E))\n", "```\n", "\n", "and Common Lisp will print the `(A B C D E)`.\n", "\n", "\n", "## An Example of ACL2 in Use\n", "\n", "To introduce you to ACL2 we will consider the app function discussed in the Common Lisp page, **except** we will omit for the moment the **declare** form, which in ACL2 is called a **guard**.\n", "\n", "Guards are arbitrary ACL2 terms that express the “intended domain” of functions. In that sense, guards are akin to type signatures. However, Common Lisp and ACL2 are untyped programming languages: while the language supports several different data types and the types of objects can be determined by predicates at runtime, any type of object may be passed to any function. Thus, guards are “extra-logical.” Recognizing both the practical and intellectual value of knowing that your functions are applied to the kinds of objects you intend, ACL2 imposes guards on Common Lisp and provides a means of proving that functions are used as intended. But the story is necessarily complicated and we do not recommend it to the new user. Get used to the fact that any ACL2 function may be applied to any objects and program accordingly. Read about guards later.\n", "\n", "Here is the definition again\n", "\n", "```lisp\n", "(defun app (x y) \n", " (cond ((endp x) y) \n", " (t (cons (car x) \n", " (app (cdr x) y))))) \n", "```\n", "\n", "The next few stops along the Walking Tour will show you\n", "\n", "The next few stops along the Walking Tour will show you\n", "\n", "- how to use the ACL2 documentation,\n", "- what happens when the above definition is submitted to ACL2,\n", "- what happens when you evaluate calls of `app`,\n", "- what one simple theorem about `app` looks like,\n", "- how ACL2 proves the theorem, and\n", "- how that theorem can be used in another proof.\n", "\n", "Along the way we will talk about the **definitional principle**, **types**, the ACL2 **read-eval-print loop**, and how the **theorem prover** works.\n", "\n", "When we complete this part of the tour we will return briefly to the notion of **guard** and revisit several of the topics above in that context.\n", "\n", "## How To Find Out about ACL2 Functions\n", "\n", "Most ACL2 primitives are documented. Here is the definition of `app` again, with the documented topics higlighted. \\* All of the links below lead into the ACL2 User's Manual. So follow these links if you with, but use your Back Button to return here!\n", "\n", "\n", "```lisp\n", "(defun app (x y) \n", " (cond ((endp x) y) \n", " (t (cons (car x) \n", " (app (cdr x) y))))) \n", "```\n", "\n", "By following the link on [`endp`\\*](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=COMMON-LISP____ENDP) we see that it is a Common Lisp function and is defined to be the same as [`atom`\\*](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=COMMON-LISP____ATOM), which recognizes non-conses. But `endp` has a guard. Since we are ignoring guards for now, we'll ignore the guard issue on `endp`.\n", "\n", "So this definition reads \"to `app x` and `y`: if `x` is an atom, return `y`; otherwise, `app (cdr x)` and `y` and then cons `(car x)` onto that.\"\n", "\n", "## How To Find Out about ACL2 Functions (cont)\n", "\n", "The ACL2 documentation is also available in Emacs, via the ACL2-Doc browser (see [ACL2-Doc](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____ACL2-DOC))\\* , allowing you to explore the hyperlinked documentation in the comfort of a text editor that can also interact with ACL2.\n", "\n", "In addition, runtime images of ACL2 have the hyperlinked text as a large ACL2 data structure that can be explored with ACL2’s `:doc` command. If you have ACL2 running, try the command `:doc endp`.\n", "\n", "Another way to find out about ACL2 functions, if you have an ACL2 image available, is to use the command [`:args`\\*](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____ARGS) which prints the formals, type, and guard of a function symbol.\n", "\n", "Of course, the ACL2 documentation can also be printed out as a very long book but we do not recommend that! See the ACL2 Home Page to download the Postscript.\n", "\n", "## The admission of App\n", "\n", "Now let’s continue with `app`." ] }, { "cell_type": "code", "execution_count": 1, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\r\n", "The admission of APP is trivial, using the relation O< (which is known\r\n", "to be well-founded on the domain recognized by O-P) and the measure\r\n", "(ACL2-COUNT X). We observe that the type of APP is described by the\r\n", "theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive\r\n", "type reasoning.\r\n", "\r\n", "Summary\r\n", "Form: ( DEFUN APP ...)\r\n", "Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))\r\n", "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n", " APP\r\n" ] } ], "source": [ "(defun app (x y) \n", " (cond ((endp x) y) \n", " (t (cons (car x) \n", " (app (cdr x) y))))) " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The text between the lines above is one interaction with the ACL2 command loop. Interacting with the latest version of ACL2 may not produce the very same output, but we trust you’ll recognize the basics.\n", "\n", "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.\n", "\n", "Let’s look at it a little more closely.\n", "\n", "## Revisiting the Admission of App\n", "\n", "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.\n", "\n", "```lisp\n", "ACL2 !> (defun app (x y) \n", " (cond ((endp x) y) \n", " (t (cons (car x) \n", " (app (cdr x) y))))) \n", "\n", "The admission of APP is trivial, using the relation O< (which is known\n", "to be well-founded on the domain recognized by O-P) and the measure\n", "(ACL2-COUNT X). We observe that the type of APP is described by the\n", "theorem (OR (CONSP (APP X Y)) (EQUAL (APP X Y) Y)). We used primitive\n", "type reasoning.\n", "\n", "Summary\n", "Form: ( DEFUN APP ...)\n", "Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))\n", "Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)\n", " APP\n", "```\n", "\n", "> COMMENT: As I could not add link to code blocks, I listed links you need to visit.\n", "> - [addmission](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____About_02the_02Admission_02of_02Recursive_02Definitions)\n", "> - [o<](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____O_C3)\\*\n", "> - [o-p](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____O-P)\\*\n", "> - [ACL2-count](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____ACL2-COUNT)\\*\n", "> - [observe](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Guessing_02the_02Type_02of_02a_02Newly_02Admitted_02Function)\n", "> - [type](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____About_02Types)\n", "\n", "## Evaluating App on Sample Input" ] }, { "cell_type": "code", "execution_count": 2, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(X Y Z)\r\n" ] } ], "source": [ "(app nil '(x y z))" ] }, { "cell_type": "code", "execution_count": 3, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(1 2 3 4 5 6 7)\r\n" ] } ], "source": [ "(app '(1 2 3) '(4 5 6 7)) " ] }, { "cell_type": "code", "execution_count": 4, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(A B C D E F G X Y Z)\r\n" ] } ], "source": [ "(app '(a b c d e f g) '(x y z)) \n", "; click http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Conversion for an explanation" ] }, { "cell_type": "code", "execution_count": 5, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(1 2 3 4 5 6)\r\n" ] } ], "source": [ "(app (app '(1 2) '(3 4)) '(5 6))" ] }, { "cell_type": "code", "execution_count": 6, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "(1 2 3 4 5 6)\r\n" ] } ], "source": [ "(app '(1 2) (app '(3 4) '(5 6))) " ] }, { "cell_type": "code", "execution_count": 7, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "T\r\n" ] } ], "source": [ "(let ((a '(1 2)) \n", " (b '(3 4)) \n", " (c '(5 6))) \n", " (equal (app (app a b) c) \n", " (app a (app b c)))) " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "As we can see from these examples, ACL2 functions can be executed more or less as Common Lisp.\n", "\n", "The last three examples suggest an interesting property of `app`\n", "\n", "## The Associativity of App\n", "\n", "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.\n", "\n", "Wouldn't it be cool if you could type" ] }, { "cell_type": "code", "execution_count": 9, "metadata": { "scrolled": true }, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\r\n", "\r\n", "ACL2 Error in TOP-LEVEL: Global variables, such as A, B and C, are\r\n", "not allowed. See :DOC ASSIGN and :DOC @.\r\n", "\r\n" ] } ], "source": [ "(equal (app (app a b) c) \n", " (app a (app b c))) " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "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. Click [here](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Free_02Variables_02in_02Top-Level_02Input) to see the message.\n", "\n", "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.\n", "\n", "## The Theorem that App is Associative" ] }, { "cell_type": "code", "execution_count": 10, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\r\n", "*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.\r\n", "\r\n", "Perhaps we can prove *1 by induction. Three induction schemes are\r\n", "suggested by this conjecture. Subsumption reduces that number to two.\r\n", "However, one of these is flawed and so we are left with one viable\r\n", "candidate. \r\n", "\r\n", "We will induct according to a scheme suggested by (APP A B). This\r\n", "suggestion was produced using the :induction rule APP. If we let (:P A B C)\r\n", "denote *1 above then the induction scheme we'll use is\r\n", "(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C))\r\n", " (:P A B C))\r\n", " (IMPLIES (ENDP A) (:P A B C))).\r\n", "This induction is justified by the same argument used to admit APP.\r\n", "When applied to the goal at hand the above induction scheme produces\r\n", "two nontautological subgoals.\r\n", "Subgoal *1/2\r\n", "Subgoal *1/2'\r\n", "Subgoal *1/1\r\n", "Subgoal *1/1'\r\n", "\r\n", "*1 is COMPLETED!\r\n", "Thus key checkpoint Goal is COMPLETED!\r\n", "\r\n", "Q.E.D.\r\n", "\r\n", "Summary\r\n", "Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...)\r\n", "Rules: ((:DEFINITION APP)\r\n", " (:DEFINITION ENDP)\r\n", " (:DEFINITION NOT)\r\n", " (:FAKE-RUNE-FOR-TYPE-SET NIL)\r\n", " (:INDUCTION APP)\r\n", " (:REWRITE CAR-CONS)\r\n", " (:REWRITE CDR-CONS))\r\n", "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n", "Prover steps counted: 435\r\n", " ASSOCIATIVITY-OF-APP\r\n" ] } ], "source": [ "(defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c))))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "The formula above says `app` is associative. The [`defthm`](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____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 database as a [`rewrite`](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____REWRITE)\\* rule, but we won’t go into that just yet.\n", "\n", "What we will consider is how the ACL2 theorem prover proves this formula.\n", "\n", "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.\n", "\n", "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.\n", "\n", "## The Proof of the Associativity of App\n", "\n", "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. (The most recent version of ACL2 may print slightly different output but the basics are the same.) Just follow the Walking Tour after exploring the explanations.\n", "\n", "However, before exploring this (defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c))))(defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c))))output you should understand that ACL2 users rarely read successful proofs! Instead, they look at certain subgoals printed in failed proofs, figure whether and how those subgoals can be proved, and give ACL2 directions for proving them, usually by simply proving other lemmas. Furthermore, to be a good user of ACL2 you do not have to understand how the theorem prover works. You just have to understand how to interact with it. We explain this in great detail later. But basically all new users are curious to know how ACL2 works and this little tour attempts to give some answers, just to satisfy your curiosity.\n", "\n", "```lisp\n", "ACL2 !> (defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c))))\n", "\n", "*1 (the initial Goal, a key checkpoint) is pushed for proof by induction.\n", "\n", "Perhaps we can prove *1 by induction. Three induction schemes are\n", "suggested by this conjecture. Subsumption reduces that number to two.\n", "However, one of these is flawed and so we are left with one viable\n", "candidate. \n", "\n", "We will induct according to a scheme suggested by (APP A B). This\n", "suggestion was produced using the :induction rule APP. If we let (:P A B C)\n", "denote *1 above then the induction scheme we'll use is\n", "(AND (IMPLIES (AND (NOT (ENDP A)) (:P (CDR A) B C))\n", " (:P A B C))\n", " (IMPLIES (ENDP A) (:P A B C))).\n", "This induction is justified by the same argument used to admit APP.\n", "When applied to the goal at hand the above induction scheme produces\n", "two nontautological subgoals.\n", "\n", "Subgoal *1/2 \n", "(IMPLIES (AND (NOT (ENDP A)) \n", " (EQUAL (APP (APP (CDR A) B) C) \n", " (APP (CDR A) (APP B C)))) \n", " (EQUAL (APP (APP A B) C) \n", " (APP A (APP B C)))). \n", " \n", "By the simple :definition ENDP we reduce the conjecture to \n", " \n", "Subgoal *1/2' \n", "(IMPLIES (AND (CONSP A) \n", " (EQUAL (APP (APP (CDR A) B) C) \n", " (APP (CDR A) (APP B C)))) \n", " (EQUAL (APP (APP A B) C) \n", " (APP A (APP B C)))). \n", " \n", "But simplification reduces this to T, using the :definition APP, the \n", ":rewrite rules CDR-CONS and CAR-CONS and primitive type reasoning. \n", "\n", "Subgoal *1/1 \n", "(IMPLIES (ENDP A) \n", " (EQUAL (APP (APP A B) C) \n", " (APP A (APP B C)))). \n", " \n", "By the simple :definition ENDP we reduce the conjecture to \n", " \n", "Subgoal *1/1' \n", "(IMPLIES (NOT (CONSP A)) \n", " (EQUAL (APP (APP A B) C) \n", " (APP A (APP B C)))). \n", " \n", "But simplification reduces this to T, using the :definition APP and \n", "primitive type reasoning. \n", "*1 is COMPLETED!\n", "Thus key checkpoint Goal is COMPLETED!\n", "\n", "Q.E.D.\n", "\n", "Summary\n", "Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...)\n", "Rules: ((:DEFINITION APP)\n", " (:DEFINITION ENDP)\n", " (:DEFINITION NOT)\n", " (:FAKE-RUNE-FOR-TYPE-SET NIL)\n", " (:INDUCTION APP)\n", " (:REWRITE CAR-CONS)\n", " (:REWRITE CDR-CONS))\n", "Time: 0.01 seconds (prove: 0.01, print: 0.00, other: 0.00)\n", "Prover steps counted: 435\n", " ASSOCIATIVITY-OF-APP\n", "```\n", "\n", "> COMMENT: As I could not add link to code blocks, I listed links you need to visit.\n", "> - [\\*1](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Name_02the_02Formula_02Above)\n", "> - [Perhaps](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Perhaps)\n", "> - [Subsumption](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Subsumption_02of_02Induction_02Candidates_02in_02App_02Example)\n", "> - [flawed](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Flawed_02Induction_02Candidates_02in_02App_02Example)\n", "> - [justified](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Justification_02of_02the_02Induction_02Scheme)\n", "> - [applied](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Instantiation_02of_02the_02Induction_02Scheme)\n", "> - [nontautological subgoals](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Nontautological_02Subgoals)\n", "> - [Subgoal \\*1/2](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____On_02the_02Naming_02of_02Subgoals)\n", "> - [ENDP](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Overview_02of_02the_02Expansion_02of_02ENDP_02in_02the_02Induction_02Step)\n", "> - [Subgoal \\*1/1](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Overview_02of_02the_02Expansion_02of_02ENDP_02in_02the_02Base_02Case)\n", "> - [But](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Overview_02of_02the_02Final_02Simplification_02in_02the_02Base_02Case)\n", "> - [completes](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____Popping_02out_02of_02an_02Inductive_02Proof)\n", "> - [Q.E.D.](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Q.E.D._02Message)\n", "> - [Rules](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Rules_02used_02in_02the_02Associativity_02of_02App_02Proof)\n", "> - [0.01](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Time_02Taken_02to_02do_02the_02Associativity_02of_02App_02Proof)\n", "\n", "## Guiding the ACL2 Theorem Prover\n", "\n", "Now that you have seen the theorem prover in action you might be curious as to how you guide it.\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/interactive-theorem-prover.gif)\n", "\n", "Look at the picture above. It is meant to suggest that *Q* is an important lemma needed for the proof *P*. Note that to lead the prover to the proof of *P* the user first proves *Q*. In a way, the formulation and proof of *Q* is a hint to the prover about how to prove *P*.\n", "\n", "The user usually doesn't think of *Q* or recognize the need to prove it separately until he or she sees the theorem prover **fail** to prove *P* wihout it \"knowing\" *Q*.\n", "\n", "The way the user typically discovers the need for *Q* is to look at failed proofs.\n", "\n", "## ACL2 as an Interactive Theorem Prover (cont)\n", "\n", "When ACL2 proves a lemma, it is converted into one or more **rules** and stored in a **database**. The theorem prover is **rule-driven**. By proving lemmas you can configure ACL2 to behave in certain ways when it is trying to prove formulas in a certain problem domain. The expert user can make ACL2 do amazingly \"smart\" looking things.\n", "\n", "But it would be wrong to think that ACL2 *knows* the mathematical content of formula just because it has proved it. What ACL2 knows — all ACL2 knows — is what is encoded in its rules. There are many types of rules (see [rule-classes](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____RULE-CLASSES)\\*)\n", "\n", "Many formuals can be effectively coded as rules. But by the same token, it is possible to encode a formula as a rule that is so ineffective it cannot even prove itself!\n", "\n", "The way a formula is stored as a rule is entirely up to the user. That is, **you** determine how ACL2 should use each formula that it proves.\n", "\n", "The most common kind of rule is the **rewrite rule**. It is so common that if you don't tell ACL2 how to store a formula, it stores it as a rewrite rule.\n", "\n", "## ACL2 System Archtecture\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/acl2-system-architecture.gif)\n", "\n", "The user interacts with the theorem prover by giving it definitions, theorems and advice. Most often the advice is about how to store each proved theorem as a rule. Sometimes the advice is about how to prove a specific theorem.\n", "\n", "The databese consists of all the rules ACL2 \"knows.\" It is possible to include in the database all of the rules in some certified file of other events. Such certified files are called [books](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____BOOKS)\\*.\n", "\n", "Interesting proofs are usually built on top of many boks, some of which are written especially for that problem domain and others of which are about oft--used domains, like arithmetic or list processing. ACL2's distribution includes many books written by users. See the \"books\" link under the **Lemma Libraries and Utilities**\\* link tof the ACL2 home page.\n", "\n", "## Rewrite Rules are Generated from DEFTHM Events\n", "\n", "By reading the documentation of [`defthm`](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____DEFTHM)\\* (and especially of its [`:rule-classes`](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____RULE-CLASSES)\\* argument) you would lean that when we submitted the command\n", "\n", "```lisp\n", "(defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c)))) \n", "```\n", "\n", "We not only command the system to prove that `app` is an associative function but\n", "\n", "> \\* we commanded it to use that fact as a rewrite rule. \n", "\n", "That means that every time the system encounters a term of the form\n", "\n", "```lisp\n", "(app (app x y) z)\n", "```\n", "\n", "it will replace it with\n", "\n", "```lisp\n", "(app x (app y z))\n", "```\n", "\n", "## You Must Think about the Use of a Formula as a Rule\n", "\n", "This is **good** and **bad**.\n", "\n", "The good news is that you can **program** ACL2's simplifier.\n", "\n", "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**!\n", "\n", "For example, if after proving `associativity-of-app` as previously shown, you engaged in the mathematically trivial act of proving it again but with the equality reversed, you would have programmed ACL2's rewriter to loop forever.\n", "\n", "You can avoid adding any rule by using the command;" ] }, { "cell_type": "code", "execution_count": 11, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\r\n", "\r\n", "ACL2 Error in ( DEFTHM ASSOCIATIVITY-OF-APP ...): The name \r\n", "ASSOCIATIVITY-OF-APP is in use as a theorem. The redefinition feature\r\n", "is currently off. See :DOC ld-redefinition-action.\r\n", "\r\n", "\r\n", "Note: ASSOCIATIVITY-OF-APP was previously defined at the top level.\r\n", "\r\n", "\r\n", "Summary\r\n", "Form: ( DEFTHM ASSOCIATIVITY-OF-APP ...)\r\n", "Rules: NIL\r\n", "Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)\r\n", "\r\n", "ACL2 Error in ( DEFTHM ASSOCIATIVITY-OF-APP ...): See :DOC failure.\r\n", "\r\n", "******** FAILED ********\r\n" ] } ], "source": [ "(defthm associativity-of-app \n", " (equal (app (app a b) c) \n", " (app a (app b c))) \n", " :rule-classes nil) " ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "## Using the Associativity of App to Prove a Trivial Consequence\n", "\n", "If we have proved the associativity-of-app rule, then the following theorem is trivial:" ] }, { "cell_type": "code", "execution_count": 12, "metadata": {}, "outputs": [ { "name": "stdout", "output_type": "stream", "text": [ "\r\n", "ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...): The previously\r\n", "added rule ASSOCIATIVITY-OF-APP subsumes a newly proposed :REWRITE\r\n", "rule generated from TRIVIAL-CONSEQUENCE, in the sense that the old\r\n", "rule rewrites a more general target. Because the new rule will be\r\n", "tried first, it may nonetheless find application.\r\n", "\r\n", "\r\n", "Q.E.D.\r\n", "\r\n", "Summary\r\n", "Form: ( DEFTHM TRIVIAL-CONSEQUENCE ...)\r\n", "Rules: ((:REWRITE ASSOCIATIVITY-OF-APP))\r\n", "Warnings: Subsume\r\n", "Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)\r\n", "Prover steps counted: 82\r\n", " TRIVIAL-CONSEQUENCE\r\n" ] } ], "source": [ "(defthm trivial-consequence\n", " (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7)\n", " (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7))))))" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "Below we show the proof\n", "\n", "```lisp\n", "ACL2 !>(defthm trivial-consequence \n", " (equal (app (app (app (app x1 x2) (app x3 x4)) (app x5 x6)) x7) \n", " (app x1 (app (app x2 x3) (app (app x4 x5) (app x6 x7)))))) \n", " \n", "ACL2 Warning [Subsume] in ( DEFTHM TRIVIAL-CONSEQUENCE ...): The previously \n", "added rule ASSOCIATIVITY-OF-APP subsumes the newly proposed :REWRITE \n", "rule TRIVIAL-CONSEQUENCE, in the sense that the old rule rewrites a \n", "more general target. Because the new rule will be tried first, it \n", "may nonetheless find application. \n", " \n", "By the simple :rewrite rule ASSOCIATIVITY-OF-APP we reduce the conjecture \n", "to \n", " \n", "Goal' \n", "(EQUAL (APP X1 \n", " (APP X2 \n", " (APP X3 (APP X4 (APP X5 (APP X6 X7)))))) \n", " (APP X1 \n", " (APP X2 \n", " (APP X3 (APP X4 (APP X5 (APP X6 X7))))))). \n", " \n", "But we reduce the conjecture to T, by primitive type reasoning. \n", " \n", "Q.E.D. \n", " \n", "Summary \n", "Form: ( DEFTHM TRIVIAL-CONSEQUENCE ...) \n", "Rules: ((:REWRITE ASSOCIATIVITY-OF-APP) \n", " (:FAKE-RUNE-FOR-TYPE-SET NIL)) \n", "Warnings: Subsume \n", "Time: 0.20 seconds (prove: 0.02, print: 0.00, other: 0.18) \n", " TRIVIAL-CONSEQUENCE \n", "```\n", "\n", "> COMMENT: As I could not add link to code blocks, I listed links you need to visit.\n", "> - [ACL2 Warning](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02WARNING_02about_02the_02Trivial_02Consequence)\n", "> - [ASSOCIATIVITY-OF-APP](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02First_02Application_02of_02the_02Associativity_02Rule)\n", "> - [Subsume](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____The_02Summary_02of_02the_02Proof_02of_02the_02Trivial_02Consequence)\n", "\n", "You might explore the links before moving on.\n", "\n", "## The End of the Walking Tour\n", "\n", "![](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/res/tours/sitting.gif)\n", "\n", "The completes the Walking Tour.\n", "\n", "We intend to document many other parts of the system this way, but we just haven't gotten around to it.\n", "\n", "To start the two tours over again from the beginning, click on the icons below. If you are really interested in learning how to use ACL2, we recommend that you repeat each tour at least once more to explore branches of the tour that you might have missed.\n", "\n", "If you want to learn how to use the theorem prover, we now recommend that you devote the time necessary to work your way through the extended introduction to how to use the prover.\n", "\n", "See [introduction-to-the-theorem-prover](http://www.cs.utexas.edu/users/moore/acl2/v8-3/combined-manual/index.html?topic=ACL2____INTRODUCTION-TO-THE-THEOREM-PROVER).\n", "\n", "This will explain how to interact with ACL2 and has some sample problems for you to solve including some challenge proofs to make ACL2 find.\n", "\n", "We hope you enjoy ACL2. We do.\n", "\n", "Matt Kaufmann and J Strother Moore" ] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# Appendix: Playground\n", "\n", "The Jupyter provides an interactive programming environment. You can run ACL2 code in below cells. Try to review this tour!" ] }, { "cell_type": "code", "execution_count": null, "metadata": {}, "outputs": [], "source": [] }, { "cell_type": "markdown", "metadata": {}, "source": [ "# License\n", "\n", "```\n", "[Note: The license below is based on the template found July 25, 2014\n", " at: http://opensource.org/licenses/BSD-3-Clause. Except as\n", " otherwise noted, it applies to all files distributed from\n", " http://www.cs.utexas.edu/users/moore/acl2/current/,\n", " as well as to all files distributed from\n", " https://github.com/acl2/acl2 other than those in the\n", " ACL2 Community Books (the books/ subdirectory).\n", "```\n", "\n", "When a file in the ACL2 Community Books refers to this LICENSE, that file's\n", "specified copyright supersedes the copyright shown immediately below.]\n", "\n", "Copyright (c) 2020, Regents of the University of Texas\n", "All rights reserved.\n", "\n", "Redistribution and use in source and binary forms, with or without\n", "modification, are permitted provided that the following conditions are\n", "met:\n", "\n", "- Redistributions of source code must retain the above copyright\n", " notice, this list of conditions and the following disclaimer.\n", "\n", "- Redistributions in binary form must reproduce the above copyright\n", " notice, this list of conditions and the following disclaimer in the\n", " documentation and/or other materials provided with the distribution.\n", "\n", "- Neither the name of the copyright holder nor the names of\n", " its contributors may be used to endorse or promote products derived\n", " from this software without specific prior written permission.\n", "\n", "THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS\n", "\"AS IS\" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT\n", "LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR\n", "A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT\n", "HOLDER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,\n", "SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT\n", "LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,\n", "DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY\n", "THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT\n", "(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE\n", "OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE." ] } ], "metadata": { "kernelspec": { "display_name": "ACL2", "language": "acl2", "name": "acl2" }, "language_info": { "codemirror_mode": "lisp", "file_extension": ".lisp", "mimetype": "text/x-lisp", "name": "acl2" } }, "nbformat": 4, "nbformat_minor": 4 }