• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Community
  • Std
    • Std/lists
    • Omaps
      • Defomap
      • Update
      • Mapp
      • Assoc
      • Update*
      • From-lists
      • Keys
      • List-lookup
      • Size
      • Compatiblep
      • Submap
      • Tail
      • Restrict
      • Head
      • Update-induction-on-maps
      • Rlookup
      • Lookup
      • List-notin
      • Emptyp
      • Rlookup*
      • Map
      • Lookup*
      • Values
      • List-in
      • Delete*
      • In*
      • Delete
      • From-alist
      • Mfix
      • Head-val
      • Head-key
      • Omap-induction2
      • Omap-order-rules
    • Std/alists
    • 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
  • 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))))

Theorem: assoc-of-mfix-map

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

Theorem: assoc-mequiv-congruence-on-map

(defthm assoc-mequiv-congruence-on-map
  (implies (mequiv map map-equiv)
           (equal (assoc key map)
                  (assoc key map-equiv)))
  :rule-classes :congruence)