		Search-engine friendly clone of the ACL2 documentation.

Deffixequiv-mutual

Like deffixequiv, but for mutually-recursive functions.

See deffixequiv. The deffixequiv-mutual macro attempts to prove the same theorems, but for a clique of mutually recursive functions. This is trickier because, as per usual with mutually recursive functions, we typically need to prove the congruences all together, for all of the functions in the clique at once, using a mutually inductive proof.

Accordingly, the deffixequiv-mutual macro attempts to prove a mutually-inductive theorem of which the individual function-of-fix-arg theorems are corollaries, then uses these to prove the constant-normalization and congruence theorems. (These three theorems are discussed in deffixequiv.

Important Note: deffixequiv-mutual will not work if the mutual recursion in question was not created using defines.

Examples

The syntax of deffixequiv-mutual is similar to that of deffixequiv. You again have the choice of either providing :omit, args, or both. However, are also some extensions of these options, as described below.

As a running example, consider the following mutual recursion:

(defines foo-bar-mutual-rec
  (define foo ((x integerp) y (z natp))
    :flag f
    ...)
  (define bar ((x integerp) y (z nat-listp))
    :flag b
    ...))

Here, then, are some ways to invoke deffixequiv-mutual:

;; Derives all argument types from guards and proves
;; them all in one mutual induction.
;;
;; Note: use name of defines form, foo-bar-mutual-rec,
;;       not the name of one of the functions!
(deffixequiv-mutual foo-bar-mutual-rec)

;; Proves only things pertaining to the X argument of both functions
(deffixequiv-mutual foo-bar-mutual-rec :args (x))
;; Same:
(deffixequiv-mutual foo-bar-mutual-rec :omit (y z))

;; Proves string congruence of Y on both functions
(deffixequiv-mutual foo-bar-mutual-rec :args ((y string)))

;; Proves string congruence of y in foo and string-listp in bar
(deffixequiv-mutual foo-bar-mutual-rec
                    :args ((foo (y stringp))
                           (bar (y string-listp))))

;; Omit x in foo and y in bar
(deffixequiv-mutual foo-bar-mutual-rec
                    :omit ((foo x) (bar y)))

;; Various combinations of :args usages
(deffixequiv-mutual foo-bar-mutual-rec
   :args (x                       ;; all functions, automatic type
          (z natp :hints (...))   ;; all functions, explicit type
          (foo (y stringp :skip-const-thm t :hints (...)))
                                  ;; foo only, explicit type
          (bar (z nat-listp)))    ;; override non-function-specific entry
   :hints (...))  ;; hints for the whole inductive proof