An alias for EQUAL. Useful if you want to prove an equality in FGL using a particular strategy.
(top-level-equal x y) → *
Sometimes if you're proving an equivalence of two objects using
FGL/SAT/bitblasting, it's advantageous to use a strategy other than just
checking satisfiability of the negation of the top-level equivalence. For
example, in proving the correctness of SIMD implementations where you're
proving equivalence of two wide integers composed of packed arithmetic results,
you might want to instead prove each of the lanes separately. We can use an
FGL rewrite rule to rewrite the top-lvel equal call to an alias that has a
rewriting strategy to solve it with this scheme. But we don't want to rewrite
all calls of equal this way! Instead, we suggest an alternate strategy:
- Locally introduce a rule rewriting (top-level-equal x y) to the
function implementing your special solving strategy -- solve-lane-by-lane, for example.
- Add a hint to your def-fgl-thm: :hints ('(:clause-processor
The hint will replace only the equal call at the top level of your
theorem with top-level-equal.
Definitions and Theorems
(defun top-level-equal (x y)
(declare (xargs :guard t))
(equal x y))
- Clause processor that replaces the final call of equal in a
theorem conclusion with top-level-equal.