		Search-engine friendly clone of the ACL2 documentation.

Mutual-recursion

Make-flag

Create a flag-based ACL2::induction scheme for a mutual-recursion.

The make-flag macro lets you quickly introduce:

a "flag function" that mimics a mutual-recursion, and
a theorem proving that the appropriate invocations of the flag function are equivalent to the original mutually-recursive functions,
a macro for proving properties by induction according to the flag function.

Generally speaking, writing a corresponding flag function is the first step toward proving any inductive property about mutually recursive definitions; more discussion below.

Using make-flag

Example:

(make-flag flag-pseudo-termp               ; flag function name (optional)
           pseudo-termp                    ; any member of the clique
           ;; optional arguments:
           :flag-mapping ((pseudo-termp      term)
                          (pseudo-term-listp list))
           :defthm-macro-name defthm-pseudo-termp
           :flag-var flag
           :body :last                     ; use last body, not original
           :hints (("Goal" ...))         ; for the measure theorem
                                           ; (usually not necessary)
           :expand-with-original-defs t    ; for the equivalence thm
                                           ; (usually not necessary)
           )

Here pseudo-termp is the name of a function in a mutually recursive clique. In this case, the clique has two functions, pseudo-termp and pseudo-term-listp. The name of the newly generated flag function can be provided explicitly, or else will be formed by sticking flag- on the front of the clique member's name.

The other arguments are optional:

:flag-mapping specifies short names to identify with each of the functions of the clique. By default we just use the function names themselves, but it's usually nice to pick shorter names since you'll have to mention them in the theorems you prove. The argument, if supplied and non-nil, should be a list that specifies a short name for every function in the clique. Each member of that list should be of the form (old new) where (of course) old and new are symbols.
:defthm-macro-name lets you name the new macro that will be generated for proving theorems by inducting with the flag function. By default it is named defthm-[flag-function-name], i.e., for the above example, it would be called defthm-flag-pseudo-termp.
:flag-var specifies the name of the variable to use for the flag. By default it is just called flag, and we rarely change it. To be more precise, it is pkg::flag where pkg is the package of the new flag function's name; usually this means you don't have to think about the package.
:ruler-extenders lets you give a value for the ACL2::ruler-extenders of the new flag function.
:body is nil by default, specifying that the original definition is used when extracting the body of each function. The most recent definition rule is used if :body is :last. Otherwise :body should be a list with members of the form (fn1 fn2), indicating that the definition associated with a rule named fn2, if there is one, should be used as the definition for the function symbol, fn1 — and in that case, the formal parameters list specified by fn2 must equal the formal parameters list for fn1. See the community book books/tools/flag-tests.lisp for an example of using such a alist for :body, in particular for the purpose of using definitions installed with ACL2::install-not-normalized.
:expand-with-original-defs slightly changes the hints given to the theorem proving that each invocation of the new flag function is equal to the appropriate call of one of the functions of the clique. After induction on the flag function, this theorem uses an expand hint on any call in the conclusion of one of the functions. Normally it doesn't specify what definition to expand with, but if the :expand-with-original-defs keyword is given then it says to expand with the function symbol itself (i.e., the function's original definition) in each case. This helps in cases where the proof is disrupted by some other definition rule.

Proving Theorems with make-flag

To prove an inductive theorem about a mutually-recursive function, you usually have to effectively prove a single, big, ugly formula that has a different case about each function in the clique.

Normally, even with the flag function written for you, this would be a tedious process. Here is an example of how you might prove by induction that pseudo-termp and pseudo-term-listp return Booleans:

;; ACL2 can prove these are Booleans even without induction due to
;; type reasoning, so for illustration we'll turn these off so that
;; induction is required:

(in-theory (disable (:type-prescription pseudo-termp)
                    (:type-prescription pseudo-term-listp)
                    (:executable-counterpart tau-system)))

;; Main part of the proof, ugly lemma with cases.  Note that we
;; have to use :rule-classes nil here because this isn't a valid
;; rewrite rule.

(local (defthm crux
         (cond ((equal flag 'term)
                (booleanp (pseudo-termp x)))
               ((equal flag 'list)
                (booleanp (pseudo-term-listp lst)))
               (t
                t))
         :rule-classes nil
         :hints(("Goal" :induct (flag-pseudo-termp flag x lst)))))

;; Now we have to re-prove each part of the lemma so that we can use
;; it as a proper rule.

(defthm type-of-pseudo-termp
  (booleanp (pseudo-termp x))
  :rule-classes :type-prescription
  :hints(("Goal" :use ((:instance crux (flag 'term))))))

(defthm type-of-pseudo-term-listp
  (booleanp (pseudo-term-listp lst))
  :rule-classes :type-prescription
  :hints(("Goal" :use ((:instance crux (flag 'list))))))

Obviously this is tedious and makes you say everything twice. Since the steps are so standard, make-flag automatically gives you a macro to automate the process. Here's the same proof, done with the new macro:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp x))
    :rule-classes :type-prescription
    :flag term)
  (defthm type-of-pseudo-term-listp
    (booleanp (pseudo-term-listp lst))
    :rule-classes :type-prescription
    :flag list))

It's worth understanding some of the details of what's going on here.

The macro automatically tries to induct using the induction scheme. But this only works if you're using the formals of the flag function as the variable names in the theorems. In the case of pseudo-termp, this is pretty subtle: ACL2's definition uses different variables for the term/list cases, i.e.,

(mutual-recursion
 (defun pseudo-termp (x) ...)
 (defun pseudo-term-listp (lst) ...))

So the theorem above only works without hints because we happened to choose x and lst as our variables. If, instead, we wanted to use different variable names in our theorems, we'd have to give an explicit induction hint. For example:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp term))
    :rule-classes :type-prescription
    :flag term)
  (defthm type-of-pseudo-term-listp
    (booleanp (pseudo-term-listp termlist))
    :rule-classes :type-prescription
    :flag list)
  :hints(("Goal" :induct (flag-pseudo-termp flag term termlist))))

Bells and Whistles

New! Proof Templates. You can submit, e.g., (defthm-pseudo-termp), with no arguments, to print a ``template'' that is similar to the above form. This can be a convenient starting place for writing down a new theorem.

Localizing Theorems. Sometimes you may only want to export one of the theorems. For instance, if we only want to add a rule about the term case, but no the list case, we could do this:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp x))
    :rule-classes :type-prescription
    :flag term)
  (defthm type-of-pseudo-term-listp
    (booleanp (pseudo-term-listp lst))
    :flag list
    :skip t))

Irrelevant Cases. Sometimes the theorem you want is inductive in such a way that some functions are irrelevant; nothing needs to be proved about them in order to prove the desired theorem about the others. The :skip keyword can be used with a theorem of T to do this:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp x))
    :rule-classes :type-prescription
    :flag term)
  (defthm type-of-pseudo-term-listp
    t
    :flag list
    :skip t))

Alternatively, you can provide the :skip-others keyword to the top-level macro and simply leave out the trivial parts:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp x))
    :rule-classes :type-prescription
    :flag term)
  :skip-others t)

Multiple Theorems. You may have more than one defthm form for a given flag. For the main inductive proof, these are all simply conjoined together (and their hints are simply appended together), but they are exported as separate theorems and may have different :rule-classes.

Legacy Syntax. There is an older, alternate syntax for make-flag that is still available. To encourage transitioning to the new syntax, the old syntax is not documented and should not be used. Support for the old syntax will eventually be removed. If you are maintaining legacy code that still uses the old syntax, see the comments in flag.lisp for some details.

Advanced Hints

For advanced users, note that each individual "theorem" can have its own computed hints. For instance we can write:

(defthm-pseudo-termp
  (defthm type-of-pseudo-termp
    (booleanp (pseudo-termp term))
    :rule-classes :type-prescription
    :flag term
    :hints ('(:expand ((pseudo-termp x)))))
  (defthm type-of-pseudo-term-listp
    (booleanp (pseudo-term-listp termlist))
    :rule-classes :type-prescription
    :flag list
    :hints ('(:expand ((pseudo-term-listp lst)))))
  :hints(("Goal" :induct (flag-pseudo-termp flag term termlist))))

These hints are used during the mutually inductive proof. Under the top-level induction, we check the clause for the current subgoal to determine the hypothesized setting of the flag variable, and provide the computed hints for the appropriate case.

If you provide both a top-level hints form and hints on some or all of the separate theorems, both sets of hints have an effect; try :trans1 on such a defthm-flag-fn form to see what you get.

You may use subgoal hints as well as computed hints, but they will not have any effect if the particular subgoal does not occur when those hints are in effect. We simply translate subgoal hints to computed hints:

("Subgoal *1/5.2" :in-theory (theory 'foo))
  --->
(and (equal id (parse-clause-id "Subgoal *1/5.2"))
     '(:in-theory (theory 'foo)))

As mentioned above, if there is more than one defthm form for a given flag, the hints for all such forms are simply appended together; the hints given to one such form may affect what you might think of as the proof of another.