		Search-engine friendly clone of the ACL2 documentation.

Library-extensions

Lists-noforkp

Check that two lists do not fork in front.

Signature
(lists-noforkp list1 list2) → yes/no
Arguments: list1 — Guard (true-listp list1).; list2 — Guard (true-listp list2).
Returns: yes/no — Type (booleanp yes/no).

The lists must be considered from right to left w.r.t. forking. That is, the lists start at nil and are extended via cons. So long we the same things are consed to both in the same order, the lists do not fork, i.e. stay the same. If elements are added to one list but not the other, the former is ``ahead'', but there is no forking. There continued to be no forking if the shorter list is extended with the same elements as the longer list. Only if at some point there are two different elements, the two lists have forked.

Saying that the two lists do not diverge amounts to saying that the longer one is an extension of the shorter one, or that they are equal if they have the same length. Saying that one is an extension of another is expressed by saying that the shorter one is obtained by removing from (the front of) the longer one a number of elements equal to the difference in lengths.

We prove various properties of this predicate, so that we do not need to open it in proofs that use it.

Definitions and Theorems

Function: lists-noforkp

(defun lists-noforkp (list1 list2)
  (declare (xargs :guard (and (true-listp list1)
                              (true-listp list2))))
  (let ((__function__ 'lists-noforkp))
    (declare (ignorable __function__))
    (cond ((< (len list1) (len list2))
           (equal (nthcdr (- (len list2) (len list1))
                          list2)
                  list1))
          ((> (len list1) (len list2))
           (equal (nthcdr (- (len list1) (len list2))
                          list1)
                  list2))
          (t (equal list1 list2)))))

Theorem: booleanp-of-lists-noforkp

(defthm booleanp-of-lists-noforkp
  (b* ((yes/no (lists-noforkp list1 list2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: lists-noforkp-of-same

(defthm lists-noforkp-of-same
  (lists-noforkp list list))

Theorem: lists-noforkp-of-nil-left

(defthm lists-noforkp-of-nil-left
  (implies (true-listp list)
           (lists-noforkp nil list)))

Theorem: lists-noforkp-of-nil-right

(defthm lists-noforkp-of-nil-right
  (implies (true-listp list)
           (lists-noforkp list nil)))

Theorem: lists-noforkp-of-append-left

(defthm lists-noforkp-of-append-left
  (lists-noforkp (append list1 list2)
                 list2))

Theorem: lists-noforkp-of-append-right

(defthm lists-noforkp-of-append-right
  (lists-noforkp list2 (append list1 list2)))

Theorem: lists-noforkp-of-append-more-right

(defthm lists-noforkp-of-append-more-right
  (implies (and (lists-noforkp list1 list2)
                (<= (len list1) (len list2)))
           (lists-noforkp list1 (append list list2))))

Theorem: lists-noforkp-commutative

(defthm lists-noforkp-commutative
  (equal (lists-noforkp list1 list2)
         (lists-noforkp list2 list1)))