		Search-engine friendly clone of the ACL2 documentation.

Std/alists

Alist-equiv

(alist-equiv a b) determines whether the alists a and b are equivalent up to hons-assoc-equal, i.e., whether they bind the same value to every key.

This is a fundamental equivalence relation for alists. It allows you to consider the equivalence of alists regardless of the order of their elements, the presence of shadowed elements, etc.

Note that list-equiv is a refinement of alist-equiv.

Definitions and Theorems

Function: alist-equiv

(defun
 alist-equiv (a b)
 "Do A and B agree on the values of every key?"
 (declare (xargs :guard t))
 (mbe
  :logic (and (sub-alistp a b) (sub-alistp b a))
  :exec (with-fast-alist a
                         (with-fast-alist b
                                          (and (sub-alistp a b)
                                               (sub-alistp b a))))))

Theorem: alist-equiv-is-an-equivalence

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

Theorem: alist-equiv-means-all-keys-agree

(defthm alist-equiv-means-all-keys-agree
        (implies (alist-equiv x y)
                 (alists-agree keys x y)))

Theorem: list-equiv-refines-alist-equiv

(defthm list-equiv-refines-alist-equiv
        (implies (list-equiv x y)
                 (alist-equiv x y))
        :rule-classes (:refinement))

Subtopics

Basic-alist-equiv-congruences: Some congruence rules about alist-equiv for basic alist functions.
Alist-equiv-bad-guy: (alist-equiv-bad-guy al1 al2) finds some key, if one exists, that differs between the alists al1 and al2.