• 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
        • Prefixp-theorems
      • 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

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.