• 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

Fal-find-any

Find the first of many keys bound in a fast alist.

Signature

(fal-find-any keys alist) → ans

Arguments

keys — List of keys to look for.

alist — Fast alist to search.

Returns

ans — A (key . value) pair on success, or nil on failure.

We walk over each key in keys. As soon as we find a key that is bound in alist, we return its value. If none of the keys are bound in alist, we return nil.

Definitions and Theorems

Function: fal-find-any

(defun fal-find-any (keys alist)
       (declare (xargs :guard t))
       (let ((__function__ 'fal-find-any))
            (declare (ignorable __function__))
            (if (atom keys)
                nil
                (or (hons-get (car keys) alist)
                    (fal-find-any (cdr keys) alist)))))

Theorem: fal-find-any-when-atom

(defthm fal-find-any-when-atom
        (implies (atom keys)
                 (equal (fal-find-any keys alist) nil)))

Theorem: fal-find-any-when-empty-alist

(defthm fal-find-any-when-empty-alist
        (implies (atom alist)
                 (not (fal-find-any keys alist))))

Theorem: fal-find-any-of-cons

(defthm fal-find-any-of-cons
        (equal (fal-find-any (cons key keys) alist)
               (or (hons-get key alist)
                   (fal-find-any keys alist))))

Theorem: type-of-fal-find-any

(defthm type-of-fal-find-any
        (or (not (fal-find-any keys alist))
            (consp (fal-find-any keys alist)))
        :rule-classes :type-prescription)

Theorem: consp-of-fal-find-any

(defthm consp-of-fal-find-any
        (iff (consp (fal-find-any keys alist))
             (fal-find-any keys alist)))

Theorem: fal-find-any-of-list-fix-keys

(defthm fal-find-any-of-list-fix-keys
        (equal (fal-find-any (list-fix keys) alist)
               (fal-find-any keys alist)))

Theorem: list-equiv-implies-equal-fal-find-any-1

(defthm list-equiv-implies-equal-fal-find-any-1
        (implies (list-equiv keys keys-equiv)
                 (equal (fal-find-any keys alist)
                        (fal-find-any keys-equiv alist)))
        :rule-classes (:congruence))

Theorem: alist-equiv-implies-equal-fal-find-any-2

(defthm alist-equiv-implies-equal-fal-find-any-2
        (implies (alist-equiv alist alist-equiv)
                 (equal (fal-find-any keys alist)
                        (fal-find-any keys alist-equiv)))
        :rule-classes (:congruence))

Theorem: fal-find-any-of-append

(defthm fal-find-any-of-append
        (equal (fal-find-any (append x y) alist)
               (or (fal-find-any x alist)
                   (fal-find-any y alist))))

Theorem: fal-find-any-under-iff

(defthm fal-find-any-under-iff
        (iff (fal-find-any keys alist)
             (intersectp-equal keys (alist-keys alist))))

Theorem: set-equiv-implies-iff-fal-find-any-1

(defthm set-equiv-implies-iff-fal-find-any-1
        (implies (set-equiv keys keys-equiv)
                 (iff (fal-find-any keys alist)
                      (fal-find-any keys-equiv alist)))
        :rule-classes (:congruence))

Theorem: hons-assoc-equal-when-found-by-fal-find-any

(defthm hons-assoc-equal-when-found-by-fal-find-any
        (implies (and (equal (fal-find-any keys alist) ans)
                      ans)
                 (equal (hons-assoc-equal (car ans) alist)
                        ans)))