(alist-equiv-bad-guy al1 al2) finds some key, if one exists, that
differs between the alists
This is generally useful for doing pick-a-point style reasoning about alist equivalence.
Definition:
(defchoose alist-equiv-bad-guy (bg) (al1 al2) (not (equal (hons-assoc-equal bg al1) (hons-assoc-equal bg al2))))
Theorem:
(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:
(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:
(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:
(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:
(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:
(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)))))