• 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
        • Take-of-take-split
        • Take-of-too-many
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
      • All-equalp
      • Sublistp
      • Std/lists/nthcdr
      • Std/lists/append
      • Listpos
      • List-equiv
      • Final-cdr
      • Std/lists/remove
      • Subseq-list
      • Rcons
      • Std/lists/revappend
      • Std/lists/remove-duplicates-equal
      • Std/lists/last
      • Std/lists/reverse
      • Std/lists/resize-list
      • Flatten
      • Suffixp
      • Std/lists/set-difference
      • Std/lists/butlast
      • 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
• Take

Std/lists/take

Lemmas about take available in the std/lists library.

Definitions and Theorems

Theorem: consp-of-take

(defthm consp-of-take
        (equal (consp (take n xs))
               (not (zp n))))

Theorem: take-under-iff

(defthm take-under-iff
        (iff (take n xs) (not (zp n))))

Theorem: len-of-take

(defthm len-of-take
        (equal (len (take n xs)) (nfix n)))

Theorem: take-of-cons

(defthm take-of-cons
        (equal (take n (cons a x))
               (if (zp n)
                   nil (cons a (take (1- n) x)))))

Theorem: take-of-append

(defthm take-of-append
        (equal (take n (append x y))
               (if (< (nfix n) (len x))
                   (take n x)
                   (append x (take (- n (len x)) y)))))

Theorem: take-of-zero

(defthm take-of-zero (equal (take 0 x) nil))

Theorem: take-of-1

(defthm take-of-1
        (equal (take 1 x) (list (car x))))

Theorem: car-of-take

(defthm car-of-take
        (implies (<= 1 (nfix n))
                 (equal (car (take n x)) (car x))))

Theorem: second-of-take

(defthm second-of-take
        (implies (<= 2 (nfix n))
                 (equal (second (take n x)) (second x))))

Theorem: third-of-take

(defthm third-of-take
        (implies (<= 3 (nfix n))
                 (equal (third (take n x)) (third x))))

Theorem: fourth-of-take

(defthm fourth-of-take
        (implies (<= 4 (nfix n))
                 (equal (fourth (take n x)) (fourth x))))

Theorem: take-of-len-free

(defthm take-of-len-free
        (implies (equal len (len x))
                 (equal (take len x) (list-fix x))))

Theorem: equal-of-take-and-list-fix

(defthm equal-of-take-and-list-fix
        (equal (equal (take n x) (list-fix x))
               (equal (len x) (nfix n))))

Theorem: take-of-len

(defthm take-of-len
        (equal (take (len x) x) (list-fix x)))

Theorem: subsetp-of-take

(defthm subsetp-of-take
        (iff (subsetp (take n x) x)
             (or (<= (nfix n) (len x))
                 (member-equal nil x))))

Theorem: take-fewer-of-take-more

(defthm take-fewer-of-take-more
        (implies (<= (nfix a) (nfix b))
                 (equal (take a (take b x)) (take a x))))

Theorem: take-of-take-same

(defthm take-of-take-same
        (equal (take a (take a x)) (take a x)))

Theorem: no-duplicatesp-of-take

(defthm no-duplicatesp-of-take
        (implies (and (no-duplicatesp-equal l)
                      (<= (nfix n) (len l)))
                 (no-duplicatesp-equal (take n l))))

Theorem: take-as-append-and-nth

(defthm take-as-append-and-nth
        (equal (take n l)
               (if (zp n)
                   nil
                   (append (take (- n 1) l)
                           (list (nth (- n 1) l)))))
        :rule-classes ((:definition :install-body nil)))

Theorem: list-equiv-implies-equal-take-2

(defthm list-equiv-implies-equal-take-2
        (implies (list-equiv x x-equiv)
                 (equal (take n x) (take n x-equiv)))
        :rule-classes (:congruence))

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

(defthm list-equiv-implies-equal-butlast-1
        (implies (list-equiv lst lst-equiv)
                 (equal (butlast lst n)
                        (butlast lst-equiv n)))
        :rule-classes (:congruence))

Theorem: element-list-p-of-take

(defthm element-list-p-of-take
        (implies (element-list-p (double-rewrite x))
                 (iff (element-list-p (take n x))
                      (or (element-p nil)
                          (<= (nfix n) (len x)))))
        :rule-classes :rewrite)

Theorem: elementlist-projection-of-take-nil-preserving

(defthm elementlist-projection-of-take-nil-preserving
        (implies (equal nil (element-xformer nil))
                 (equal (elementlist-projection (take n x))
                        (take n (elementlist-projection x))))
        :rule-classes :rewrite)

Theorem: elementlist-projection-of-take

(defthm elementlist-projection-of-take
        (implies (<= (nfix n) (len x))
                 (equal (elementlist-projection (take n x))
                        (take n (elementlist-projection x))))
        :rule-classes :rewrite)

Subtopics

Take-of-take-split

Aggressive case splitting rule to reduce (take a (take b x)).

Take-of-too-many

Rewrite (take n x) when n is more than (len x).