• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
    • 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
        • Basic-alist-equiv-congruences
        • Alist-equiv-bad-guy
      • 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/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Alist-equiv

Alist-equiv-bad-guy

(alist-equiv-bad-guy al1 al2) finds some key, if one exists, that differs between the alists al1 and al2.

This is generally useful for doing pick-a-point style reasoning about alist equivalence.

Definitions and Theorems

Definition: alist-equiv-bad-guy

(defchoose alist-equiv-bad-guy (bg)
                               (al1 al2)
  (not (equal (hons-assoc-equal bg al1)
              (hons-assoc-equal bg al2))))

Theorem: alists-agree-when-agree-on-alist-equiv-bad-guy

(defthm alists-agree-when-agree-on-alist-equiv-bad-guy
  (implies (let ((bg (alist-equiv-bad-guy al1 al2)))
             (equal (hons-assoc-equal bg al1)
                    (hons-assoc-equal bg al2)))
           (alists-agree keys al1 al2)))

Theorem: alists-agree-when-agree-on-alist-equiv-bad-guy1

(defthm alists-agree-when-agree-on-alist-equiv-bad-guy1
  (implies (let ((bg (alist-equiv-bad-guy al1 al2)))
             (equal (hons-assoc-equal bg al1)
                    (hons-assoc-equal bg al2)))
           (alists-agree keys al2 al1)))

Theorem: sub-alistp-when-agree-on-alist-equiv-bad-guy

(defthm sub-alistp-when-agree-on-alist-equiv-bad-guy
  (implies (let ((bg (alist-equiv-bad-guy al1 al2)))
             (equal (hons-assoc-equal bg al1)
                    (hons-assoc-equal bg al2)))
           (sub-alistp al1 al2)))

Theorem: sub-alistp-when-agree-on-alist-equiv-bad-guy1

(defthm sub-alistp-when-agree-on-alist-equiv-bad-guy1
  (implies (let ((bg (alist-equiv-bad-guy al2 al1)))
             (equal (hons-assoc-equal bg al1)
                    (hons-assoc-equal bg al2)))
           (sub-alistp al1 al2)))

Theorem: alist-equiv-when-agree-on-bad-guy

(defthm alist-equiv-when-agree-on-bad-guy
  (implies (let ((bg (alist-equiv-bad-guy al1 al2)))
             (equal (hons-assoc-equal bg al1)
                    (hons-assoc-equal bg al2)))
           (equal (alist-equiv al1 al2) t)))

Theorem: alist-equiv-iff-agree-on-bad-guy

(defthm alist-equiv-iff-agree-on-bad-guy
  (iff (alist-equiv al1 al2)
       (let ((bg (alist-equiv-bad-guy al1 al2)))
         (equal (hons-assoc-equal bg al1)
                (hons-assoc-equal bg al2)))))