• Top
  • Documentation
  • Books
  • 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
      • 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/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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.