• Top
  • Documentation
  • Books
  • 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/osets
    • Std/io
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/alists
• Strip-cars

Alist-keys

(alist-keys x) collects all keys bound in an alist.

This is a "modern" equivalent of strip-cars, which properly respects the non-alist convention; see std/alists for discussion of this convention.

Note that the list of keys returned by alist-keys may contain duplicates. This happens whenever the input alist contains "shadowed" bindings, as in ((a . 1) (a . 2)).

Note about Normal Forms

A key is a among the alist-keys of an alist exactly when hons-assoc-equal is non-nil. We generally prefer hons-assoc-equal as the normal form, so the following rule is enabled by default::

Theorem: alist-keys-member-hons-assoc-equal

(defthm alist-keys-member-hons-assoc-equal
  (iff (member-equal x (alist-keys a))
       (hons-assoc-equal x a)))

However, sometimes the member-based normal form works better when you want to tie into powerful set-reasoning strategies. To support this, the following rule is available but is disabled by default:

Theorem: hons-assoc-equal-iff-member-alist-keys

(defthm hons-assoc-equal-iff-member-alist-keys
  (iff (hons-assoc-equal x a)
       (member-equal x (alist-keys a))))

Obviously these two rules loop, so a theory-invariant insists that you choose one or the other. For greater compatibility between books, please do not non-locally switch the normal form.

Definitions and Theorems

Function: alist-keys

(defun alist-keys (x)
  (declare (xargs :guard t))
  (cond ((atom x) nil)
        ((atom (car x)) (alist-keys (cdr x)))
        (t (cons (caar x) (alist-keys (cdr x))))))

Theorem: alist-keys-when-atom

(defthm alist-keys-when-atom
  (implies (atom x)
           (equal (alist-keys x) nil)))

Theorem: alist-keys-of-cons

(defthm alist-keys-of-cons
  (equal (alist-keys (cons a x))
         (if (atom a)
             (alist-keys x)
           (cons (car a) (alist-keys x)))))

Theorem: list-equiv-implies-equal-alist-keys-1

(defthm list-equiv-implies-equal-alist-keys-1
  (implies (list-equiv x x-equiv)
           (equal (alist-keys x)
                  (alist-keys x-equiv)))
  :rule-classes (:congruence))

Theorem: true-listp-of-alist-keys

(defthm true-listp-of-alist-keys
  (true-listp (alist-keys x))
  :rule-classes :type-prescription)

Theorem: alist-keys-of-hons-acons

(defthm alist-keys-of-hons-acons
  (equal (alist-keys (hons-acons key val x))
         (cons key (alist-keys x))))

Theorem: alist-keys-of-pairlis$

(defthm alist-keys-of-pairlis$
  (equal (alist-keys (pairlis$ keys vals))
         (list-fix keys)))

Theorem: alist-keys-member-hons-assoc-equal

(defthm alist-keys-member-hons-assoc-equal
  (iff (member-equal x (alist-keys a))
       (hons-assoc-equal x a)))

Theorem: hons-assoc-equal-iff-member-alist-keys

(defthm hons-assoc-equal-iff-member-alist-keys
  (iff (hons-assoc-equal x a)
       (member-equal x (alist-keys a))))

Theorem: hons-assoc-equal-when-not-member-alist-keys

(defthm hons-assoc-equal-when-not-member-alist-keys
  (implies (not (member-equal x (alist-keys a)))
           (equal (hons-assoc-equal x a) nil)))

Theorem: alist-keys-of-append

(defthm alist-keys-of-append
  (equal (alist-keys (append x y))
         (append (alist-keys x) (alist-keys y))))

Theorem: alist-keys-of-rev

(defthm alist-keys-of-rev
  (equal (alist-keys (rev x))
         (rev (alist-keys x))))

Theorem: alist-keys-of-revappend

(defthm alist-keys-of-revappend
  (equal (alist-keys (revappend x y))
         (revappend (alist-keys x)
                    (alist-keys y))))