• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
      • Std/lists/abstract
      • Rev
      • Defsort
      • List-fix
      • Std/lists/nth
        • Equal-by-nths
      • 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
      • 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
• Nth

Std/lists/nth

Lemmas about nth available in the std/lists library.

Definitions and Theorems

Trivial reductions

Theorem: nth-when-atom

(defthm nth-when-atom
        (implies (atom x)
                 (equal (nth n x) nil)))

Theorem: nth-when-zp

(defthm nth-when-zp
        (implies (zp n)
                 (equal (nth n x) (car x))))

Theorem: nth-of-nil

(defthm nth-of-nil (equal (nth n nil) nil))

Theorem: nth-of-list-fix

(defthm nth-of-list-fix
        (equal (nth n (list-fix x)) (nth n x)))

Theorem: nth-of-nfix

(defthm nth-of-nfix
        (equal (nth (nfix n) x) (nth n x)))

Note: Matt Kaufmann reported that the following lemma got expensive in one of his books, so we now disable it by default and instead leave enabled a -cheap rule with a backchain limit.

Theorem: nth-when-too-large

(defthm nth-when-too-large
        (implies (<= (len x) (nfix n))
                 (equal (nth n x) nil)))

Theorem: nth-when-too-large-cheap

(defthm nth-when-too-large-cheap
        (implies (<= (len x) (nfix n))
                 (equal (nth n x) nil))
        :rule-classes ((:rewrite :backchain-limit-lst 1)))

Lemmas about ACL2-count of nth

Theorem: acl2-count-of-nth-linear

(defthm acl2-count-of-nth-linear
        (implies (consp x)
                 (< (acl2-count (nth i x))
                    (acl2-count x)))
        :rule-classes :linear)

Theorem: acl2-count-of-nth-linear-weak

(defthm acl2-count-of-nth-linear-weak
        (<= (acl2-count (nth i x))
            (acl2-count x))
        :rule-classes :linear)

Theorem: acl2-count-of-nth-rewrite

(defthm acl2-count-of-nth-rewrite
        (equal (< (acl2-count (nth i x))
                  (acl2-count x))
               (or (consp x) (> (acl2-count x) 0))))

Nth with other basic list functions

Note that we don't prove a rule about update-nth, because nth-update-nth is an ACL2 builtin.

Theorem: member-of-nth

(defthm member-of-nth
        (implies (< (nfix n) (len x))
                 (member (nth n x) x)))

Theorem: nth-of-append

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

Theorem: nth-of-revappend

(defthm nth-of-revappend
        (equal (nth n (revappend x y))
               (if (< (nfix n) (len x))
                   (nth (- (len x) (+ 1 (nfix n))) x)
                   (nth (- n (len x)) y))))

Theorem: nth-of-rev

(defthm nth-of-rev
        (equal (nth n (rev x))
               (if (< (nfix n) (len x))
                   (nth (- (len x) (+ 1 (nfix n))) x)
                   nil)))

Theorem: nth-of-reverse

(defthm nth-of-reverse
        (equal (nth n (reverse x))
               (if (< (nfix n) (len x))
                   (nth (- (len x) (+ 1 (nfix n))) x)
                   nil)))

Theorem: nth-of-take

(defthm nth-of-take
        (equal (nth i (take n l))
               (if (< (nfix i) (nfix n))
                   (nth i l)
                   nil)))

Theorem: nth-of-make-list-ac

(defthm nth-of-make-list-ac
        (equal (nth n (make-list-ac m val acc))
               (if (< (nfix n) (nfix m))
                   val (nth (- n (nfix m)) acc))))

Theorem: nth-of-repeat

(defthm nth-of-repeat
        (equal (nth n (repeat m a))
               (if (< (nfix n) (nfix m)) a nil)))

Theorem: nth-of-nthcdr

(defthm nth-of-nthcdr
        (equal (nth n (nthcdr m x))
               (nth (+ (nfix n) (nfix m)) x)))

Theorem: nth-of-last

(defthm nth-of-last
        (equal (nth n (last x))
               (if (zp n) (car (last x)) nil)))

Theorem: nth-of-butlast

(defthm nth-of-butlast
        (equal (nth n (butlast x m))
               (if (< (nfix n) (- (len x) (nfix m)))
                   (nth n x)
                   nil)))

Nth of element lists and projections

These are for use with std::deflist and std::defprojection.

Theorem: element-p-of-nth-when-element-list-p-when-nil-element

(defthm element-p-of-nth-when-element-list-p-when-nil-element
        (implies (and (element-p nil) (element-list-p x))
                 (element-p (nth n x)))
        :rule-classes :rewrite)

Theorem: element-p-of-nth-when-element-list-p-when-nil-unknown

(defthm element-p-of-nth-when-element-list-p-when-nil-unknown
        (implies (and (element-list-p x)
                      (< (nfix n) (len x)))
                 (element-p (nth n x)))
        :rule-classes :rewrite)

Theorem: element-p-of-nth-when-element-list-p-when-nil-not-element-non-negated

(defthm
 element-p-of-nth-when-element-list-p-when-nil-not-element-non-negated
 (implies (and (not (element-p nil))
               (element-list-p x))
          (iff (element-p (nth n x))
               (< (nfix n) (len x))))
 :rule-classes :rewrite)

Theorem: element-p-of-nth-when-element-list-p-when-nil-not-element-negated

(defthm
   element-p-of-nth-when-element-list-p-when-nil-not-element-negated
   (implies (and (not (element-p nil))
                 (element-list-p x))
            (iff (non-element-p (nth n x))
                 (<= (len x) (nfix n))))
   :rule-classes :rewrite)

Theorem: nth-of-elementlist-projection-when-nil-preservingp

(defthm nth-of-elementlist-projection-when-nil-preservingp
        (implies (equal (element-xformer nil) nil)
                 (equal (nth n (elementlist-projection x))
                        (element-xformer (nth n x))))
        :rule-classes :rewrite)

Theorem: nth-of-elementlist-projection-when-not-nil-preservingp

(defthm nth-of-elementlist-projection-when-not-nil-preservingp
        (equal (nth n (elementlist-projection x))
               (and (< (nfix n) (len x))
                    (element-xformer (nth n x))))
        :rule-classes :rewrite)

Theorem: nth-of-element-list-fix-when-nil-element

(defthm nth-of-element-list-fix-when-nil-element
        (implies (element-p nil)
                 (equal (nth n (element-list-fix x))
                        (element-fix (nth n x))))
        :rule-classes :rewrite)

Theorem: nth-of-element-list-fix-unless-nil-element

(defthm nth-of-element-list-fix-unless-nil-element
        (equal (nth n (element-list-fix x))
               (and (< (nfix n) (len x))
                    (element-fix (nth n x))))
        :rule-classes :rewrite)

Subtopics

Equal-by-nths

Proof technique: show two lists are equal by showing that their nth elements are always the same.