		Search-engine friendly clone of the ACL2 documentation.

Std/lists/butlast

Lemmas about butlast available in the std/lists library.

Definitions and Theorems

The usual definition of butlast is in terms of take. But it's often more convenient to reason about butlast directly. In that case, its recursive redefinition may be what you want:

Theorem: butlast-redefinition

(defthm
    butlast-redefinition
    (equal (butlast x n)
           (if (>= (nfix n) (len x))
               nil (cons (car x) (butlast (cdr x) n))))
    :rule-classes ((:definition :clique (butlast)
                                :controller-alist ((butlast t t)))))

Function: butlast-induction

(defun butlast-induction (x n)
       (if (>= (nfix n) (len x))
           nil
           (cons (car x)
                 (butlast-induction (cdr x) n))))

Theorem: use-butlast-induction

(defthm
     use-butlast-induction t
     :rule-classes ((:induction :pattern (butlast x n)
                                :scheme (butlast-induction x n))))

For use with std::deflist:

Theorem: element-list-p-of-butlast

(defthm element-list-p-of-butlast
        (implies (element-list-p (double-rewrite x))
                 (element-list-p (butlast x n)))
        :rule-classes :rewrite)