		Search-engine friendly clone of the ACL2 documentation.

Omaps

Compatiblep

Check if two omaps are compatible, in the sense that they map their common keys to the same values.

Signature
(compatiblep map1 map2) → yes/no
Arguments: map1 — Guard (mapp map1).; map2 — Guard (mapp map2).
Returns: yes/no — Type (booleanp yes/no).

This definition is not optimal for execution. The compatibility of two omaps can be checked by linearly scanning through them in order. A future version of this operation should have that definition, at least for execution.

Definitions and Theorems

Function: compatiblep

(defun compatiblep (map1 map2)
  (declare (xargs :guard (and (mapp map1) (mapp map2))))
  (let ((__function__ 'compatiblep))
    (declare (ignorable __function__))
    (cond ((emptyp map1) t)
          ((mv-let (key1 val1)
                   (head map1)
             (let ((pair2 (assoc key1 map2)))
               (and pair2 (not (equal val1 (cdr pair2))))))
           nil)
          (t (compatiblep (tail map1) map2)))))

Theorem: booleanp-of-compatiblep

(defthm booleanp-of-compatiblep
  (b* ((yes/no (compatiblep map1 map2)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: compatiblep-when-left-emptyp

(defthm compatiblep-when-left-emptyp
  (implies (emptyp map1)
           (compatiblep map1 map2)))

Theorem: compatiblep-when-right-emptyp

(defthm compatiblep-when-right-emptyp
  (implies (emptyp map2)
           (compatiblep map1 map2)))