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

Listpos

(listpos x y) returns the starting position of the first occurrence of the sublist x within the list y, or NIL if there is no such occurrence.

See also sublistp, which is closely related.

Definitions and Theorems

Function: listpos

(defun listpos (x y)
       (declare (xargs :guard t))
       (cond ((prefixp x y) 0)
             ((atom y) nil)
             (t (let ((pos-in-cdr (listpos x (cdr y))))
                     (and pos-in-cdr (+ 1 pos-in-cdr))))))

Theorem: listpos-when-atom-left

(defthm listpos-when-atom-left
        (implies (atom x)
                 (equal (listpos x y) 0)))

Theorem: listpos-when-atom-right

(defthm listpos-when-atom-right
        (implies (atom y)
                 (equal (listpos x y)
                        (if (atom x) 0 nil))))

Theorem: listpos-of-list-fix-left

(defthm listpos-of-list-fix-left
        (equal (listpos (list-fix x) y)
               (listpos x y)))

Theorem: listpos-of-list-fix-right

(defthm listpos-of-list-fix-right
        (equal (listpos x (list-fix y))
               (listpos x y)))

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

(defthm list-equiv-implies-equal-listpos-1
        (implies (list-equiv x x-equiv)
                 (equal (listpos x y)
                        (listpos x-equiv y)))
        :rule-classes (:congruence))

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

(defthm list-equiv-implies-equal-listpos-2
        (implies (list-equiv y y-equiv)
                 (equal (listpos x y)
                        (listpos x y-equiv)))
        :rule-classes (:congruence))

Theorem: listpos-under-iff

(defthm listpos-under-iff
        (iff (listpos x y) (sublistp x y)))

Theorem: natp-of-listpos

(defthm natp-of-listpos
        (equal (natp (listpos x y))
               (sublistp x y)))

Theorem: integerp-of-listpos

(defthm integerp-of-listpos
        (equal (integerp (listpos x y))
               (sublistp x y)))

Theorem: rationalp-of-listpos

(defthm rationalp-of-listpos
        (equal (rationalp (listpos x y))
               (sublistp x y)))

Theorem: acl2-numberp-of-listpos

(defthm acl2-numberp-of-listpos
        (equal (acl2-numberp (listpos x y))
               (sublistp x y)))

Theorem: listpos-lower-bound-weak

(defthm listpos-lower-bound-weak
        (<= 0 (listpos x y))
        :rule-classes (:linear))

Theorem: listpos-upper-bound-weak

(defthm listpos-upper-bound-weak
        (<= (listpos x y) (len y))
        :rule-classes ((:rewrite) (:linear)))

Theorem: listpos-upper-bound-strong-1

(defthm listpos-upper-bound-strong-1
        (equal (< (listpos x y) (len y))
               (consp y))
        :rule-classes
        ((:rewrite)
         (:linear :corollary (implies (consp y)
                                      (< (listpos x y) (len y))))))

Theorem: listpos-upper-bound-strong-2

(defthm listpos-upper-bound-strong-2
        (implies (sublistp x y)
                 (<= (listpos x y) (- (len y) (len x))))
        :rule-classes ((:rewrite) (:linear)))

Theorem: listpos-complete

(defthm
     listpos-complete
     (implies (prefixp x (nthcdr n y))
              (and (listpos x y)
                   (<= (listpos x y) (nfix n))))
     :rule-classes
     ((:rewrite)
      (:linear :corollary (implies (prefixp x (nthcdr n y))
                                   (<= (listpos x y) (nfix n))))))