		Search-engine friendly clone of the ACL2 documentation.

Subseq-list

Lemmas about subseq-list available in the std/lists library.

ACL2's built-in subseq-list function is used in the definition of subseq. It has a somewhat reasonable definition in terms of take and nthcdr.

Function: subseq-list

(defun subseq-list (lst start end)
  (declare (xargs :guard (and (true-listp lst)
                              (integerp start)
                              (integerp end)
                              (<= 0 start)
                              (<= start end))))
  (take (- end start) (nthcdr start lst)))

Unfortunately subseq-list doesn't properly nfix its start argument, so in the logic, when start is a negative number, we can end up doing a longer take, which is kind of appalling and somewhat reduces our ability to write nice rules about subseq-list.

It is often pretty reasonable to just leave subseq-list enabled.

Definitions and Theorems

Theorem: len-of-subseq-list

(defthm len-of-subseq-list
  (equal (len (subseq-list x start end))
         (nfix (- end start))))

Theorem: consp-of-subseq-list

(defthm consp-of-subseq-list
  (equal (consp (subseq-list x start end))
         (posp (- end start))))

Theorem: subseq-list-under-iff

(defthm subseq-list-under-iff
  (iff (subseq-list x start end)
       (posp (- end start))))

Theorem: subseq-list-of-list-fix

(defthm subseq-list-of-list-fix
  (equal (subseq-list (list-fix x) start end)
         (subseq-list x start end)))

Theorem: list-equiv-implies-equal-subseq-list-1

(defthm list-equiv-implies-equal-subseq-list-1
  (implies (list-equiv x x-equiv)
           (equal (subseq-list x start end)
                  (subseq-list x-equiv start end)))
  :rule-classes (:congruence))

Theorem: subseq-list-starting-from-zero

(defthm subseq-list-starting-from-zero
  (equal (subseq-list x 0 n) (take n x)))

Theorem: subseq-list-of-len

(defthm subseq-list-of-len
  (implies (natp n)
           (equal (subseq-list x n (len x))
                  (nthcdr n (list-fix x)))))