		Search-engine friendly clone of the ACL2 documentation.

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.