		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv

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

The deffixequiv macro can be used to automate certain tedious theorems that arise when following the fty-discipline. In particular, it is intended to help achieve condition 4:

Every function that takes an argument of the foo type should have an equality congruence with foo-equiv on that argument.

Example

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 deffixequiv form will automatically prove nat-equiv congruences and certain related rules for each of the three arguments of multiply-and-add:

(fty::deffixequiv multiply-and-add)

This example is especially concise and automatic because deffixequiv has a special integration with define: it ``knows'' how to:

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 deffixequiv on functions that have not been introduced with define; see the 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.

Theorems Generated

In most cases, three theorems are generated for each argument. Continuing the multiply-and-add example, here are the theorems that will be generated for the c argument:

(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 :executablep nil to the deffixtype form. It is also possible to skip the normalize-const theorem on an individual argument-basis (see below for details), but this is usually going to be much more tedious: you will typically have many functions that operate on your type, and you probably don't want to have to suppress this theorem for each argument of each function!

General Forms

In the general case, there are two ways to invoke deffixequiv.

Basic Form — :omit

(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 :omit.

Advanced Form — :args

(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 :args say which formals to generate theorems about, and no theorems will be generated about any formals that are omitted from :args. The :args also allow you to manually control what type the argument will be assumed to have, specify hints, and so forth.

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 define, then you can either infer the type of the argument (e.g., a above) or manually override it (e.g., c above).

As a special consideration, you can also skip the normalize-const theorem for a certain argument like this:

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

Support for Mutual Recursion

The deffixequiv form typically cannot be used successfully for mutually recursive functions, e.g., those created with defines. Instead, see deffixequiv-mutual.

Subtopics

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.