• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/osets
      • Omaps
        • Defomap
        • Update
        • Mapp
        • Assoc
        • Update*
        • Size
        • Keys
        • From-lists
        • Update-induction-on-maps
        • Compatiblep
        • Tail
        • Head
        • Restrict
        • Submap
        • Map
        • Rlookup
        • Emptyp
        • Rlookup*
        • Lookup*
        • Delete*
        • Values
        • In*
        • Lookup
        • Delete
        • Mfix
        • Head-val
        • Head-key
        • Omap-induction2
        • Omap-order-rules
      • All-by-membership
      • Defset
      • In
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Double-containment
      • Difference
      • Cardinality
      • Set
      • Intersectp
    • Std/io
    • 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

• Omaps

Assoc

Find the pair in the omap with a given key.

Signature

(assoc key map) → pair?

Arguments

map — Guard (mapp map).

Returns

pair? — Type (listp pair?).

If the key is present, return the cons pair with the key. Otherwise, return nil.

This is similar to common-lisp::assoc for alists.

Definitions and Theorems

Function: assoc

(defun assoc (key map)
  (declare (xargs :guard (mapp map)))
  (let ((__function__ 'assoc))
    (declare (ignorable __function__))
    (cond ((emptyp map) nil)
          (t (mv-let (key0 val0)
                     (head map)
               (cond ((equal key key0) (cons key0 val0))
                     (t (assoc key (tail map)))))))))

Theorem: listp-of-assoc

(defthm listp-of-assoc
  (b* ((pair? (assoc key map)))
    (listp pair?))
  :rule-classes :rewrite)

Theorem: assoc-of-mfix

(defthm assoc-of-mfix
  (equal (assoc key (mfix map))
         (assoc key map)))

Theorem: assoc-when-emptyp

(defthm assoc-when-emptyp
  (implies (emptyp map)
           (equal (assoc key map) nil))
  :rule-classes (:rewrite :type-prescription))

Theorem: assoc-of-head

(defthm assoc-of-head
  (iff (assoc (mv-nth 0 (head map)) map)
       (not (emptyp map))))

Theorem: assoc-when-assoc-tail

(defthm assoc-when-assoc-tail
  (implies (assoc key (tail map))
           (assoc key map)))

Theorem: acl2-count-assoc-<-map

(defthm acl2-count-assoc-<-map
  (implies (not (emptyp map))
           (< (acl2-count (assoc key map))
              (acl2-count map))))

Theorem: assoc-of-update

(defthm assoc-of-update
  (equal (assoc key1 (update key val map))
         (if (equal key1 key)
             (cons key val)
           (assoc key1 map))))

Theorem: assoc-of-update*

(defthm assoc-of-update*
  (equal (assoc key (update* map1 map2))
         (or (assoc key map1) (assoc key map2))))

Theorem: consp-of-assoc-of-update*

(defthm consp-of-assoc-of-update*
  (equal (consp (assoc key (update* map1 map2)))
         (or (consp (assoc key map1))
             (consp (assoc key map2)))))

Theorem: update-of-cdr-of-assoc-when-assoc

(defthm update-of-cdr-of-assoc-when-assoc
  (implies (assoc k m)
           (equal (update k (cdr (assoc k m)) m)
                  m)))

Theorem: consp-of-assoc-iff-assoc

(defthm consp-of-assoc-iff-assoc
  (iff (consp (assoc key map))
       (assoc key map)))

Theorem: head-key-minimal

(defthm head-key-minimal
  (implies (<< key (mv-nth 0 (head map)))
           (not (assoc key map))))

Theorem: head-key-not-assoc-tail

(defthm head-key-not-assoc-tail
  (not (assoc (mv-nth 0 (head map))
              (tail map))))

Theorem: assoc-of-tail-when-assoc-of-tail

(defthm assoc-of-tail-when-assoc-of-tail
  (implies (assoc key (tail map))
           (equal (assoc key (tail map))
                  (assoc key map))))

Theorem: assoc-of-tail-when-not-head

(defthm assoc-of-tail-when-not-head
  (implies (not (equal key (mv-nth 0 (head map))))
           (equal (assoc key (tail map))
                  (assoc key map))))