• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • 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
      • Stobj-updater-independence
        • Range-equal
        • Def-updater-independence-thm
      • Def-1d-arr
      • Defstobj-clone
      • Def-2d-arr
      • Defabsstobj-events
      • Bitarr
      • Natarr
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• 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))