; ACL2 Proofs -- Lesson 5
; Copyright (C) 2004 John R. Cowles, University of Wyoming
; 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: John R. Cowles
; email: cowles@uwyo.edu
; Department of Computer Science
; University of Wyoming
; Laramie, WY 82071 U.S.A.
;; In this lesson we continue with the study of Ackermann's function
;; that was studied in ACL2 Proofs -- Lesson 3 and ACL2 Proofs -- Lesson 4
;; ACL2 should readily accept the following events without error.
; Tell ACL2 the location of the arithmetic book on the hives:
:set-cbd "/home/acl2/acl2-2.7/acl2-sources/books/arithmetic/"
(include-book "top")
(defun
ack ( x y )
(declare (xargs :guard (and (integerp x)
(integerp y)
(>= x 0)
(>= y 0))
:measure (cons (+ 1 (acl2-count x))
(acl2-count y))
:verify-guards nil))
(if (zp x)
(+ y 1)
(if (zp y)
(ack (- x 1) 1)
(ack (- x 1) (ack x (- y 1))))))
(defthm
non-neg-int-ack
(implies (and (integerp y)
(>= y 0))
(and (integerp (ack x y))
(>= (ack x y) 0)))
:rule-classes :type-prescription)
(verify-guards ack)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Try to use ACL2 to prove the following event:
;; (It will FAIL.)
(defthm
ack-at-x=1
(implies (and (integerp y)
(>= y 0))
(equal (ack 1 y)
(+ 2 y))))
;; ACL2 wants to prove this event by induction, but has trouble
;; deciding on an induction scheme. Therefore, we suggest that ACL2
;; use the usual mathematical induction scheme on the nonnegative
;; integers. We do this in a slightly roundabout way because ACL2
;; always chooses induction schemes by looking at the recursive
;; definitions of the functions involved in the statement of the
;; proposed theorem. The only recursively defined function in the
;; theorem is ACK and its recursive definition does not generate
;; an induction scheme that can be used in a proof of the theorem.
;; In order to tell ACL2 about other induction schemes, a recursive
;; function must be defined using the recursion corresponding to
;; the inductive scheme: We need a function that is defined on the
;; nonnegative integers with a base step saying what to do with 0
;; and an induction step saying what to do with n based on what was
;; done to n-1. Any such function will do; one that we know about
;; is the factorial function.
(defun
fact (n)
(declare (xargs :guard (and (integerp n)
(>= n 0))))
(if (zp n)
1
(* n (fact (- n 1)))))
;; We use HINTS to tell ACL2 to use the induction scheme suggested
;; by the definition of fact.
(defthm
ack-at-x=1
(implies (and (integerp y)
(>= y 0))
(equal (ack 1 y)
(+ 2 y)))
:hints (("Goal"
:INDUCT (fact y))))
;; Here is another fact about ack for ACL2 to prove:
(defthm
ack-at-x=2
(implies (and (integerp y)
(>= y 0))
(equal (ack 2 y)
(+ 3 (* 2 y))))
:hints (("Goal"
:induct (fact y))))
;; Read about the :INDUCT hint under the topic HINTS in the ACL2
;; documentation.