• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
      • Hons-remove-duplicates
      • Std/lists/update-nth
      • Set-equiv
      • Duplicity
      • Prefixp
      • Std/lists/take
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/append
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/reverse
      • Std/lists/last
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/butlast
      • Std/lists/set-difference
      • Std/lists/len
      • Std/lists/intersectp
      • Std/lists/true-listp
      • Intersectp-witness
      • Subsetp-witness
      • Std/lists/remove1-equal
      • Rest-n
      • First-n
      • Std/lists/union
      • Append-without-guard
      • Std/lists/subsetp
      • Std/lists/member
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Std/lists
• Subseq

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