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