		Search-engine friendly clone of the ACL2 documentation.

Sublistp

(sublistp x y) checks whether the list x ever occurs within the list y.

ACL2 has a built-in search function, but it's very complicated; it can operate on either lists or strings, using either equality or case-insensitive character comparison, and can stop early, and can search from the front or end, and so on.

In comparison, sublistp is much simpler. It only operates on lists, always considers only equality, and always searches the whole list from the front. This makes it generally much more pleasant to reason about.

Definitions and Theorems

Function: sublistp

(defun sublistp (x y)
  (declare (xargs :guard t))
  (cond ((prefixp x y) t)
        ((atom y) nil)
        (t (sublistp x (cdr y)))))

Theorem: sublistp-when-atom-left

(defthm sublistp-when-atom-left
  (implies (atom x)
           (equal (sublistp x y) t)))

Theorem: sublistp-when-atom-right

(defthm sublistp-when-atom-right
  (implies (atom y)
           (equal (sublistp x y) (atom x))))

Theorem: sublistp-of-cons-right

(defthm sublistp-of-cons-right
  (equal (sublistp x (cons a y))
         (or (prefixp x (cons a y))
             (sublistp x y))))

Theorem: sublistp-when-prefixp

(defthm sublistp-when-prefixp
  (implies (prefixp x y) (sublistp x y)))

Theorem: sublistp-of-list-fix-left

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

Theorem: sublistp-of-list-fix-right

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

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

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

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

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

Theorem: lower-bound-of-len-when-sublistp

(defthm lower-bound-of-len-when-sublistp
  (implies (sublistp x y)
           (<= (len x) (len y)))
  :rule-classes ((:rewrite) (:linear)))

Theorem: sublistp-sound

(defthm sublistp-sound
  (implies (sublistp x y)
           (let ((n (listpos x y)))
             (prefixp x (nthcdr n y)))))

Theorem: sublistp-complete

(defthm sublistp-complete
  (implies (prefixp x (nthcdr n y))
           (sublistp x y)))