(in-package "ACL2")

#|

 define.lisp
 ~~~~~~~~~~~

Author: Sandip Ray
Date: Sat May  8 00:54:56 2004

In several ACL2 proofs, one encounters with the following problem. One
typically wants to define a recursive function (f x), but the termination of (f
x) is difficult to prove. Then one defines a function (fn x n) so that it has
the same recursive structure as f, but it only recurs upto n steps. The
function fn is easy to admit in ACL2 since the value of n decreases at every
recursive call. The question, then, is: Can we define the function (fn x n) and
provide some additional theorems about fn, which together guarantee that (f x)
is admissible in the logic? In this book, we investigate this issue. We will
consider a general form:

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

We define a function

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

Now let us consider when (f x) is admissible in the logic. The informal idea is
that if we know that after a sufficiently large n, say, (clock x), the function
(fn x n) is known to terminate all the time, then we know that (f x) also
terminates. But how do we capture the notion: "(clock x) is a sufficiently
large value of n" for fn. A naive approach might be to assume the following
constraint for fn:

(implies (and (natp n) (<= (clock x) n)) (equal (fn x n) (fn x (1+ n))))

However, that does not work, since we want a recursive *definition* of f. Why?
Well consider the following function fn:

(fn x n) = (if (or nil (zp n)) (base x) (f x (1- n)))

You can see that for *all* n, (fn x n) = (fn x (1+ n)). However, consider the
corresponding function f. 

(f x) = (if nil (base x) (f x))

Clearly this is not a recursive definition, and this definition cannot be
"defun"-ed in the logic, since there is no measure. So this simple constraint
does not work in general.

Note to myself: The function f can still be introduced as an encapsulate. I
dont know right now if that is possible in general. I could not quite do it for
general functions yet. I will think about it if it is thought to be
interesting. But if f is supposed to be introduced so that one wants to do
induction using f, then this is not sufficient.

Note added Sun Jun 18 17:40:22 2006: A weaker condition is sufficient to just
introduce the equation. For a proof of that fact, please refer to the book
definition.lisp.

In this book we take a different approach. For us, the notion "(clock x) is
sufficiently large" will mean that the test returns non-nil after (clock x)
steps. So we will add the constraint:

(test (recur-n x (clock x)))

where the function recur-n is as below:

(recur-n x n) = (if (zp n) x (recur-n (recur x) (1- n)))

With this constraint (which informally *means* to me that "clock is
sufficient", we show how to admit the function.

Acknowledgments: 
---------------

Vinod Vishwanath suggested this problem, and J Strother Moore suggested
thinking about definitional principles for such
"bounded recursive" functions. This is my shot at it.

|#


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

 (local (defun test (x) (declare (ignore x)) T))
 (local (defun recur (x) x))
 (local (defun clock-fn (x) (declare (ignore x)) 0))

 (defthm clock-fn-is-natp 
   (natp (clock-fn x))
   :rule-classes :type-prescription)
 
 (defun recur-n (x n)
   (if (test x) x
     (if (zp n) x
       (recur-n (recur x) (1- n)))))

 (defthm test-eventually-is-true
   (test (recur-n x (clock-fn x))))

)

(encapsulate
 (((m *) => *))

 (local
  (defthm natp-compound-recognizer
    (iff (natp n)
         (and (integerp n)
              (<= 0 n)))
    :rule-classes :compound-recognizer))

 (local
  (in-theory (disable natp)))

 (local
  (defun rec (x n)
    (declare (xargs :measure (nfix n)))
    (if (test x) x
      (if (zp n) x
        (rec (recur x) (1- n))))))
  
 (local
  (defthm rec-==recur
    (equal (recur-n x n)
           (rec x n))))
 (local
  (defthm rec-after-clock
    (test (rec x (clock-fn x)))
    :hints (("Goal"
             :in-theory (disable test-eventually-is-true)
             :use test-eventually-is-true))))

 (local
  (defun no-test (i x)
    (if (zp i)
        (not (test x))
      (and (not (test (rec x i)))
           (no-test (1- i) x)))))

  (local
   (defthm no-test-implies-no-test
     (implies (and (no-test i x)
                   (natp i)
                   (natp j)
                   (<= j i))
              (equal (test (rec x j)) nil))))

  (local
   (defun min-test-p (i x)
     (and (test (rec x i)) 
          (no-test (1- i) x))))
   (local
    (defun find-min-test (i x)
      (if (zp i)
          (if (test x) (mv T 0) (mv nil 0))
        (if (min-test-p i x) (mv T i)
          (find-min-test (1- i) x)))))

   (local
    (defthm find-min-<=i
      (implies (natp i)
               (<= (mv-nth 1 (find-min-test i x)) i))
      :rule-classes :linear))
   
   (local
    (defthm rec-+-reduction
      (implies (and (natp i)
                    (natp j))
               (equal (rec (rec x i) j)
                      (rec x (+ i j))))))
   (local
    (defthm no-test-rec-+-reduction
      (implies (and (no-test i (rec x j))
                    (no-test j x)
                    (natp i)
                    (natp j))
               (no-test (+ i j) x))))

   (local
    (defthm no-test-minus-reduction-1
      (implies (and (no-test i x)
                    (natp i)
                    (natp j)
                    (<= j i))
               (no-test j x))))

   (local
    (encapsulate 
     nil
     
     (local
      (include-book "/projects/acl2/v2-8-linux/acl2-sources/books/arithmetic-2/meta/top"))
     
     (defthm natp-to-natp
       (implies (and (natp i)
                     (natp j)
                     (<= j i))
                (natp (- i j)))
       :rule-classes :forward-chaining
       :hints (("Goal"
                :in-theory (enable natp))))

     (defthm no-test-minus-reduction-2
       (implies (and (no-test i x)
                     (natp i)
                     (natp j)
                     (<= j i))
                (no-test (- i j) (rec x j))))

     ))


   (local
    (defthm mv-nth-0-reduce
      (equal (mv-nth 0 (list x y)) x)))

   (local
    (defthm mv-nth-1-reduce
      (equal (mv-nth 1 (list x y)) y)))
   
   (local
    (in-theory (disable mv-nth)))
   
   (local
    (defthm mv-nth-0-boolean
      (booleanp (mv-nth 0 (find-min-test i x)))
      :rule-classes :type-prescription))

   (local
    (defthm mv-nth-1-natural
      (natp (mv-nth 1 (find-min-test i x)))
      :rule-classes :type-prescription))
    
    (local
     (defthm mv-nth-0-t-implies-mv-nth-1-test
       (implies (and (mv-nth 0 (find-min-test i x))
                     (natp i))
                (test (rec x (mv-nth 1 (find-min-test i x)))))))

    (local
     (defthm mv-nth-0-t-implies-mv-nth-1-no-test
       (implies (and (mv-nth 0 (find-min-test i x))
                     (natp i)
                     (natp j)
                     (< j (mv-nth 1 (find-min-test i x))))
                (no-test j x))))

    (local
     (defthm mv-nth=t
       (implies (and (test (rec x j))
                     (natp i)
                     (natp j)
                     (<= j i))
                (mv-nth 0 (find-min-test i x)))
       :hints (("Goal"
                :induct (find-min-test i x)))))

    (local
     (defthm test-implies-mv-nth-1-1
       (implies (and (natp i)
                     (natp j)
                     (< j (mv-nth 1 (find-min-test i x))))
                (no-test j x))))
    (local
     (defthm test-implies-mv-nth-1-2
       (implies (and (test (rec x j))
                     (natp i)
                     (natp j)
                     (<= j i))
                (test (rec x (mv-nth 1 (find-min-test i x)))))))

    (local
     (in-theory (disable mv-nth-0-t-implies-mv-nth-1-test
                         mv-nth-0-t-implies-mv-nth-1-no-test
                         mv-nth=t)))

    (local
     (defthm find-min-test=
       (implies (and (natp i)
                     (implies (not (zp i)) (no-test (1- i) x))
                     (<= i j)
                     (natp j)
                     (test (rec x i)))
                (equal (mv-nth 1 (find-min-test j x)) i))
       :hints (("Goal"
                :induct (find-min-test j x)))))

    (local
     (defthm natp-and-no-test-implies-not-test
       (implies (no-test j x)
                (not (test x)))))
     
    (local
     (defthm find-min-test-rec-reduction
       (implies (and (no-test i x)
                     (test (rec x (1+ i)))
                     (natp j)
                     (natp i)
                     (< i j))
                (equal (mv-nth 1 (find-min-test j x)) (1+ i)))
       :hints (("Goal"
                :in-theory (disable test-implies-mv-nth-1-1)
                :do-not '(eliminate-destructors generalize fertilize)
                :induct (find-min-test j x)))))
     (local
      (defthm test-implies-find-min-less
        (implies (and (natp i)
                      (natp j)
                      (test (rec x i))
                      (<= i j))
                 (<= (mv-nth 1 (find-min-test j x))
                     i))
        :rule-classes :linear
        :hints (("Goal"
                 :in-theory (disable test-implies-mv-nth-1-1)
                 :induct (find-min-test j x)))))
      
     (local
      (defthm rec-1-is-recur
        (implies (not (test x))
                 (equal (rec x 1) (recur x)))
        :hints (("Goal"
                 :expand (rec x 1)))))

     (local
      (defthm linear-factoid-1
        (implies (force (natp n))
                 (equal (+ -1 1 n) n))))

     (local
      (defthm linear-factoid-2
        (implies (force (natp n))
                 (equal (+ -1 n 1) n))))

     (local
      (defthm linear-factoid-3
        (implies (force (natp n))
                 (equal (+ 1 -1 n) n))))

     (local
      (defthm recur-removed
        (implies (and (not (test x))
                      (natp i))
                 (equal (rec (recur x) i)
                        (rec x (1+ i))))
        :hints (("Goal"
                 :use ((:instance (:definition rec)
                            (n (1+ i))))))))

     (local
      (defthm no-test-1-=-not-test
        (equal (no-test 1 x)
               (and (not (test x))
                    (not (test (recur x)))))
        :hints (("Goal"
                 :expand (no-test 1 x)))))

     (local
      (defthm not-test-implies-more
        (implies (test x)
                 (equal (mv-nth 1 (find-min-test i x)) 0))
        :hints (("Goal"
                 :in-theory (disable recur-removed)
                 :induct (find-min-test i x)))))

     (local
      (defthm no-test-of-recur
        (implies (not (test x))
                 (no-test (mv-nth 1 (find-min-test (clock-fn (recur x)) (recur x)))
                          x))
        :hints (("Goal"
                 :do-not '(eliminate-destructors generalize fertilize)
                 :do-not-induct t
                 :in-theory (disable rec no-test-rec-+-reduction)
                 :use ((:instance no-test-rec-+-reduction
                                  (i (1- (mv-nth 1 (find-min-test 
                                                    (clock-fn (recur x)) 
                                                    (recur x)))))
                                  (j 1))
                       (:instance test-implies-mv-nth-1-1
                                  (j (1- (mv-nth 1 (find-min-test 
                                                    (clock-fn (recur x))
                                                    (recur x)))))
                                  (x (recur x))
                                  (i (clock-fn (recur x)))))))))
      (local
       (defthm clock-recur-is-true
         (implies (not (test x))
                  (test (rec x (1+ (mv-nth 1 (find-min-test (clock-fn (recur x)) (recur x)))))))
         :hints (("Goal"
                  :in-theory  (disable test-implies-mv-nth-1-2
                                       recur-removed rec)
                  :use ((:instance recur-removed
                                   (i (mv-nth 1 (find-min-test (clock-fn (recur x))
                                                               (recur x)))))
                        (:instance test-implies-mv-nth-1-2
                                   (x (recur x))
                                   (i (clock-fn (recur x)))
                                   (j (clock-fn (recur x)))))))))
       
      (local
       (defthm not-test-implies-natp-1-
         (implies (not (test x))
                  (natp (- (clock-fn x) 1)))
         :hints (("Goal"
                  :in-theory (disable rec-after-clock 
                                      clock-fn-is-natp)
                  :use ((:instance clock-fn-is-natp)
                        (:instance rec-after-clock)))
                 ("Goal'"
                  :cases ((= (clock-fn x) 0)
                          (> (clock-fn x) 0))))))
      (local
       (defthm recur-clock-is-less
         (implies (not (test x))
                  (< (mv-nth 1 (find-min-test (clock-fn (recur x)) (recur x)))
                     (clock-fn x)))
         :rule-classes :linear
         :hints (("Goal"
                  :in-theory (disable rec test-implies-find-min-less)
                  :cases ((< (clock-fn (recur x)) (clock-fn x))
                          (>= (clock-fn (recur x)) (clock-fn x))))
                 ("Subgoal 1"
                  :use ((:instance test-implies-find-min-less
                                   (i (1- (clock-fn x)))
                                   (j (clock-fn (recur x)))
                                   (x (recur x))))))))

      (local
       (defthm find-min-test-decreases
         (implies (not (test x))
                  (< (mv-nth 1 (find-min-test (clock-fn (recur x)) (recur x)))
                     (mv-nth 1 (find-min-test (clock-fn x) x))))
         
         :hints (("Goal"
                  :do-not '(eliminate-destructors generalize fertilize)
                  :do-not-induct t
                  :in-theory (disable no-test-rec-+-reduction
                                      test-implies-mv-nth-1-1 
                                      rec
                                      find-min-test-rec-reduction)
                  :use ((:instance find-min-test-rec-reduction
                                   (i (mv-nth 1 (find-min-test (clock-fn (recur x))
                                                               (recur x))))
                                   (j (clock-fn x))))))))
       
      (local
       (in-theory (disable find-min-test)))

      (local
       (defun m (x)
         (mv-let (flg val)
                 (find-min-test (clock-fn x) x)
                 (declare (ignore flg))
                 val)))

      
      (DEFTHM m-is-ordinal
        (o-p (m x)))

      (defthm m-decreases
        (implies (not (test x))
                 (o< (m (recur x))
                     (m x))))



)

(defstub base (*) => *)
(defstub finish (* *) => *)

(defun f (x)
  (declare (xargs :measure (m x)))
  (if (test x) (base x)
    (finish x (f (recur x)))))