(in-package "ACL2")



;;  definition.lisp
;;  ~~~~~~~~~~~~~~~

;; Author: Sandip Ray
;; Date: Sun Jun 18 13:41:27 2006

;; In this book, we investigate the following question. Suppose we have four
;; functions test, base, recur, and wrap, and we want to define a function f to
;; satisfy the following equation.

;; (f x) = (if (test x) (base x) (wrap x (f (recur x))))

;; I think this form above can count as a general form of a primitive recursive
;; equation. The question is, under what conditions can we admit the equation
;; above in ACL2 (under the normal assumption that f is a new function symbol in
;; the current theory and functions test, base, wrap, and recur are symbols in the
;; theory.

;; Note that the equation cannot be admitted in general. For instance consider the
;; following instantiation:

;; (f x) = (if (equal x 0) nil (cons nil (f (- x 1))))

;; Manolios and Moore in their defpun paper prove that the equation, if admitted
;; to ACL2, would produce inconsistency. So it makes sense to ask under what
;; condition the equation for f can be admitted. 

;; Here we show one such condition, which is pretty general. The condition is the
;; following:

;; Suppose you define the "bounded version" of the function fn as follows:

;; (fn x n) = (if (or (test x) (zp n)) (base x) (wrap x (fn (recur x) (1- n))))

;; Suppose then you show that for every n larger than some function (clock-fn x)
;; the function stabilizes, that is, we know the following:

;; 1. (natp (clock-fn x))
;; 2. (natp n) /\ (n >= (clock-fn x) => (fn x n) = (fn x (+ n 1))

;; Then the above equation can be admitted.

;; Clarification
;; -------------

;; Note that we have proven just that the equation is admissible. We have not
;; proved that the function terminates on all inputs, and thus we do not have an
;; induction principle associated. In fact, in general, f might not terminate. For
;; instance consider (base x) = nil, (recur x) = x, and (wrap x y) = y. Then the
;; equation does not terminate but it essentially boils down to (f x) = (f x). See
;; the historical notes below for a different set of constraints regarding when we
;; can know that the function terminates based on the bounded version, and the
;; sister book 


;; History and Acknowledgements
;; ----------------------------

;; The problem came up in a talk by Vinod Vishwanath on February 28, 2004. Vinod
;; wanted the following. Suppose you want to define a function f, but the
;; termination argument is difficult. What you do, however, is to define a bounded
;; version of f, namely fn, and show that if we have a sufficiently large bound
;; then the recursion terminates. This should (informally) enable you to admit
;; f. J Strother Moore challenged the group to formalize the idea of admitting
;; recursive equations via proving theorems about the bounded version. I answered
;; the challenge on Sat May  8 00:54:56 2004, and the solution is documented in
;; the sister book bounded-definitions.lisp. The formalization I came up with is
;; the following. Consider f as above, and consider the following definition of n
;; recursive calls.

;; (defun recur-n (x n)
;;    (if (test x)
;;        x
;;      (if (zp n) x
;;        (recur-n (recur x) (1- n)))))


;; Suppose we have a function (clock x) such that we know 

;; a. (test (recur-n x (clock-fn x)))
;; b. (natp (clock-fn x))

;; Then we proved that the defining equation for f can be admitted under the
;; definitional principle (that is, an appropriate measure can be found). At that
;; time, I asked J if instead of these conditions (a) and (b) we had the
;; conditions (1) and (2), which are weaker, then whether it is possible to still
;; admit the equation for f. J and I thought about the question but couldn't find
;; an answer although J responded that his gut feeling was that the answer is
;; "yes". Nevertheless I forgot all about it. 

;; On Sun Jun 18 6:41:58 2006, I wanted to look over my notes for old small
;; unfinished work, and rediscovered the problem. I then remembered some of the
;; conversations I had had with Pete Manolios a month or so before, and
;; suddenly saw the proof. I spent two hours or so to formalize the proof in
;; ACL2.

;; Thanks to all the people mentioned in this note.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 1: Assumptions                                             ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; I formalize the assumptions 1 and 2 in the prefatory remarks as an
;; encapsulate. 


(encapsulate
 (((test *) => *)
  ((base *) => *) 
  ((recur *) => *)
  ((wrap * *) => *)
  ((clock-fn *) => *))

 (local (defun test (x) (declare (ignore x)) nil))
 (local (defun base (x) (declare (ignore x)) nil))
 (local (defun recur (x) (declare (ignore x)) nil))
 (local (defun wrap (x y) (declare (ignore x y)) nil))

 (defun fn (x n)
   (declare (xargs :measure (acl2-count n)))
   (if (or (test x) 
           (zp n))
       (base x)
     (wrap x (fn (recur x) (1- n)))))

 (local (defun clock-fn (x) (declare (ignore x)) 0))

 (defthm |fn stabilizes after clock|
   (implies (and (natp n)
                 (>= n (clock-fn x)))
            (equal (fn x (1+ n))
                   (fn x n))))

 (defthm |clock is natp|
   (natp (clock-fn x))
   :rule-classes :type-prescription))


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 2: Definition of Witness                                   ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;


;; We need the notion of a smallest upper bound. Notice that the function clock
;; only says that after clock number of iterations fn stabilizes. But it does
;; not say that it does not stabilize before clock. The function smallest below
;; says that it is the minimum upper bound such that the property
;; holds. [Aside: Whenever I have had something some object with a property
;; exists I have almost always needed to do an analogous argument to show that
;; there is a smallest object with the property, where the smallest is based on
;; some pre-determined total order on the domain of the objects. This is true
;; in particular when we deal with quantification since quantification only
;; guarantees some object but not a minimal object in any sense. I should think
;; about encapsulating this argument in a book so that we only need to
;; instantiate the argument any time we need it. Then again, it's not a
;; difficult argument to make so who cares!]

(defun smallest-clock (x c)
  (if (zp c) 0
    (if (not (equal (fn x c) (fn x (1- c))))
        c
      (smallest-clock x (1- c)))))

(defun smallest (x)
  (smallest-clock x (clock-fn x)))

;; We define our witnessing f for the equation above as fn when applied to
;; (smallest x).

(defun f (x) (fn x (smallest x)))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Section 3: The proof                                               ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

;; To prove that f is indeed the witness we seek we must prove the following
;; theorem.

;; (f x) = (if (test x) (base x) (f (recur x)))

;; The first case (when test holds) is trivial. So the remainder of the proof
;; script will just focus on the (not (test x)) case.

;; First some lemmas about smallest. [Technical note: My reasoning, described
;; below, is in terms of smallest, given a few properties of smallest. I first
;; prove these properties and then disable smallest. I might have actually just
;; proved the properties about smallest-clock, since it is recursive, and then
;; left smallest enabled, but I don't do so since that's not how I think about
;; the problem. To structure the proof well, I actually keep all the facts
;; about smallest in a single encapsulate and then completely disable smallest
;; for the rest of the session.]

(local (include-book "arithmetic/top-with-meta" :dir :system))

(encapsulate 
 ()

 (defthm smallest-is-natp
   (natp (smallest x))
   :rule-classes :type-prescription)

 (local
  (defthm smallest-clock-is-smallest
    (implies (and (> (smallest-clock x c) 0)
                  (natp c))
             (not (equal (fn x (smallest-clock x c))
                         (fn x (1- (smallest-clock x c))))))))
 
 
 (local
  (defthm smallest-clock-is-sufficient
    (implies (and (natp n)
                  (natp c)
                  (< n c)
                  (<= (smallest-clock x c) n))
             (equal (fn x (1+ n))
                    (fn x n)))))
 

 (defthm smallest-is-smallest
   (implies (> (smallest x) 0)
            (not (equal (fn x (smallest x))
                        (fn x (1- (smallest x))))))
   :rule-classes nil
   :hints (("Goal"
            :use ((:instance smallest-clock-is-smallest
                             (c (clock-fn x)))))))
 

(defthm smallest-is-sufficient
  (implies (and (natp n)
                (<= (smallest x) n))
           (equal (fn x (1+ n))
                  (fn x n)))
  :rule-classes nil
  :hints (("Goal"
           :cases ((>= n (clock-fn x))))))

)

(in-theory (disable smallest (smallest)))

(local
 (defun induction-hint (n)
   (if (zp n) nil
     (induction-hint (1- n)))))

;; We first prove that for any m larger than smallest, (fn x m) = (fn x
;; (smallest x)). This means that for any m,n larger than smallest (fn x m) =
;; (fn x n). This will be a critical fact soon.

(local
 (defthm f-is-same-after-smallest
   (implies (and (natp m)
                 (>= m (smallest x)))
            (equal (fn x (smallest x))
                   (fn x m)))
   :rule-classes nil
   :hints (("Goal"
            :induct (induction-hint m))
           ("Subgoal *1/2"
            :use ((:instance smallest-is-sufficient
                             (n (1- m))))))))
 
;; Now we are interested in the case where (test x) = nil. Then the lhs of the
;; desired equation is (if (= (smallest x) 0) (base x) (wrap x (fn (recur x)
;; (1- (smallest x))))) The rhs is (wrap x (fn (recur x)) (smallest (recur
;; x))).  So we need to relate (1- (smallest x)) with (smallest (recur x))
;; under the condition that (smallest x) > 0. Now what do I know when (smallest
;; x) > 0. I know that (test x) = nil. This is because otherwise (fn x
;; (smallest x)) and (fn x (1- (smallest x))) will not be different (which we
;; know from smallest-is-smallest) since by definition of fn, we are left with
;; (base x) in both cases.

(local
 (defthm smallest-greater-than-0-implies-not-test
   (implies (< 0 (smallest x))
            (not (test x)))
   :rule-classes nil
   :hints (("Goal"
            :use ((:instance (:definition fn) (n (smallest x)))
                  (:instance (:definition fn) (n (1- (smallest x))))
                  (:instance smallest-is-smallest))))))

;; Next I prove that if (smallest (recur x)) < (1- m) and (test x) does not
;; hold then fn has already stabilitized at (1- m). This is really easy from
;; smallest-is-sufficient.

(local
 (defthm smallest-less-implies-fn-stabilizes-at-m-minus-1
   (implies (and (natp m)
                 (not (test x))
                 (< (smallest (recur x)) (1- m)))
            (equal (fn x (1- m))
                   (fn x m)))
   :rule-classes nil
   :hints (("Goal"
            :use ((:instance f-is-same-after-smallest
                             (x (recur x))
                             (m (1- m)))
                  (:instance f-is-same-after-smallest
                             (x (recur x))
                             (m (- m 2))))))))

;; Now here's the key lemma, that's (smallest x) -1 < = (smallest (recur x)). I
;; know that since otherwise the function will stabilize at m-1, violating the
;; condition for smallest! So we see that it's in fact (very) important that we
;; start with smallest and not with clock-fn.

(local
 (defthm smallest-minus-1-is-smallest-of-recur
   (implies (< 0 (smallest x))
            (<= (- (smallest x) 1)
                (smallest (recur x))))
   :rule-classes nil
   :otf-flg t
   :hints (("Goal"
            :use ((:instance smallest-is-smallest)
                  (:instance
                   smallest-less-implies-fn-stabilizes-at-m-minus-1
                   (m (smallest x))))))))


;; Now of course the definition of f shows that we're done. Note that I've
;; clubbed two things together, namely the trivial case where test holds, and
;; the other case. I don't comment anything on the trivial case. But for the
;; other one note that it follows just from the above lemma.

(DEFTHM |f satisfies its defining equation|
  (equal (f x)
         (if (test x)
             (base x)
           (wrap x (f (recur x)))))
  :hints (("Goal"
           :use ((:instance f-is-same-after-smallest
                            (m (1+ (smallest (recur x)))))
                 (:instance smallest-minus-1-is-smallest-of-recur)))))