advice on case explosion in complex inductions

Recursive functions suggest inductions based on the case analysis in the function definition and the positions of recursive calls within that case analysis. That analysis is done when termination is proved. Key parts of that analysis are the notions of governing tests and ruling tests. By using the so-called ``ruler-extenders'' feature of termination analysis you can sometimes choose between ``coarse-grained'' and ``fine-grained'' inductions. The former have few cases but may provide multiple and sometimes irrelevant induction hypotheses. The latter provide more cases, each targeted at a given output, and tend to provide only induction hypotheses needed for that output. See rulers for a discussion of ruler-extenders.

Roughly speaking, a test *governs* a recursive call if the test must
be true for control to reach that call. The *ruling* tests are a subset
of the governing tests and are the ones that determine the case analysis of
any suggested induction.

For example, if we are analyzing a definition of

The default setting of ruler-extenders is `let` and `let*`
expressions, which arise frequently in interesting recursive functions
because they facilitate *code sharing* by allowing the computation of
intermediate results used on multiple output branches.) When the analysis
encounters a term considered a tip, the rulers collected so far are used to
rule *all* the recursive calls in that tip. So at a tip, the analysis
collects all the recursive calls occurring in that tip and forms measure
conjectures and, eventually, induction hypotheses about them, using the
rulers as the hypotheses of those conjectures.

So the user can influence the determination of the rulers by setting the
``ruler-extenders'' in effect when the function is admitted. The global
default ruler-extenders can be set by the event `xargs` keyword

Most often, users think about ruler-extenders only in the context of
*failed* termination proofs: inspection of the measure conjectures
reveal that an important governing hypothesis was curiously omitted, the user
consults the documentation or appeals for help from other users, and is
reminded of ruler-extenders. One could argue that users forget about
ruler-extenders because the default setting for ruler-extenders is so often
the ``right'' one. But sometimes even a function that is successfully
admitted under the default setting would benefit from selecting a non-default
setting for ruler-extenders.

Sometimes you may feel that the prover is struggling with an induction
suggested by a function, even though the function that suggested the
induction is the one you expected to be selected, and for most simple
recursive functions the induction suggested is the ``perfect'' induction for
that function. This problem of the prover struggling to simplify the
induction steps might arise most commonly with functions that have `let*` bindings that contain

(defun fn (x y) (if (consp x) (let* ((y1 (if (consp (car x)) (fn (car x) (cons 'car y)) y)) (y2 (if (consp (cdr x)) (fn (cdr x) (cons 'cdr y1)) y1))) (cons y1 y2)) y))

Recall that

(defun fn (x y) (if (consp x) ((lambda (y1 x) ((lambda (y2 y1) (cons y1 y2)) (if (consp (cdr x)) (fn (cdr x) (cons 'cdr y1)) y1) y1)) (if (consp (car x)) (fn (car x) (cons 'car y)) y) x) y))

So, the entire

(fn (car x) (cons 'car y))

and

(fn (cdr x) (cons 'cdr (if (consp (car x)) (fn (car x) (cons 'car y)) y))).

The default measure in this definition is

Now consider how the prover would attempt to prove

(and (implies (not (consp x)) (p (fn x y))) (implies (and (consp x) (p (fn (car x) (cons 'car y))) (p (fn (cdr x) (cons 'cdr (if (consp (car x)) (fn (car x) (cons 'car y)) y))))) (p (fn x y)))).

**Note**: Here and throughought this documentation topic we freely
rearrange the formulas we display to make it easier to compare different
induction schemes. For example, when the prover attempts to prove

The prover attempts to reduce each of these two conjuncts to

(implies (and (consp x)ind-hyp1ind-hyp2)ind-concl)

where, *ind-hyp1*, the first induction hypothesis, is *ind-concl*, the two
induction hypotheses will have been rewritten, making them easier to find and
identify as true if they occur in the rewriting of the conclusion.

But rewriting *ind-hyp1* here will involve rewriting *ind-concl*. In particular, inspection of

Another way to describe the unfortunate induction scheme above is that it
``coarse,'' because it provides a simple case analysis, which necessitates
lumping all the possibly relevant induction hypotheses into a single case (in
this particular example). When the induction conclusion opens, after the
induction hypotheses have all been simplified, it will cause further
splitting, (e.g., on

Depending on how hard it is to rewrite irrelevant induction hypotheses
— which depends not just on the function, like

A finer-grained induction scheme is generated, in the case of *not* to stop the collection of
rulers. This can be done by adding the keyword *any* term beginning with a

If we had defined

(defun fn (x y) (declare (xargs :ruler-extenders :lambdas)) (if (consp x) (let* ((y1 (if (consp (car x)) (fn (car x) (cons 'car y)) y)) (y2 (if (consp (cdr x)) (fn (cdr x) (cons 'cdr y1)) y1))) (cons y1 y2)) y))

Note that

The induction generated is shown below. We have slightly simplified the
induction by replacing *a b c**b* when *a*
is among the hypotheses in the case analysis, and by replacing *a
b c**c* when *a*

(and (implies (not (consp x)) (p (fn x y))) (implies (and (consp x) (not (consp (car x))) (not (consp (cdr x)))) (p (fn x y))) (implies (and (consp x) (not (consp (car x))) (consp (cdr x)) (p (fn (cdr x) (cons 'cdr y)))) (p (fn x y))) (implies (and (consp x) (consp (car x)) (not (consp (cdr x))) (p (fn (car x) (cons 'car y)))) (p (fn x y))) (implies (and (consp x) (consp (car x)) (consp (cdr x)) (p (fn (car x) (cons 'car y))) (p (fn (cdr x) (cons 'cdr (fn (car x) (cons 'car y)))))) (p (fn x y))))

Note that the case analysis here steers the

The finer case analysis gives us two base cases and four induction steps,
one of which has two induction hypotheses. We'll encounter terms of the form

**Note**: The ruler-extenders may include arbitrary function symbols
and the keyword

In the next section we'll discuss a theorem that makes use of these insights and demonstrates that the finer scheme can lead to faster proofs.

The ACL2 prettyprinter is implemented with the function `pe` command, e.g.,

We'll focus here on

A good demonstration of the ``coarse'' and ``fine'' induction schemes for

The book proves that

The coarse induction, generated under the default ruler-extenders, has 76 cases. Six are base cases. The other 70 are induction steps with varying numbers of induction hypotheses as given in the sketch below.

(76 ;; 76 cases in the induction scheme (0 . 6) ;; no induction hyps in 6 cases, i.e., Base Cases (1 . 8) ;; 1 induction hyp in 8 cases (2 . 2) ;; 2 induction hyps in 2 cases (3 . 16) ;; 3 induction hyps in 16 cases (4 . 32) ;; 4 induction hyps in 32 cases (8 . 4) ;; 8 induction hyps in 4 cases (9 . 8)) ;; 9 induction hyps in 8 cases

The fine induction, generated under the

(256 ;; 256 cases in the induction scheme (0 . 6) ;; no induction hyps in 6 cases, i.e., Base Cases (1 . 8) ;; 1 induction hyp in 8 cases (2 . 82) ;; 2 induction hyps in 82 cases (3 . 80) ;; 3 induction hyps in 80 cases (4 . 80)) ;; 4 induction hyps in 80 cases

The induction generated under the

Regardless of which induction scheme we use, the proof that

After noticing the performance differences between the coarse and fine
inductions we spent some time trying to further optimize the proof. We
compared seven different combinations of approaches. We discuss them here.
See the

As mentioned previously, a common situation with inductive proofs about
complicated mutually recursive functions is that the calls in the conclusion
aren't always automatically opened by ACL2's heuristics. So it is not
unusual in such proofs to provide a hint that explicitly expands the

We will also be experimenting with the enabled status of

The seven scenarios are specified by saying which induction scheme is
used, whether

computed — when a subgoal becomes stable, openppr1 andppr1-lst in the conclusion, and when any subgoal of that becomes stable again, enableppr1 andppr1-lst and let ACL2's heuristics take over. This hint only makes sense ifppr1 andppr1-lst are initially disabled.-
computed' — likecomputed but skips the first stable opening ofppr1 andppr1-lst . That is handled instead by an:expand hint. :expand — a traditional:expand hint to openppr1 andppr1-lst terms as they appear in induction conclusions. The expand hint is:expand ((:free (print-base print-radix width rpc state eviscp) (ppr1 x print-base print-radix width rpc state eviscp)) (:free (print-base print-radix width rpc pair-keywords-p state eviscp) (ppr1-lst lst print-base print-radix width rpc pair-keywords-p state eviscp)))

which allows the non-controller arguments ofppr1 andppr1-lst to be any terms but insists that the controllers,x andlst , respectively, be those particular variable names.

In addition, we sometime avail ourselves of special-purpose lemmas.

NIL lem — rewrites(ppr1-lst nil ...) tonil .MAX hack — lemmas aboutMAX allowing us to disableMAX

We try seven different combinations, numbered 1-7, but listed below in descending order of proof times.

n induction status hints proof time 1 coarse enabled :expand 2165.19 2 coarse disabled computed 207.49 6 fine disabled computed 82.29 3 fine enabled :expand 65.00 4 fine disabled computed + :expand 62.86 5 fine disabled computed' + :expand + NIL lem 61.58 7 fine disabled computed + :expand + MAX hack 55.14

Note that scenarios 1 and 3 are a direct comparison of coarse and fine induction with exactly the same hint. The coarse induction took 2165.19 seconds and the fine induction took 65.00, despite the fact that the coarse induction had 76 cases to deal with and the fine induction had 256. The most likely reason the coarse induction performed poorly is that there were 8 induction steps that had 9 induction hypotheses each, even though no case ever actually required more than 4 induction hypotheses.

Scenario 2 shows that much time is saved by disabling

Scenarios 4, 5, 6, and 7, attempt to improve upon the time seen in
scenario 3. We see that the best performance in this particular problem is
to use the fine induction case analysis, keep the relevant recursive
functions disabled by default, use an

However, it should be noted that the major source of improvement is the
use of the fine induction scheme. The fact that there is only a 10% further
improvement achieved by the various other hints suggests it may not be worth
the effort! Coding the computed hint took time and thought, compared to just
using an

Ignoring scenario 7 — where the additional improvement came from a
completely different source, namely, avoidng the expansion of

Of course, whether fine induction schemes will improve other proofs just
depends on how many irrelevant induction hypotheses are present and how
complicated it is to simplify the terms in the theorem. If you are proving
something about a recursive function that contains