• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
      • Std/lists/intersection$
      • Nats-equiv
      • Repeat
      • Index-of
        • Index-of-theorems
      • 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
• Search

Index-of

(index-of k x) returns the index of the first occurrence of element k in list x if it exists, NIL otherwise.

Index-of is like the Common Lisp function position, but only operates on lists and is not (logically) tail-recursive.

Definitions and Theorems

Function: index-of-aux

(defun
  index-of-aux (k x acc)
  (declare (type (integer 0 *) acc))
  (cond ((atom x) nil)
        ((equal k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Function: index-of-aux-eq

(defun
  index-of-aux-eq (k x acc)
  (declare (type (integer 0 *) acc)
           (type symbol k))
  (cond ((atom x) nil)
        ((eq k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Function: index-of-aux-eql

(defun
  index-of-aux-eql (k x acc)
  (declare (type (integer 0 *) acc)
           (xargs :guard (eqlablep k)))
  (cond ((atom x) nil)
        ((eql k (car x))
         (mbe :logic (ifix acc) :exec acc))
        (t (index-of-aux k (cdr x)
                         (+ 1 (mbe :logic (ifix acc) :exec acc))))))

Theorem: index-of-aux-eq-normalize

(defthm index-of-aux-eq-normalize
        (equal (index-of-aux-eq k x acc)
               (index-of-aux k x acc)))

Theorem: index-of-aux-eql-normalize

(defthm index-of-aux-eql-normalize
        (equal (index-of-aux-eql k x acc)
               (index-of-aux k x acc)))

Function: index-of

(defun index-of (k x)
       (declare (xargs :guard t))
       (mbe :logic (cond ((atom x) nil)
                         ((equal k (car x)) 0)
                         (t (let ((res (index-of k (cdr x))))
                                 (and res (+ 1 res)))))
            :exec (cond ((symbolp k) (index-of-aux-eq k x 0))
                        ((eqlablep k) (index-of-aux-eql k x 0))
                        (t (index-of-aux k x 0)))))

Theorem: index-of-aux-removal

(defthm index-of-aux-removal
        (equal (index-of-aux k x acc)
               (and (index-of k x)
                    (+ (index-of k x) (ifix acc)))))

Theorem: position-equal-ac-is-index-of-aux

(defthm position-equal-ac-is-index-of-aux
        (implies (integerp acc)
                 (equal (position-equal-ac k x acc)
                        (index-of-aux k x acc))))

Theorem: index-of-iff-member

(defthm index-of-iff-member
        (iff (index-of k x) (member k x)))

Theorem: integerp-of-index-of

(defthm integerp-of-index-of
        (iff (integerp (index-of k x))
             (member k x)))

Theorem: natpp-of-index-of

(defthm natpp-of-index-of
        (iff (natp (index-of k x))
             (member k x)))

Theorem: nth-of-index-when-member

(defthm nth-of-index-when-member
        (implies (member k x)
                 (equal (nth (index-of k x) x) k)))

Theorem: index-of-<-len

(defthm index-of-<-len
        (implies (member k x)
                 (< (index-of k x) (len x)))
        :rule-classes :linear)

Theorem: index-of-append-first

(defthm index-of-append-first
        (implies (index-of k x)
                 (equal (index-of k (append x y))
                        (index-of k x))))

Theorem: index-of-append-second

(defthm index-of-append-second
        (implies (and (not (index-of k x))
                      (index-of k y))
                 (equal (index-of k (append x y))
                        (+ (len x) (index-of k y)))))

Theorem: index-of-append-neither

(defthm index-of-append-neither
        (implies (and (not (index-of k x))
                      (not (index-of k y)))
                 (not (index-of k (append x y)))))

Theorem: index-of-append-split

(defthm index-of-append-split
        (equal (index-of k (append x y))
               (or (index-of k x)
                   (and (index-of k y)
                        (+ (len x) (index-of k y))))))

Subtopics

Index-of-theorems

Some theorems about the library function index-of.