; ACL2 Proofs -- Lesson 4
; 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 the function ack (for
;; Ackermann's function) studied in ACL2 Proofs -- Lesson 3.
;; By the way DO NOT try to evaluate ack for any but very small values of
;; x and y. The integer value of (ack 4 4) is estimated to have more
;; decimal digits than there are protons, neutrons, and electrons in the
;; universe.
;; 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)
(defthm
Theorem
(implies (and (integerp y)
(>= y 0))
(< y (ack x y))))
;; ACL2 uses induction to prove the following.
(thm
(implies (and (integerp y)
(>= y 0))
(< (ack x y)
(ack x (+ 1 y)))))
;; Read about THM.
;; A simple human proof, not using induction, can be based on an instance
;; of Theorem.
;; Theorem: y < (ack x y)
;; Instance: (ack x y) < (ack x-1 (ack x y)) = (ack x y+1)
;; That is, in Theorem, replace y with (ack x y) and replace x with x-1.
;; Try to get ACL2 to ``discover'' this simple proof.
;; First we use a HINT to tell ACL2 NOT to use induction.
;; Try to use ACL2 to prove the following event:
;; (It will FAIL.)
(defthm
monotony-2nd-arg-ack
(implies (and (integerp y)
(>= y 0))
(< (ack x y)
(ack x (+ 1 y))))
:HINTS (("Goal"
:DO-NOT-INDUCT T)))
;; ACL2 completely misses the simple instance of Theorem, so we add to
;; the HINTS to draw ACL2's attention to the instance. Try this in ACL2:
(defthm
monotony-2nd-arg-ack
(implies (and (integerp y)
(>= y 0))
(< (ack x y)
(ack x (+ 1 y))))
:HINTS (("Goal"
:do-not-induct t
:USE ((:INSTANCE
Theorem
(x (- x 1))
(y (ack x y))))
:IN-THEORY (DISABLE Theorem))))
;; Read about DEFTHM, HINTS, and DISABLE in the ACL2 documentation.