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