		Search-engine friendly clone of the ACL2 documentation.

Stobj-updater-independence

Range-equal

Check that a range of entries from two lists are equal.

Signature
(range-equal start num x y) → *
Arguments: start — Guard (natp start).; num — Guard (natp num).; x — Guard (true-listp x).; y — Guard (true-listp y).

This is useful for stobj updater independence theorems, e.g.,

(def-stobj-updater-independence sum-range-of-field2-updater-independence
  (implies (range-equal 0 k (nth 2 new) (nth 2 old))
           (equal (sum-range-of-field2 k new)
                  (sum-range-of-field2 k old))))

Also see range-nat-equiv, which is similar but checks nat-equiv of corresponding elements instead of equal.

Definitions and Theorems

Function: range-equal

(defun range-equal (start num x y)
  (declare (xargs :guard (and (natp start)
                              (natp num)
                              (true-listp x)
                              (true-listp y))))
  (let ((__function__ 'range-equal))
    (declare (ignorable __function__))
    (if (zp num)
        t
      (and (equal (nth start x) (nth start y))
           (range-equal (1+ (lnfix start))
                        (1- num)
                        x y)))))

Theorem: range-equal-open

(defthm range-equal-open
  (implies (not (zp num))
           (equal (range-equal start num x y)
                  (and (equal (nth start x) (nth start y))
                       (range-equal (1+ (lnfix start))
                                    (1- num)
                                    x y)))))

Theorem: range-equal-of-nfix-start

(defthm range-equal-of-nfix-start
  (equal (range-equal (nfix start) num x y)
         (range-equal start num x y)))

Theorem: range-equal-nat-equiv-congruence-on-start

(defthm range-equal-nat-equiv-congruence-on-start
  (implies (nat-equiv start start-equiv)
           (equal (range-equal start num x y)
                  (range-equal start-equiv num x y)))
  :rule-classes :congruence)

Theorem: range-equal-of-nfix-num

(defthm range-equal-of-nfix-num
  (equal (range-equal start (nfix num) x y)
         (range-equal start num x y)))

Theorem: range-equal-nat-equiv-congruence-on-num

(defthm range-equal-nat-equiv-congruence-on-num
  (implies (nat-equiv num num-equiv)
           (equal (range-equal start num x y)
                  (range-equal start num-equiv x y)))
  :rule-classes :congruence)

Theorem: range-equal-of-list-fix-x

(defthm range-equal-of-list-fix-x
  (equal (range-equal start num (acl2::list-fix x)
                      y)
         (range-equal start num x y)))

Theorem: range-equal-list-equiv-congruence-on-x

(defthm range-equal-list-equiv-congruence-on-x
  (implies (acl2::list-equiv x x-equiv)
           (equal (range-equal start num x y)
                  (range-equal start num x-equiv y)))
  :rule-classes :congruence)

Theorem: range-equal-of-list-fix-y

(defthm range-equal-of-list-fix-y
  (equal (range-equal start num x (acl2::list-fix y))
         (range-equal start num x y)))

Theorem: range-equal-list-equiv-congruence-on-y

(defthm range-equal-list-equiv-congruence-on-y
  (implies (acl2::list-equiv y y-equiv)
           (equal (range-equal start num x y)
                  (range-equal start num x y-equiv)))
  :rule-classes :congruence)

Theorem: nth-when-range-equal

(defthm nth-when-range-equal
  (implies (and (range-equal start num x y)
                (<= (nfix start) (nfix n))
                (< (nfix n)
                   (+ (nfix start) (nfix num))))
           (equal (nth n x) (nth n y))))

Theorem: range-equal-self

(defthm range-equal-self
  (range-equal start num x x))

Theorem: range-equal-of-update-out-of-range-1

(defthm range-equal-of-update-out-of-range-1
  (implies (not (and (<= (nfix start) (nfix n))
                     (< (nfix n)
                        (+ (nfix start) (nfix num)))))
           (equal (range-equal start num (update-nth n v x)
                               y)
                  (range-equal start num x y))))

Theorem: range-equal-of-update-out-of-range-2

(defthm range-equal-of-update-out-of-range-2
  (implies (not (and (<= (nfix start) (nfix n))
                     (< (nfix n)
                        (+ (nfix start) (nfix num)))))
           (equal (range-equal start num x (update-nth n v y))
                  (range-equal start num x y))))

Theorem: range-equal-of-empty

(defthm range-equal-of-empty
  (range-equal start 0 x y))