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

• 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)))