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
(def-universal-equiv gfix-equiv :equiv-terms ((equal (gfix x))))
(defun gfix-equiv (x y) (equal (gfix x) (gfix y))) (defequiv gfix-equiv)
(with appropriate hints to ensure that the