INDUCTION

Major Section:  RULE-CLASSES

Example:
(:induction :corollary t  ; the theorem proved is irrelevant!
            :pattern (* 1/2 i)
            :condition (and (integerp i) (>= i 0))
            :scheme (recursion-by-sub2 i))

In ACL2, as in Nqthm, the functions in a conjecture ``suggest'' the inductions considered by the system. Because every recursive function must be admitted with a justification in terms of a measure that decreases in a well-founded way on a given set of ``controlling'' arguments, every recursive function suggests a dual induction scheme that ``unwinds'' the function from a given application.

For example, since append (actually binary-append, but we'll ignore the distinction here) decomposes its first argument by successive cdrs as long as it is a non-nil true list, the induction scheme suggested by (append x y) has a base case supposing x to be either not a true list or to be nil and then has an induction step in which the induction hypothesis is obtained by replacing x by (cdr x). This substitution decreases the same measure used to justify the definition of append. Observe that an induction scheme is suggested by a recursive function application only if the controlling actuals are distinct variables, a condition that is sufficient to ensure that the ``substitution'' used to create the induction hypothesis is indeed a substitution and that it drives down a certain measure. In particular, (append (foo x) y) does not suggest an induction unwinding append because the induction scheme suggested by (append x y) requires that we substitute (cdr x) for x and we cannot do that if x is not a variable symbol.

Once ACL2 has collected together all the suggested induction schemes it massages them in various ways, combining some to simultaneously unwind certain cliques of functions and vetoing others because they ``flaw'' others. We do not further discuss the induction heuristics here; the interested reader should see Chapter XIV of A Computational Logic (Boyer and Moore, Academic Press, 1979) which represents a fairly complete description of the induction heuristics of ACL2.

However, unlike Nqthm, ACL2 provides a means by which the user can elaborate the rules under which function applications suggest induction schemes. Such rules are called :induction rules. The definitional principle automatically creates an :induction rule, named (:induction fn), for each admitted recursive function, fn. It is this rule that links applications of fn to the induction scheme it suggests. Disabling (:induction fn) will prevent fn from suggesting the induction scheme derived from its recursive definition. It is possible for the user to create additional :induction rules by using the :induction rule class in defthm.

Technically we are ``overloading'' defthm by using it in the creation of :induction rules because no theorem need be proved to set up the heuristic link represented by an :induction rule. However, since defthm is generally used to create rules and rule-class objects are generally used to specify the exact form of each rule, we maintain that convention and introduce the notion of an :induction rule. An :induction rule can be created from any lemma whatsoever.

General Form of an :induction Lemma or Corollary:
T


General Form of an :induction rule-class:
(:induction :pattern pat-term
            :condition cond-term
            :scheme scheme-term)

The induction rule created is used as follows. When an instance of the :pattern term occurs in a conjecture to be proved by induction and the corresponding instance of the :condition term is known to be non-nil (by type reasoning alone), the corresponding instance of the :scheme term is created and the rule ``suggests'' the induction, if any, suggested by that term. If rec-fn is recursive, then the suggestion is the one that unwinds that recursion.

Consider, for example, the example given above,

(:induction :pattern (* 1/2 i)
            :condition (and (integerp i) (>= i 0))
            :scheme (recursion-by-sub2 i)).

(defun recursion-by-sub2 (i)
  (if (and (integerp i)
           (< 1 i))
      (recursion-by-sub2 (- i 2))
      t))

(and (implies (not (and (integerp i) (< 1 i)))   ; base case
              (:p i))
     (implies (and (and (integerp i) (< 1 i))    ; induction step
                   (:p (- i 2)))
              (:p i)))

Suppose the above :induction rule has been added. Then an occurrence of, say, (* 1/2 k) in a conjecture to be proved by induction would suggest, via this rule, an induction on k by twos, provided k was known to be a nonnegative integer. This is because the induction rule's :pattern is matched in the conjecture, its :condition is satisfied, and the :scheme suggested by the rule is that derived from (recursion-by-sub2 k), which is induction on k by twos. Similarly, the term (* 1/2 (length l)) would suggest no induction via this rule, even though the rule ``fires'' because it creates the :scheme (recursion-by-sub2 (length l)) which suggests no inductions unwinding recursion-by-sub2 (since the controlling argument of recursion-by-sub2 in this :scheme is not a variable symbol).

Continuing this example one step further illustrates the utility of :induction rules. We could define the function recursion-by-cddr that suggests the induction scheme decomposing its consp argument two cdrs at a time. We could then add the :induction rule linking (* 1/2 (length x)) to (recursion-by-cddr x) and arrange for (* 1/2 (length l)) to suggest induction on l by cddr.

Observe that :induction rules require no proofs to be done. Such a rule is merely a heuristic link between the :pattern term, which may occur in conjectures to be proved by induction, and the :scheme term, from which an induction scheme may be derived. Hence, when an :induction rule-class is specified in a defthm event, the theorem proved is irrelevant. The easiest theorem to prove is, of course, t. Thus, we suggest that when an :induction rule is to be created, the following form be used:

(defthm name T
  :rule-classes ((:induction :pattern pat-term
                             :condition cond-term
                             :scheme scheme-term)))