; 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))))