Fn-equal
Equivalence relation on tame functions
Fn-equal is an equivalence relation on tame functions. It
holds between fn1 and fn2 iff both are tame functions and
(apply$ fn1 args) is (apply$ fn2 args), for all args. A
defun-sk event is used to express the universally quantified condition.
defwarrant proves that fn-equal is a congruence relation for
every argument position of ilk :FN.
Ideally one can substitute one functional object for an equivalent one in
functional positions. For example, fn-equal holds between
'(LAMBDA (X) X) and 'IDENTITY, so one would hold that
(collect$ '(LAMBDA (X) X) lst) could be rewritten to (collect$
'IDENTITY lst) since the first argument of collect$ (as defined in
the introduction-to-apply$) has ilk :FN. Unfortunately, because
these are quoted constants, ACL2's rewriter will not rewrite one to the
other!
We regard fn-equal as a reminder to us — or a challenge to
users! — to find a way to handle functional equivalence in the
rewriter.
