(in-package "ACL2")
(local (include-book "tree-reconstruction-proof"))
(set-enforce-redundancy t)
; This book from the standard distribution of ACL2 introduces the lexicographic
; measure, llist, and a well-founded relation, l<, on such measures.
(include-book "ordinals/lexicographic-ordering" :dir :system)
; This book from the standard distribution provides b*, an extension to Lisp's
; let* macro for sequential variable binding. B* is like let* but also allows
; us to bind vectors of variables to the corresponding results returned by
; multi-valued functions. We comment further when we use b*.
(include-book "tools/bstar" :dir :system)
; We represent binary trees as cons trees and leaves as the keyword :LEAF.
; The tree ; Node(Leaf, Node(Node(Leaf, Leaf), Leaf)) is
; (:LEAF . ((:LEAF . :LEAF) . :LEAF))
(defun node (x y)
(declare (xargs :guard t))
(cons x y))
(defun leaf ()
(declare (xargs :guard t))
:LEAF)
(defun treep (x)
(if (consp x)
(and (treep (car x))
(treep (cdr x)))
(eq x :LEAF)))
; The function depths, below, returns the depths of the successive nodes in a
; tree x.
(defun depths_rec (d x)
(cond ((atom x)
(list d))
(t (append (depths_rec (+ d 1) (car x))
(depths_rec (+ d 1) (cdr x))))))
(defun depths (x)
(depths_rec 0 x))
; Below is the measure we will use to admit build_rec. It builds an ordinal
; corresponding to the lexicographic combination of the length of s and the
; non-negative difference of the (car s) and d (after coercing them to
; integers).
(defun build_rec-measure (s d)
(llist (len s) (- (ifix (car s)) (ifix d))))
; We now define build_rec. We define it as a function. To handle failure, we
; return a special flag and test that flag after each recursive call. To
; handle the side-effect of popping s, we return the new s. We use ACL2's
; mechanism for ``multiple-valued functions.'' In particular, build_rec
; returns a vector of 3 values. (a) The first component of the vector is a
; Boolean flag that indicates whether the function ``failed.'' (b) The second
; component, of interest only if the function succeeds, is the tree
; constructed. (c) The third component is the remaining tail of s. The ACL2
; construct used to return three such values is (mv a b c). ``Mv'' stand for
; ``multiple values.''
; Given that (build_rec d s) returns a vector of three such values, then the
; idiom
; (mv-let (erp val new-s)
; (build_rec d s)
; (cond
; (erp )
; (t )))
; should be read as follows: ``evaluate (build_rec d s) and bind the variables
; erp, val, and new-s to the resulting three values. If erp is non-nil, the
; computation ``failed'' and we execute the expression . Otherwise,
; the computation ``succeeded'' and we execute expression . Both
; and may refer to the variables d, s, erp, val, and
; new-s.
; Another problem we have to deal with is that ACL2 must prove termination of
; every function admitted by defun. This function contains nested recursion in
; the sense that the second call of build_rec (to compute the right subtree,
; called val2 below) takes as its last argument the s returned by the first
; recursive call. To prove that the function terminates we must know something
; about this new s. But we cannot know anything about the value of the
; function BEFORE its definitional equation is admitted. So we insert a
; runtime test in the definition below, between the two recursive calls, to
; confirm that the new s has an appropriate property. We embed this test in a
; call of the ACL2 function MBT, which means ``must be true.'' After defining
; the function with this runtime test, we verify the guards -- showing that all
; subexpressions of the defun respect the declared ``types.'' Among other
; things, this proves that the inserted test is always T (as required by the
; guard for MBT). Then, just to make it clear that our definition implements
; the same algorithm shown in the problem statement, we define macros that
; handle the treatment of the first and third returned values and prove that
; our function satisfies the recurence equation drawn from the problem
; statement. We also show that, still further below, that the termination
; proof obligations (that a well-founded measure is decreasing in each
; recursive call) can be proved without the presence of the MBT.
; One last minor point: ACL2 is untyped, so in the initial version of our defun
; we must make sure that d and every element of s is an integer. After
; admitting it with those runtime tests, we show that the guards allow us to
; remove those tests.
(defun build_rec (d s)
; The :measure below is a lexicographic combination of the length of s and the
; non-negative difference between the first element of s and d (after coercing
; both to integers). Defun will force ACL2 to prove that this measure
; decreases according to the specified well-founded relation below, on every
; recursive call. The only fly in the story is that the definition below
; includes a test, marked with mbt below and explained there. However, we
; prove that this test is equivalent to T when the :guards of build_rec are
; respected, i.e., when d is an integer and s is a list of integers as
; specified below. We will also demonstrate that we can prove the termination
; obligations when the mbt test is eliminated.
(declare (xargs :measure (build_rec-measure s d)
:well-founded-relation l<
:guard (and (integerp d)
(integer-listp s))
:verify-guards nil))
(cond
((endp s)
(mv t nil s))
(t (let ((h (ifix (car s)))
(d (ifix d)))
; Because ACL2 is untyped, above we coerce d and the elements of s to integers
; with the function ifix. Any element of s that is not an integer is coerced
; to 0. We will prove that we will only call this function on an integer d and
; list of integers s, so how we handle the ``unexpected'' cases does not
; matter.
(cond ((< h d)
(mv t nil s))
((equal h d)
(let ((s (cdr s)))
(mv nil (leaf) s)))
(t (mv-let (erp1 val1 s1)
(build_rec (+ d 1) s)
(cond
(erp1 (mv erp1 nil s1))
; The next condition is a call of MBT ("must be true"). A call of MBT
; logically returns its argument. HOWEVER, guard verification guarantees that
; the argument actually always evaluates to T (true) -- and in fact, execution
; of this function will simply treat the MBT call as T, without even evaluating
; the argument. Thus, by proving termination of the logical code, we have in
; actuality proved termination of the running code in which the MBT call is
; replaced by T. For another way to see that the executable code terminates,
; see the Remark below.
((mbt (or (equal s1 s)
(< (len s1) (len s))))
(mv-let (erp2 val2 s2)
(build_rec (+ d 1) s1)
(if erp2
(mv erp2 nil s2)
(mv nil (node val1 val2) s2))))
(t (mv :impossible nil s))))))))))
; The following shows that we respect the specified guards of build_rec and
; also shows that when the guards are true the MBT above is equivalent to T.
(verify-guards build_rec)
; We now demonstrate that our build_rec is exactly yours. We do it by:
; (1) lifting the runtime ifix tests out of the definition and relying on
; the guards to insure that they are unnecessary,
; (2) defining Lisp macros to manipulate triples so as to treat the
; first returned value as an error flag and the last as the new value of
; s, and
; (3) exploiting the fact that the MBT test used in build_rec always
; returns T.
; Here are the macros we mentioned in (2):
(defmacro fail () `(mv t nil s))
(defmacro succeed (val) `(mv nil ,val s))
(defmacro let! (bindings body)
(cond ((endp bindings) body)
(t `(mv-let (erp ,(car (car bindings)) s)
,(cadr (car bindings))
(cond
(erp (fail))
(t (let! ,(cdr bindings) ,body)))))))
; We extend the notation supported by the b* macro. It will be obvious what
; this does in a moment.
(def-b*-binder !
`(let! ((,(car args) ,(car forms)))
,rest-expr))
; And here is the ``pretty'' version of our build_rec that is the same as
; yours. This theorem shows that our build_rec satisfies the equation
; suggested in the problem statement, with appropriate handling of failure.
; Think of b* as a sequence of (conditional) assignments and compare the sequence
; below to the problem statement.
(defthm pretty-def-of-build_rec
(implies (and (integerp d)
(integer-listp s))
(equal (build_rec d s)
(b* (((when (endp s)) (fail))
(h (first s))
((when (< h d)) (fail))
((when (equal h d)) (let ((s (rest s)))
(succeed (leaf))))
((! val1) (build_rec (+ d 1) s))
((! val2) (build_rec (+ d 1) s)))
(succeed (node val1 val2)))))
:rule-classes nil)
; Because of the work done by verify-guards, as explained in our comment about
; MBT in the definition of build_rec, the runtime (Common Lisp) version of our
; build_rec actually computes EXACTLY as suggested by the theorem above:
; provided d is an integer and s is a list of integers, no unnecessary runtime
; tests are performed.
(defun build (s)
(declare (xargs :guard (integer-listp s)))
(mv-let (erp tree s)
(build_rec 0 s)
(cond
(erp :fail)
((not (endp s)) :fail)
(t tree))))
; -----------------------------------------------------------------
; Verification Task 1: If build does not fail on a list of integers s, then
; the depths of the leaves in tree built is s.
(defthm verification-task-1
(implies (and (integer-listp s)
(not (equal (build s) :fail)))
(equal (depths (build s)) s)))
; -----------------------------------------------------------------
; Verification Task 2: If build fails, then no object x has the property
; that its depths is s.
(defthm verification-task-2
(implies (equal (build s) :fail)
(not (equal (depths x) s))))
; -----------------------------------------------------------------
; Verification Task 3: Build terminates. That is insured by the admissions of
; the definitions of build_rec and build as total functions... Except that our
; build_rec has the MBT test in it that the problem does not have. However, we
; have proved (in the verify-guards above) that the MBT is always T, and hence
; we can prove the termination obligations without that test. Here they are, with
; the MBT test removed.
; Technically we prove that the specified measure is a lexicographic measure
; (lexp) and that it decreases in each recursive call, provided the relevant
; tests are true. L< is known to be well-founded by virtue of being defined in
; terms of ACL2's built in well-founded ``ordinal less-than'' on ordinals below
; epsilon_0.
(defthm verification-task-3
(and (lexp (build_rec-measure s d))
(implies (and (not (endp s))
(<= (ifix d) (ifix (car s)))
(not (equal (ifix (car s)) (ifix d))))
(l< (build_rec-measure s (+ (ifix d) 1))
(build_rec-measure s d)))
(implies (and (not (endp s))
(<= (ifix d) (ifix (car s)))
(not (equal (ifix (car s)) (ifix d)))
(not (mv-nth 0 (build_rec (+ (ifix d) 1) s))))
(l< (build_rec-measure (mv-nth 2 (build_rec (+ (ifix d) 1) s))
(+ (ifix d) 1))
(build_rec-measure s d))))
:rule-classes nil)
; -----------------------------------------------------------------
; Here is the demonstration that build satisfies the two concrete examples
; given.
(defthm verification-task-4
(and (equal (build '(1 3 3 2))
(node (leaf) (node (node (leaf) (leaf)) (leaf))))
(equal (build '(1 3 2 2))
:FAIL))
:rule-classes nil)
; To demonstrate that our build is reasonably efficient, we note that every
; Lisp s-expression is isomorphic to one of your trees. So below we define a
; function that builds the tree corresponding to a given s-expression. Since
; our defuns are, in fact, s-expressions, they provide a source of trees on
; which we can test build -- a source containing bigger examples than those
; requested. To illustrate this, we take the defun of build_rec, convert it to
; one of your trees, and then exhibit the list of depths of its leaves and show
; that we get that tree back when we build from that list of depths.
(defun tree-fix (x)
(if (atom x)
(leaf)
(node (tree-fix (car x))
(tree-fix (cdr x)))))
(defthm verification-task-4-redux
(let ((tree (tree-fix
'(defun build_rec (d s)
(declare (xargs :measure (llist (len s)
(nfix (- (ifix (car s)) (ifix d))))
:well-founded-relation l<
:guard (and (integerp d)
(integer-listp s))
:verify-guards nil))
(cond
((endp s)
(mv t nil s))
(t (let ((h (ifix (car s)))
(d (ifix d)))
(cond ((< h d)
(mv t nil s))
((equal h d)
(let ((s (cdr s)))
(mv nil (leaf) s)))
(t (mv-let (erp1 val1 s1)
(build_rec (+ d 1) s)
(cond
(erp1 (mv erp1 nil s1))
((mbt (or (equal s1 s)
(< (len s1) (len s))))
(mv-let (erp2 val2 s2)
(build_rec (+ d 1) s1)
(if erp2
(mv erp2 nil s2)
(mv nil (node val1 val2) s2))))
(t (mv :impossible nil s)))))))))))))
(and (equal (depths tree)
'(1 2 4 5 5 5 7 8 10 12 13 13 13 15 17 19 20 20 18 18 19 19 17 14 12
10 11 12 14 16 17 17 17 18 18 16 14 15 15 6 6 9 10 10 10 11 12 13
13 9 9 11 14 16 18 19 19 17 15 15 17 18 18 16 14 14 17 18 19 19 18
19 20 21 21 17 18 19 20 20 19 22 24 25 25 23 21 22 23 25 25 25 25 21
18 18 20 22 23 24 24 23 25 26 27 27 25 25 24 26 28 29 30 31 31 27 28
30 32 33 34 34 33 35 36 36 36 37 37 35 32 29 29 31 32 33 33 32 34 35
36 36 34 34 33 34 36 37 38 39 39 37 38 40 41 42 42 40 40 36 32 28 28
30 31 32 33 33 29 27 23 19 17 13 10 8 5))
(equal (build (depths tree))
tree)))
:rule-classes nil)