A macro for automatically proving boilerplate theorems that show a function has the appropriate congruences for its typed arguments.

The

Every function that takes an argument of thefoo type should have an equality congruence withfoo-equiv on that argument.

As an example, consider the following trivial function, introduced with define.

(define multiply-and-add ((a natp) (b natp) (c natp)) :returns (ans natp :rule-classes :type-prescription) (let ((a (lnfix a)) (b (lnfix b)) (c (lnfix c))) (+ (* a b) c)))

Given this definition, the following

(fty::deffixequiv multiply-and-add)

This example is especially concise and automatic because

- look up the std::extended-formals from the definition,
- notice that these arguments are natps,
- look up the corresponding fixing function and equivalence relation (assuming the basetypes book has been loaded), and then
- generate and prove the correct theorems.

It is possible, but less automatic, to use *Advanced Form*
below.

It is also possible, and even **more automatic**, to instruct define to automatically attempt a deffixequiv on its own: see
fixequiv-hook.

In most cases, three theorems are generated for each argument. Continuing
the

(defthm multiply-and-add-of-nfix-c (equal (multiply-and-add a b (nfix c)) (multiply-and-add a b c))) (defthm multiply-and-add-of-nfix-c-normalize-const (implies (syntaxp (and (quotep c) (not (natp (cadr c))))) (equal (multiply-and-add a b c) (multiply-and-add a b (nfix c))))) (defthm multiply-and-add-nat-equiv-congruence-on-c (implies (nat-equiv c c-equiv) (equal (multiply-and-add a b c) (multiply-and-add a b c-equiv))) :rule-classes :congruence)

In rare cases, certain types may have a predicate and/or fixing function that is either expensive to execute or even ACL2::non-executable. In this case, the second theorem, which normalizes constant values by fixing them to the correct type, will not work well.

The recommended way to suppress this theorem is to add

In the general case, there are two ways to invoke

(deffixequiv function-name :omit (a b) ;; optional :hints (...) ;; applied to all arguments )

This form only works for functions introduced with define. It tries
to prove the theorems described above for each argument that has a known type,
unless the argument is explicitly listed in

(deffixequiv function-name :args (a ;; derive type from DEFINE (b :hints (...)) ;; derive type from DEFINE, custom hints (c natp ...)) ;; explicitly use type NATP :hints (...)) ;; hints for all arguments

This form provides finer-grained control over exactly what will be proven.
In this form, the

This form can work even on functions that are not introduced with define **if** a type is given explicitly for each argument. On the other
hand, if the function is introduced with

As a special consideration, you can also skip the

(deffixequiv foo :args ((c nat :skip-const-thm t)))

The

- Deffixequiv-sk
- A variant of
`deffixequiv`for`defun-sk`functions. - Fixequiv-hook
- An std::post-define-hook for automatically proving fty congruences rules.
- Set-fixequiv-guard-override
- Override the type that is associated with a guard function for purposes of determining automatic congruences with deffixequiv.