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