; ACL2 Proofs -- Lesson 3
; 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.
;; This lesson is motivated by the following event which FAILS in
;; ACL2. (Fire up ACL2 and try it!)
#|
(defun
ack ( x y )
(declare (xargs :guard (and (integerp x)
(>= x 0)
(integerp y)
(>= y 0))))
(if (zp x)
(+ y 1)
(if (zp y)
(ack (- x 1) 1)
(ack (- x 1)
(ack x (- y 1))))))
|#
;; The problem is that ACL2 cannot prove that the function terminates
;; on all inputs. ACL2 says how to fix the problem: Specify a :MEASURE.
;; 1. Link to the ACL2 User Manual. Read the ACL2 documentation about DEFUN.
;; Pay attention to the discussion of termination requirement for
;; admissibility of functions.
;; 2. The most commonly used measure function is acl2-count, which computes a
;; nonnegative integer size for all ACL2 objects. Read about ACL2-COUNT.
;; 3. Read about E0-ORDINALP, E0-ORD-<, and PROOF-OF-WELL-FOUNDEDNESS.
;; We follow the suggestion of ACL2 and supply a :MEASURE which allows
;; ACL2 to prove the function terminates on all inputs.
;; (Fire up ACL2 and try it!)
#|
(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))))
(if (zp x)
(+ y 1)
(if (zp y)
(ack (- x 1) 1)
(ack (- x 1)
(ack x (- y 1))))))
|#
;; However, the event still FAILS, this time because ACL2 cannot
;; prove that the guard is true on each recursive call to the
;; function. We overcome this temporarily by telling ACL2 not
;; to verify that the guard holds on recursive calls. Read about
;; GUARDs in the documentation.
(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))))))
;; We now verify that the guard is true on each recursive call
;; in the definition by proving that (ack x y) always returns
;; a nonnegative integer.
(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)
;; Read about VERIFY-GUARDS.
;; Read about TYPE-PRESCRIPTION.
;; Finally we prove a theorem about the function we worked so hard
;; to have ACL2 accept:
(defthm
theorem
(implies (and (integerp y)
(>= y 0))
(< y (ack x y))))