Unequiv
The universal equivalence relation, true of every pair of objects. Used
in FGL to program testbenches.
- Signature
(unequiv x y) → *
Unequiv takes two arguments and always returns T. It is an
equivalence relation; in fact, it is the equivalence relation for which every
other equivalence relation is a refinement.
In FGL, if the rewriter enters an unequiv equivalence context, there
are several tools that can be used that can't be used under other equivalence
contexts. These tools include extralogical forms such as syntax-interp,
fgl-interp-obj, and assume. The rewriter can also apply rules whose
equivalence relation is unequiv, meaning the LHS and RHS don't actually
need to be related at all. When the rewriter is under an unequiv context
it essentially means that whatever it computes there can't be relevant to the
truth or falsity of the theorem under consideration, so it can do whatever the
user asks it to do.
Definitions and Theorems
Function: unequiv
(defun unequiv (x y)
(declare (xargs :guard t))
(let ((__function__ 'unequiv))
(declare (ignorable __function__))
t))
Theorem: unequiv-is-an-equivalence
(defthm unequiv-is-an-equivalence
(and (booleanp (unequiv x y))
(unequiv x x)
(implies (unequiv x y) (unequiv y x))
(implies (and (unequiv x y) (unequiv y z))
(unequiv x z)))
:rule-classes (:equivalence))
