		Search-engine friendly clone of the ACL2 documentation.

Macro-libraries

Def-universal-equiv

A macro for defining universally quantified equivalence relations.

It is often useful to introduce equivalence relations such as:

A === B when for every possible element E, A and B agree on E.

For some particular notion of what agree means. This macro gives you a quick way to introduce such a relation, using defun-sk, and then automatically prove that it is an equivalence relation. For instance, an equivalence such as:

(defun-sk foo-equiv (a b)
  (forall (x y z)
          (and (bar-equiv (foo a x y)
                          (foo b x y))
               (baz-equiv (fa a z)
                          (fa b z)))))

Can be introduced using:

(def-universal-equiv foo-equiv (a b)
  :qvars (x y z)
  :equivs ((bar-equiv (foo a x y))
           (baz-equiv (fa a z))))

When called with :defquant t, we use defquant instead of defun-sk. This requires that the WITNESS-CP book be included.

Note that :qvars may be omitted, in which case there is no quantifier (defun-sk) introduced. This can be used as a shortcut to prove that a fixing function induces an equivalence relation, e.g.,

(def-universal-equiv gfix-equiv
  :equiv-terms ((equal (gfix x))))

produces

(defun gfix-equiv (x y)
 (equal (gfix x) (gfix y)))

(defequiv gfix-equiv)

(with appropriate hints to ensure that the defequiv succeeds).