• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
      • Alist-keys
      • Remove-assocs
      • Alist-vals
      • Alist-map-vals
      • Std/alists/strip-cdrs
      • Hons-rassoc-equal
      • Alist-map-keys
      • Std/alists/hons-assoc-equal
      • Fal-extract
      • Std/alists/strip-cars
      • Fal-find-any
      • Fal-extract-vals
      • Std/alists/abstract
      • Fal-all-boundp
      • Std/alists/alistp
      • Append-alist-vals
      • Append-alist-keys
      • Alist-equiv
      • Hons-remove-assoc
      • Std/alists/pairlis$
      • Alists-agree
      • Worth-hashing
      • Sub-alistp
      • Alist-fix
      • Std/alists/remove-assoc-equal
      • Std/alists/assoc-equal
    • 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/alists

Alists-agree

(alists-agree keys al1 al2) determines if the alists al1 and al2 agree on the value of every key in keys.

Definitions and Theorems

Function: alists-agree

(defun alists-agree (keys al1 al2)
       "Do AL1 and AL2 agree on the value of every KEY in KEYS?"
       (declare (xargs :guard t))
       (or (atom keys)
           (and (equal (hons-get (car keys) al1)
                       (hons-get (car keys) al2))
                (alists-agree (cdr keys) al1 al2))))

Theorem: list-equiv-implies-equal-alists-agree-1

(defthm list-equiv-implies-equal-alists-agree-1
        (implies (list-equiv keys keys-equiv)
                 (equal (alists-agree keys al1 al2)
                        (alists-agree keys-equiv al1 al2)))
        :rule-classes (:congruence))

Theorem: alists-agree-hons-assoc-equal

(defthm alists-agree-hons-assoc-equal
        (implies (and (alists-agree keys a b)
                      (member-equal x keys))
                 (equal (hons-assoc-equal x b)
                        (hons-assoc-equal x a))))

Theorem: alists-agree-self

(defthm alists-agree-self
        (alists-agree keys a a))

Theorem: alists-agree-sym

(defthm alists-agree-sym
        (implies (alists-agree keys a b)
                 (alists-agree keys b a)))

Function: alists-disagree-witness

(defun alists-disagree-witness (keys al1 al2)
       (and (consp keys)
            (if (not (equal (hons-get (car keys) al1)
                            (hons-get (car keys) al2)))
                (car keys)
                (alists-disagree-witness (cdr keys)
                                         al1 al2))))

Theorem: alists-agree-iff-witness

(defthm alists-agree-iff-witness
        (iff (alists-agree keys al1 al2)
             (let ((x (alists-disagree-witness keys al1 al2)))
                  (implies (member-equal x keys)
                           (equal (hons-assoc-equal x al1)
                                  (hons-assoc-equal x al2))))))

Theorem: alists-agree-trans

(defthm alists-agree-trans
        (implies (and (alists-agree keys x y)
                      (alists-agree keys y z))
                 (alists-agree keys x z)))