;;; mccarthy-91.lisp
;;; Admissibility of an iterative version of McCarthy's 91 function.
;;; Created: 6-6-2000 Last revised: 2-8-00
;;;============================================================================

;;; To certify this book:

#|
;**** WARNING ****
; Due to a bug in version 2.5, a useful meta rule in multiset.lisp is not 
; applied where needed in this book. There is no such problem in Version
; 2.4 

; To fix this problem in version 2.5, the file patch-meta.lisp has to be 
; loaded before certification (thanks to Matt Kaufmann for sending us
; the patch): 

(value :q)

(load "../../patch-meta.lisp")
;********

(in-package "ACL2")



(certify-book "mccarthy-91")



|#

(in-package "ACL2")

(include-book "../../defmul")

(set-verify-guards-eagerness 2)


;;;****************************************************************************
;;; USING MULTISETS RELATIONS TO PROVE TERMINATION OF McCARTHY'S 91 FUNCTION
;;;****************************************************************************


;;; ===========================================================================
;;; 1. Admission of an iterative version of McCarthy 91 function.
;;; ===========================================================================

;;; Instead of defining the following definition of McCarthy's 91 function:

; (defun mc (x)
;   (declare (xargs :mode :program))
;   (if (> x 100)
;       (- x 10)
;       (mc (mc (+ x 11))))) 

;;; Our goal is to define in ACL2 the following iterative version:

; (defun mc-aux (n z)
;   (declare (xargs :measure ...
; 		    :well-founded-relation ...))
;   (cond ((or (zp n) (not (integerp z))) z)
; 	((> z 100) (mc-aux (- n 1) (- z 10)))
; 	(t (mc-aux (+ n 1) (+ z 11)))))

; (defun mc-it (x)
;   (mc-aux 1 x))

;;; We will replay the proof of Dershowitz & Manna in "Proving
;;; termination with multiset orderings"

;;; ---------------------------------------------------------------------------
;;; 1.1 A well-founded relation rel-mc
;;; ---------------------------------------------------------------------------

;;; The measures:
(defun integerp-<=-111 (x)
  (and (integerp x) (<= x 111)))

;;; REMARK : There is a mistake in the proof by D&M, because they say
;;; that the domain is 0 <= x < 111.

;;; The relation:
(defun rel-mc (x y)
  (and (integerp-<=-111 x)
       (integerp-<=-111 y)
       (< y x)))

;;; The embedding:
(defun fn-rel-mc (x)
  (if (integerp-<=-111 x)
      (- 111 x)
      0))

;;; The well-foundedness theorem:
(defthm rel-mc-well-founded
  (and (e0-ordinalp (fn-rel-mc x))
       (implies (rel-mc x y)
		(e0-ord-< (fn-rel-mc x) (fn-rel-mc y))))
  :rule-classes :well-founded-relation)

;;; REMARK: One could think that integerp-<=-111 is the MP property of the
;;; well-founded relation, instead of T. But there is a subtle difference: our
;;; measure (our multisets) can contain elements greater than 111, although
;;; those elements are not comparable.

;;; ---------------------------------------------------------------------------
;;; 1.2 Extension of rel-mc to mul-rel-mc (well founded).
;;;----------------------------------------------------------------------------

;;; (defmul-components rel-mc)
; => The list of components is: 
;     (REL-MC REL-MC-WELL-FOUNDED T FN-REL-MC X Y)

(defmul (REL-MC REL-MC-WELL-FOUNDED T FN-REL-MC X Y) :verify-guards t)

;;;----------------------------------------------------------------------------
;;; 1.3 Definition of a measure in order to accept mc-aux.
;;;----------------------------------------------------------------------------

(defun f91 (x)
  (cond ((not (integerp x)) x)
	((> x 100) (- x 10))
	(t 91)))

(defun measure-mc-aux (n z)
  (declare (xargs :guard (and (integerp n) (>= n 0))))
  (if (zp n)
      nil
      (cons z (measure-mc-aux (- n 1) (f91 z)))))

;;;----------------------------------------------------------------------------
;;; 1.4 Definition of "mc-aux".
;;;----------------------------------------------------------------------------

;;; Fundamental rewrite rule for our proof strategy:
;;; The rule measure-mc-aux-expand expands measure-mc-aux where the
;;; expansion heuristics of the system fail. This is important for two
;;; reasons. First, measure-mc-aux definition is expanded whenever it
;;; can be deduced that n>0, and the multiset obtained explicitly
;;; present the first (and second sometimes) elements and the same tail,
;;; allowing the meta rule of multiset.lisp to rewrite. Second, the IF
;;; in the rule performs almost the same case distinction as in the hand
;;; proof. 

(defthm measure-mc-aux-expand
  (implies (and (not (zp n)) (integerp z))
	   (equal (measure-mc-aux n z)
		  (cons z (measure-mc-aux (- n 1)
					  (if (> z 100) (- z 10) 91))))))

;;; The next theorem comes from the "equalities" book 
;;; ("../distribution/books/arithmetic/equalities.lisp"). It's the only event
;;; from this book needed in the admission of "mc-aux".

(defthm fold-consts-in-+
  (implies (and (syntaxp (quotep x))
		(syntaxp (quotep y)))
	   (equal (+ x (+ y z))
		  (+ (+ x y) z))))

(in-theory (disable multiset-diff))

;;; At last:

(defun mc-aux (n z)
  (declare (xargs 
	    :guard (and (integerp n) (>= n 0))
	    :measure (measure-mc-aux n z)
	    :well-founded-relation mul-rel-mc))
  (cond ((or (zp n) (not (integerp z))) z)
	((> z 100) (mc-aux (- n 1) (- z 10)))
	(t (mc-aux (+ n 1) (+ z 11)))))

(defun mc-it (x)
  (mc-aux 1 x))


;;; ============================================================================
;;; 2. Properties of mc-it
;;; ============================================================================


;;; ----------------------------------------------------------------------------
;;; 2.1 mc-it is equal to f91
;;; ----------------------------------------------------------------------------


(defun iter-f91 (n x)
  (declare (xargs :guard (and (integerp n) (>= n 0))))
  (if (zp n)
      x
      (iter-f91 (- n 1) (f91 x))))

;;; Fundamental rewrite rule for our proof strategy:
				 
(defthm iter-f91-expand
  (implies (and (not (zp n)) (integerp z))
	   (equal (iter-f91 n z)
		  (iter-f91 (- n 1)
			    (if (> z 100) (- z 10) 91))))) 
		  
(defthm iter-f91-mc-aux
  (equal (mc-aux n z) (iter-f91 n z))
  :hints (("Goal" :induct (mc-aux n z))))

(defthm mc-it-equals-f91-for-non-integers
  (implies (not (integerp x))
	   (equal (iter-f91 n x) x)))

(defthm equal-mc-it-and-f91
  (equal (mc-it x) (f91 x)))


;;; ----------------------------------------------------------------------------
;;; 2.2 mc-it verifies the recursion scheme of mc
;;; ----------------------------------------------------------------------------

(defthm mc-it-recursive-schema
  (equal (mc-it x)
	 (cond ((not (integerp x)) x)
	       ((> x 100) (- x 10))
	       (t (mc-it (mc-it (+ x 11))))))
  :rule-classes nil)


;;; ----------------------------------------------------------------------------
;;; 2.3 Every function satisfying the recursion scheme of mc is equal to f91 
;;; ----------------------------------------------------------------------------



;;; A general function M satisfying the above recursive equation:

(encapsulate 
 ((M (x) t))

 (local (defun M (x) (mc-it x)))

 (defthm M-it-recursive-schema
   (equal (M x)
	  (cond ((not (integerp x)) x)
		((> x 100) (- x 10))
		(t (M (M (+ x 11))))))
   :rule-classes :definition))

(defun iter-M (n x)
  (declare (xargs :guard (and (integerp n) (>= n 0))))
  (if (zp n)
      x
      (iter-M (- n 1) (M x))))

(defthm M-expand
  (implies (and (not (zp n)) (integerp z))
	   (equal (iter-M n z)
		  (iter-M (- n 1)
			  (if (> z 100) (- z 10) (M (M (+ z 11)))))))) 

(defthm iter-M-equals-mc-aux
  (equal (iter-M n z) (mc-aux n z))
  :hints (("Goal" :in-theory (disable iter-f91-mc-aux))))

;;; Then M is equal to f91

(encapsulate
 ()
 
 (local
  (defthm iter-M-1-M
    (equal (M x) (iter-M 1 x))
    :hints (("Goal" :in-theory (disable iter-M-equals-mc-aux)
	     :expand (iter-M 1 x)))))
 
 (defthm M-equal-f91
   (equal (M x) (f91 x))))