• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • 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
      • Def-1d-arr
      • Defstobj-clone
      • Def-2d-arr
      • Defabsstobj-events
      • Bitarr
        • Bits-equiv
        • Set-bit
        • Resize-bits
        • Get-bit
        • Bits-length
      • Natarr
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Bitarr

Bits-equiv

Bit-for-bit list equivalence: bits-equiv recognizes lists whose nth elements are bit-equiv to one another. It is often useful for reasoning about bit arrays like bitarr.

This is a universal equivalence, introduced using def-universal-equiv.

Function: bits-equiv

(defun bits-equiv (x y)
       (declare (xargs :non-executable t))
       (declare (xargs :guard t))
       (prog2$ (throw-nonexec-error 'bits-equiv
                                    (list x y))
               (let ((i (bits-equiv-witness x y)))
                    (and (bit-equiv (nth i x) (nth i y))))))

Definitions and Theorems

Theorem: bits-equiv-necc

(defthm bits-equiv-necc
        (implies (not (and (bit-equiv (nth i x) (nth i y))))
                 (not (bits-equiv x y))))

Theorem: bits-equiv-is-an-equivalence

(defthm bits-equiv-is-an-equivalence
        (and (booleanp (bits-equiv x y))
             (bits-equiv x x)
             (implies (bits-equiv x y)
                      (bits-equiv y x))
             (implies (and (bits-equiv x y) (bits-equiv y z))
                      (bits-equiv x z)))
        :rule-classes (:equivalence))

Theorem: bits-equiv-implies-bit-equiv-nth-2

(defthm bits-equiv-implies-bit-equiv-nth-2
        (implies (bits-equiv x x-equiv)
                 (bit-equiv (nth i x) (nth i x-equiv)))
        :rule-classes (:congruence))

Theorem: bits-equiv-implies-bits-equiv-update-nth-3

(defthm bits-equiv-implies-bits-equiv-update-nth-3
        (implies (bits-equiv x x-equiv)
                 (bits-equiv (update-nth i v x)
                             (update-nth i v x-equiv)))
        :rule-classes (:congruence))

Theorem: bit-equiv-implies-bits-equiv-update-nth-2

(defthm bit-equiv-implies-bits-equiv-update-nth-2
        (implies (bit-equiv v v-equiv)
                 (bits-equiv (update-nth i v x)
                             (update-nth i v-equiv x)))
        :rule-classes (:congruence))

Theorem: bits-equiv-implies-bits-equiv-cdr-1

(defthm bits-equiv-implies-bits-equiv-cdr-1
        (implies (bits-equiv a a-equiv)
                 (bits-equiv (cdr a) (cdr a-equiv)))
        :rule-classes (:congruence))

Theorem: bits-equiv-implies-bit-equiv-car-1

(defthm bits-equiv-implies-bit-equiv-car-1
        (implies (bits-equiv x x-equiv)
                 (bit-equiv (car x) (car x-equiv)))
        :rule-classes (:congruence))

Theorem: bit-equiv-implies-bits-equiv-cons-1

(defthm bit-equiv-implies-bits-equiv-cons-1
        (implies (bit-equiv a a-equiv)
                 (bits-equiv (cons a b)
                             (cons a-equiv b)))
        :rule-classes (:congruence))

Theorem: bits-equiv-implies-bits-equiv-cons-2

(defthm bits-equiv-implies-bits-equiv-cons-2
        (implies (bits-equiv b b-equiv)
                 (bits-equiv (cons a b)
                             (cons a b-equiv)))
        :rule-classes (:congruence))