SPLITTER

Major Section:  MISCELLANEOUS

The application of a rule to a term may cause a goal to simplify to more than one subgoal. A rule with such an application is called a ``splitter''. Here, we explain the output produced for splitters when proof output is enabled (see set-inhibit-output-lst) and such reporting is turned on (as it is by default) -- that is, when the value of (splitter-output) is true.

See set-splitter-output for how to turn off, or on, the reporting of splitters. Also see set-case-split-limitations for information on how to control case splits.

We begin by describing three types of splitters.

if-intro: The rule application may have introduced a call of IF, in the sense discussed at the end below.

case-split: For the application of a rule with hypothesis of the form (case-split <hyp>), <hyp> did not simplify to true or false.

immed-forced: For the application of a rule with hypothesis of the form (force <hyp>), <hyp> did not simplify to true or false, where immediate-force-modep is enabled (see immediate-force-modep).

These three annotations -- if-intro, case-split, and immed-forced -- may be used in proof output and summaries for describing rule applications, as discussed below. A fourth annotation, forced, maybe also be used in proof output to indicate the application of a rule with hypothesis of the form (force <hyp>) when <hyp> did not simplify to true or false, where immediate-force-modep is disabled (see immediate-force-modep). We don't consider such uses of force to be splitters, because they do not cause case splits (though they do produce goals to prove after lower-case ``q.e.d.'' is printed); see force.

There are three kinds of output affected by splitters, illustrated in turn below using examples.

(a) During the proof, gag-mode off
(b) During the proof, gag-mode on
(c) Summary

Of course, (a) and (b) are skipped if proof output is inhibited, which (c) is skipped if summary output is inhibited; see set-inhibit-output-lst.

(a) During the proof, gag-mode off

With gag-mode off (or when using :pso, :psof, or :psog) one normally gets an English commentary. The following output indicates that at least one application of each rule F and G is of type if-intro, at least one application of rules G and R1 are of type case-split, and at least one application of rule R3 is of type immed-forced. If immediate-force-modep is off then ``immed-forced'' would be replaced by ``forced''.

  This simplifies, using the :definitions F (if-intro), G (case-split and
  if-intro) and H and the :rewrite rules R1, R2 (case-split), and
  R3 (immed-forced), to the following two conjectures.

Note that any such printing of ``forced'' is done even if (splitter-output) is false. Such forcing indication is also made when raw proof format is used -- see set-raw-proof-format -- but in that case, no indication is made for splitters in the proof output.

(b) During the proof, gag-mode on

With gag-mode on the proof output is greatly abbreviated. However, ``Splitter Notes'' are printed so that even with gag-mode on, one can get important information to help control large case splits, by disabling splitter rules as appropriate. These are printed at the point when a goal splits into subgoals. Here, for example, is the Splitter Note that corresponds to the output shown in (a) above. It shows the goal whose simplification has produced a split into more than one subgoal, and it shows how many subgoals have been created.

Splitter note (see :DOC splitter) for Subgoal *1/2.2.1' (2 subgoals).
  case-split: ((:DEFINITION G) (:REWRITE R2))
  immed-forced: ((:REWRITE R3))
  if-intro: ((:DEFINITION G) (:DEFINITION F))

(c) Summary

Here is a possible summary corresponding to our running example. In the summary, ``Splitter rules'' is omitted if there are no splitter rules, and a splitter type is only mentioned if there is at least one corresponding splitter rule.

Summary
Form:  ( THM ...)
Rules: ((:DEFINITION F)
        (:DEFINITION G)
        (:DEFINITION H)
        (:REWRITE R1)
        (:REWRITE R2)
        (:REWRITE R3))
Splitter rules (see :DOC splitter):
  case-split: ((:DEFINITION G) (:REWRITE R2))
  immed-forced: ((:REWRITE R3))
  if-intro: ((:DEFINITION G) (:DEFINITION F))
Time:  0.01 seconds (prove: 0.00, print: 0.00, other: 0.00)
Prover steps counted:  145

We conclude by giving the criteria for a rewrite or definition rule application to be a splitter of type if-intro.

o Reporting of splitter rules is on, i.e., the value of (splitter-output) is true.

o At least two subgoals are created, even before considering subgoals generated by hypotheses that are calls of case-split or force.

o The term to which the rule is applied is at the top level, rather than being encountered when trying to establish the hypothesis of a rule.

o The rule is a rewrite rule, a definition rule, or a meta rule.

o There is a call of the function symbol IF in the right-hand side of the rewrite rule; or, in the case of a definition rule, in the body of the definition; or, in the case of a meta rule, in the result of applying the metafunction.

o There is a call of the function symbol IF in the result of rewriting: the right-hand side (for a rewrite rule), the definition body (for a definition rule), or the metafunction application (for a meta rule).

Any rule application meeting the above criteria will be considered a splitter of type if-intro, even if the call does not actually cause a case split. For example, if you are proving (implies (hyp x) (conc x)) and rule R rewrites (hyp x) to (if (h1 x) (h2 x) nil), which is really the term (and (h1 x) (h2 x)), then R may be labelled as a splitter rule. If you want to find the causes of case-splitting, the list of if-intro splitters can help you narrow your search, but may include irrelevant rules as well.

Finally, note that you may see splits not attributed to splitters. We believe that this will be uncommon during simplification, though it can occur for example when a call of IF is in the body of a LET expression, i.e., in a call of a LAMBDA expression. But splits caused by other processes, notably destructor elimination (see elim), will typically not be attributed to splitters.