subseq

(in-package "ACL2")

(defsection subseq-list
  :parents (std/lists subseq)
  :short "Lemmas about @(see subseq-list) available in the @(see std/lists)
library."
  :long "<p>ACL2's built-in @('subseq-list') function is used in the definition
of @('subseq').  It has a somewhat reasonable definition in terms of @(see take)
and @(see nthcdr).</p>

@(def subseq-list)

<p>Unfortunately @('subseq-list') doesn't properly @(see 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').</p>

<p>It is often pretty reasonable to just leave @('subseq-list') enabled.</p>"
  (defthm len-of-subseq-list
    (equal (len (subseq-list x start end)) (nfix (- end start))))
  (defthm consp-of-subseq-list
    (equal (consp (subseq-list x start end))
      (posp (- end start))))
  (defthm subseq-list-under-iff
    (iff (subseq-list x start end) (posp (- end start))))
  (defthm subseq-list-of-list-fix
    (equal (subseq-list (list-fix x) start end)
      (subseq-list x start end)))
  (defcong list-equiv equal (subseq-list x start end) 1)
  (defthm subseq-list-starting-from-zero
    (equal (subseq-list x 0 n) (take n x))
    :hints (("Goal" :in-theory (enable subseq-list))))
  (defthm subseq-list-of-len
    (implies (natp n)
      (equal (subseq-list x n (len x)) (nthcdr n (list-fix x))))
    :hints (("Goal" :in-theory (enable take)))))