A macro for automatically proving boilerplate theorems that show a function has the appropriate congruences for its typed arguments.
Every function that takes an argument of the
footype should have an equality congruence with foo-equivon 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
This example is especially concise and automatic because
It is possible, but less automatic, to use
In most cases, three theorems are generated for each argument. Continuing
(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)))