• Top
  • Documentation
  • Books
  • 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
        • Prefixp-theorems
      • 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
      • Std/lists/add-to-set
      • 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

Prefixp

(prefixp x y) determines if the list x occurs at the front of the list y.

Definitions and Theorems

Function: prefixp

(defun prefixp (x y)
  (declare (xargs :guard t))
  (if (consp x)
      (and (consp y)
           (equal (car x) (car y))
           (prefixp (cdr x) (cdr y)))
    t))

Theorem: prefixp-when-not-consp-left

(defthm prefixp-when-not-consp-left
  (implies (not (consp x)) (prefixp x y)))

Theorem: prefixp-of-cons-left

(defthm prefixp-of-cons-left
  (equal (prefixp (cons a x) y)
         (and (consp y)
              (equal a (car y))
              (prefixp x (cdr y)))))

Theorem: prefixp-when-not-consp-right

(defthm prefixp-when-not-consp-right
  (implies (not (consp y))
           (equal (prefixp x y) (not (consp x)))))

Theorem: prefixp-of-cons-right

(defthm prefixp-of-cons-right
  (equal (prefixp x (cons a y))
         (if (consp x)
             (and (equal (car x) a)
                  (prefixp (cdr x) y))
           t)))

Theorem: prefixp-of-list-fix-left

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

Theorem: prefixp-of-list-fix-right

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

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

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

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

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

Theorem: len-when-prefixp

(defthm len-when-prefixp
  (implies (prefixp x y)
           (equal (< (len y) (len x)) nil))
  :rule-classes
  ((:rewrite)
   (:linear :corollary (implies (prefixp x y)
                                (<= (len x) (len y))))))

Theorem: take-when-prefixp

(defthm take-when-prefixp
  (implies (prefixp x y)
           (equal (take (len x) y) (list-fix x))))

Theorem: prefixp-of-take

(defthm prefixp-of-take
  (equal (prefixp (take n x) x)
         (<= (nfix n) (len x))))

Theorem: prefixp-reflexive

(defthm prefixp-reflexive (prefixp x x))

Theorem: prefixp-of-append-arg2

(defthm prefixp-of-append-arg2
  (equal (prefixp x (append y z))
         (or (prefixp x y)
             (and (equal (true-list-fix y)
                         (take (len y) x))
                  (prefixp (nthcdr (len y) x) z)))))

Theorem: prefixp-when-equal-lengths

(defthm prefixp-when-equal-lengths
  (implies (>= (len x) (len y))
           (equal (prefixp x y) (list-equiv x y))))

Theorem: prefixp-transitive

(defthm prefixp-transitive
 (implies (and (prefixp x y) (prefixp y z))
          (prefixp x z))
 :rule-classes
 (:rewrite
     (:rewrite :corollary (implies (and (prefixp y z) (prefixp x y))
                                   (prefixp x z)))))

Theorem: prefixp-append-append

(defthm prefixp-append-append
  (equal (prefixp (append x1 x2) (append x1 y))
         (prefixp x2 y)))

Theorem: prefixp-nthcdr-nthcdr

(defthm prefixp-nthcdr-nthcdr
  (implies (and (>= (len l2) n)
                (equal (take n l1) (take n l2)))
           (equal (prefixp (nthcdr n l1) (nthcdr n l2))
                  (prefixp l1 l2))))

Theorem: prefixp-one-way-or-another

(defthm prefixp-one-way-or-another
  (implies (and (prefixp x z)
                (prefixp y z)
                (not (prefixp x y)))
           (prefixp y x))
  :rule-classes
  (:rewrite (:rewrite :corollary (implies (and (prefixp y z)
                                               (prefixp x z)
                                               (not (prefixp x y)))
                                          (prefixp y x)))))

Theorem: nth-when-prefixp

(defthm nth-when-prefixp
  (implies (and (prefixp x y) (< (nfix n) (len x)))
           (equal (nth n y) (nth n x)))
  :rule-classes
  ((:rewrite :corollary (implies (and (prefixp x y)
                                      (not (list-equiv x y))
                                      (< (nfix n) (len x)))
                                 (equal (nth n y) (nth n x))))))

Theorem: append-when-prefixp

(defthm append-when-prefixp
  (implies (prefixp x y)
           (equal (append x (nthcdr (len x) y))
                  y)))

Theorem: subsetp-when-prefixp

(defthm subsetp-when-prefixp
  (implies (prefixp x y)
           (subsetp-equal x y)))

Theorem: prefixp-of-append-arg1

(defthm prefixp-of-append-arg1
  (equal (prefixp (append x y) z)
         (and (<= (+ (len x) (len y)) (len z))
              (equal (true-list-fix x)
                     (take (len x) z))
              (prefixp y (nthcdr (len x) z)))))

Theorem: prefixp-when-prefixp

(defthm prefixp-when-prefixp
  (implies (prefixp y x)
           (equal (prefixp x y) (list-equiv x y))))

Subtopics

Prefixp-theorems

Some theorems about the library function prefixp.