HOL: Description

Simplification — simpLib

The simplifier is HOL’s most sophisticated rewriting engine. It is recommended as a general purpose work-horse during interactive theorem-proving. As a rewriting tool, the simplifier’s general role is to apply theorems of the general form $$ \vdash l = r $$ to terms, replacing instances of $l$ in the term with $r$. Thus, the basic simplification routine is a conversion, taking a term $t$, and returning a theorem $\vdash t = t'$, or the exception UNCHANGED.

The basic conversion is

   simpLib.SIMP_CONV : simpLib.simpset -> thm list -> term -> thm

The first argument, a simpset, is the standard way of providing a collection of rewrite rules (and other data, to be explained below) to the simplifier. There are simpsets accompanying most of HOL’s major theories. For example, the simpset bool_ss in boolSimps embodies all of the usual rewrite theorems one would want over boolean formulas:

> SIMP_CONV bool_ss [] ``p /\ T \/ ~(q /\ r)``;
val it = ⊢ p ∧ T ∨ ¬(q ∧ r) ⇔ p ∨ ¬q ∨ ¬r: thm

In addition to rewriting with the obvious theorems, bool_ss is also capable of performing simplifications that are not expressible as simple theorems:

> SIMP_CONV bool_ss [] ``?x. (\y. P (f y)) x /\ (x = z)``;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = ⊢ (∃x. (λy. P (f y)) x ∧ x = z) ⇔ P (f z): thm

In this example, the simplifier performed a $\beta$-reduction in the first conjunct under the existential quantifier, and then did an “unwinding” or “one-point” reduction, recognising that the only possible value for the quantified variable x was the value z.

The second argument to SIMP_CONV is a list of theorems to be added to the provided simpset, and used as additional rewrite rules. In this way, users can temporarily augment standard simpsets with their own rewrites. If a particular set of theorems is often used as such an argument, then it is possible to build a simpset value to embody these new rewrites.

For example, the rewrite arithmeticTheory.LEFT_ADD_DISTRIB, which states that $p(m + n) = pm + pn$ is not part of any of HOL’s standard simpsets. This is because it can cause an unappealing increase in term size (there are two occurrences of $p$ on the right hand side of the theorem). Nonetheless, it is clear that this theorem may be appropriate on occasion:

> open arithmeticTheory;   ... output elided ...
> SIMP_CONV bossLib.arith_ss [LEFT_ADD_DISTRIB] ``p * (n + 1)``;
val it = ⊢ p * (n + 1) = p + n * p: thm

Note how the arith_ss simpset has not only simplified the intermediate (p * 1) term, but also re-ordered the addition to put the simpler term on the left, and sorted the multiplication’s arguments.

High-Level Simplification Tactics

The simplifier is implemented around the conversion SIMP_CONV introduced above. This is a function for “converting” terms into theorems. To apply the simplifier to goals (alternatively, to perform tactic-based proofs with the simplifier), HOL provides a number of tactics, all of which are available in bossLib. These tactics divide into two classes.

The first and more commonly used class is of high-level tactics used in the form $$ \mathtt{tactic\_name}[\mathit{th}_1,\dots,\mathit{th}_n] $$ where the various $\mathit{th}_i$ are theorems that are passed to the simplifier and used as additional rewrites. There is a simpset used here, but it is implicit: the global, “stateful” simpset, embodying all of a theory and a theory’s ancestors’ useful simplification technology. For more on the stateful simpset, see Section 8.5.3.5 below.

The commonly used tactics of this sort are simp, rw, fs and gs. All of these tactics use the stateful simpset, and (by default), add the arithmetic decision procedure for $\mathbb{N}$, as well as a handling of let-terms that turns let x = v in M into M with free occurrences of x replaced by v.

The exact behaviour of these tactics can be further adjusted with the use of special theorem forms, described below in Section 8.5.6.4.

simp : thm list -> tactic

A call to simp[$\mathit{th}_1,\dots,\mathit{th}_n$] simplifies the current goal, using the augmented stateful simpset described above, as well as the theorems passed in the argument list. Finally, all of the goal’s assumptions are also used as a source of rewrites. When an assumption is used by simp, it is converted into rewrite rules in the same way as theorems passed in the list given as the tactic’s argument. For example, an assumption ~P will be treated as the rewrite |- P = F.

> g ‘x < 3 /\ P x ==> x < 20 DIV 2’;   ... output elided ...
> e (simp[]);
OK..
val it =
   Initial goal proved.
   ⊢ x < 3 ∧ P x ⇒ x < 20 DIV 2: proof

The simp tactic is implemented with the low-level tactic asm_simp_tac (described below).

rw : thm list -> tactic

A call to rw[$\mathit{th}_1,\dots,\mathit{th}_n$] is similar in behaviour to simp with the same arguments but does its simplification while interleaving phases of aggressive “goal-stripping”. In particular, rw begins by stripping all outermost universal quantifiers and conjunctions. It follows this with elimination of variables v that appear in assumptions of the form v = e or e = v (where v cannot be free in e). After a phase of simplification (as per simp), the rw tactic then does a case-split on all free if-then-else subterms within the goal, strips away universal quantifiers, implications and conjunctions (à la STRIP_TAC), and then simplifies equalities involving data type constructors in the assumptions and goal. (Such equalities will simplify to falsity if the constructors are different, or will simplify with an injectivity result.)

This last phase of stripping may result in a goal that could simplify yet further but there is no final simplification to catch this possibility. Despite peculiarities such as this, rw is often a useful way to simplify and remove unnecessary propositional structure.

The rw tactic performs the same mixture of simplification and goal-splitting as the low-level tactic rw_tac.

gs : thm list -> tactic

The gs tactic (where “gs” should be read as “global simplification”) simplifies both the assumptions of a goal as well as its conclusion. The assumptions are repeatedly simplified with respect to each other, meaning that the process begins by simplifying the oldest assumption with all the other (newer) assumptions available as possible rewrites. Then, the next oldest assumption is simplified, using all the other assumptions (including the just-simplified oldest assumption). This process passes through the list of all assumptions and then repeats if any of the assumptions changed. When no further change occurs among the assumptions, all of the assumptions are used to simplify the goal’s conclusion.

When an assumption $A_i$ is simplified, a theorem of the form $\vdash A_i \Leftrightarrow A_i'$ is produced. Then $A_i'$ is added to the goal as a new assumption, using the theorem-tactical strip_assume_tac. This latter will (recursively) split conjunctions into multiple assumptions (i.e., an assumption $p \land q$ will turn into two assumptions, $p$ and $q$), will cause a case-split if the assumption is a disjunction, and will choose fresh variable names to eliminate existential quantifiers. If this “stripping” is not desired, the gns variant of gs can be used (‘n’ for “no strip”).

It can often be useful to eliminate variable equalities among assumptions (as is done by rw above). If this behaviour is also desired, the gvs variant can be used. The gnvs tactic, which combines both options, is also available.

Finally, the rgs variant sweeps through the assumption list in the opposite order, simplifying the newest assumption first.

fs : thm list -> tactic

The fs tactic is similar to gs in that it simplifies not only a goal’s conclusion but its assumptions as well.

It simplifies each assumption in turn, additionally using earlier assumptions in the simplification of later assumptions. After being simplified, each assumption is added back into the goal’s assumption list with the strip_assume_tac theorem-tactical.

fs attacks the assumptions in the order in which they appear in the list of terms that represent the goal’s assumptions. Typically then, the first assumption to be simplified will be the assumption most recently added. Viewed in the light of goalstackLib’s printing of goals, FULL_SIMP_TAC works its way up the list of assumptions, from bottom to top.

Unlike gs, the fs tactic makes exactly one pass over the assumptions before proceeding to simplify the goal. Though this is in principle more efficient, this comes at the cost of frequently being annoying to use. As with gs, there is an rfs variant to this tactic, which simplifies the goal’s assumptions in reverse order (but again, only once).

The fs tactic is based on the low-level tactic full_simp_tac.

Low-Level Simplification Tactics

The second class of simplification tactics are more primitive and explicitly take a simpset as an argument. This ability to specify a simpset to use allows for finer-grained control of just what the tactic will do. In particular, the bool_ss simpset is relatively common as an argument to these tactics precisely because it does so little.

All these tactics have upper-case aliases (e.g., SIMP_TAC and simp_tac are the same function). It is up to the user to decide which they prefer to see in their proof scripts.

simp_tac : simpset -> thm list -> tactic

The tactic simp_tac is the simplest simplification function: it attempts to simplify the current goal (ignoring the assumptions) using the given simpset and the additional theorems. It is little more than the lifting of the underlying SIMP_CONV conversion to the tactic level through the use of the standard function CONV_TAC.

asm_simp_tac : simpset -> thm list -> tactic

Like simp_tac, asm_simp_tac simplifies the current goal (leaving the assumptions untouched), but includes the goal’s assumptions as extra rewrite rules. Thus:

OK..
1 subgoal:
val it =
   
    0.  x = 3
   ------------------------------------
        P x

> e (asm_simp_tac bool_ss []);
OK..
1 subgoal:
val it =
   
    0.  x = 3
   ------------------------------------
        P 3

In this example, asm_simp_tac used x = 3 as an additional rewrite rule, and replaced the x of P x with 3. When an assumption is used by asm_simp_tac it is converted into rewrite rules in the same way as theorems passed in the list given as the tactic’s second argument. For example, an assumption ~P will be treated as the rewrite |- P = F.

full_simp_tac : simpset -> thm list -> tactic

The tactic full_simp_tac simplifies not only a goal’s conclusion but its assumptions as well. It proceeds by simplifying each assumption in turn, additionally using earlier assumptions in the simplification of later assumptions. After being simplified, each assumption is added back into the goal’s assumption list with the strip_assume_tac theorem-tactical. This means that assumptions that become conjunctions will have each conjunct assumed separately. Assumptions that become disjunctions will cause one new sub-goal to be created for each disjunct. If an assumption is simplified to false, this will solve the goal.

The full_simp_tac tactic attacks the assumptions in the order in which they appear in the list of terms that represent the goal’s assumptions. Typically then, the first assumption to be simplified will be the assumption most recently added. Viewed in the light of goalstackLib’s printing of goals, full_simp_tac works its way up the list of assumptions, from bottom to top.

The following demonstrates a simple use of full_simp_tac:

OK..
1 subgoal:
val it =
   
    0.  f x < 10
    1.  x = 4
   ------------------------------------
        4 + x < 10

> e (full_simp_tac bool_ss []);
OK..
1 subgoal:
val it =
   
    0.  f 4 < 10
    1.  x = 4
   ------------------------------------
        4 + 4 < 10

In this example, the assumption x = 4 caused the x in the assumption f x < 10 to be replaced by 4. The x in the goal was similarly replaced. If the assumptions had appeared in the opposite order, only the x of the goal would have changed.

The next session demonstrates more interesting behaviour:

OK..
1 subgoal:
val it =
   
    0.  x ≤ 4
   ------------------------------------
        f x + 1 < 10

> e (full_simp_tac bool_ss [arithmeticTheory.LESS_OR_EQ]);
OK..
2 subgoals:
val it =
   
    0.  x = 4
   ------------------------------------
        f 4 + 1 < 10
   
    0.  x < 4
   ------------------------------------
        f x + 1 < 10

In this example, the goal was rewritten with the theorem stating $$ \vdash x \leq y \iff x < y \lor x = y $$ Turning the assumption into a disjunction resulted in two sub-goals. In the second of these, the assumption x = 4 further simplified the rest of the goal.

rw_tac : simpset -> thm list -> tactic

Though its type is the same as the simplification tactics already described, rw_tac is “augmented” in two ways:

• When simplifying the goal, the provided simpset is augmented not only with the theorems explicitly passed in the second argument, but also with all of the rewrite rules from the TypeBase, as well as with the goal’s assumptions. These rewrites include results about record field selectors and updators, as well as distinctness and injectivity theorems for data type constructors.
• rw_tac also repeatedly “strips” the goal in the same way as the high-level rw tactic (see above).

The augmentation of the provided simpset that occurs before rw_tac does any simplification work can be slow when the TypeBase is large.

The standard simpsets

HOL comes with a number of standard simpsets. All of these are accessible from within bossLib, though some originate in other structures.

pure_ss and bool_ss

The pure_ss simpset (defined in structure pureSimps) contains no rewrite theorems at all, and plays the role of a blank slate within the space of possible simpsets. When constructing a completely new simpset, pure_ss is a possible starting point. The pure_ss simpset has just two components: congruence rules for specifying how to traverse terms, and a function that turns theorems into rewrite rules. Congruence rules are further described in Section 8.5.6; the generation of rewrite rules from theorems is described in Section 8.5.5.3.

The bool_ss simpset (defined in structure boolSimps) is often used when other simpsets might do too much. It contains rewrite rules for the boolean connectives, and little more. It contains all of the de Morgan theorems for moving negations in over the connectives (conjunction, disjunction, implication and conditional expressions), including the quantifier rules that have $\neg(\forall x.\,P(x))$ and $\neg(\exists x.\,P(x))$ on their left-hand sides. It also contains the rules specifying the behaviour of the connectives when the constants T and F appear as their arguments. (One such rule is |- T /\ p = p.)

As in the example above, bool_ss also performs $\beta$-reductions and one-point unwindings. The latter turns terms of the form $$ \exists x.\;P(x)\land\dots x = e \dots\land Q(x) $$ into $$ P(e) \land \dots \land Q(e) $$ Similarly, unwinding will turn $\forall x.\;x = e \Rightarrow P(x)$ into $P(e)$.

Finally, bool_ss also includes congruence rules that allow the simplifier to make additional assumptions when simplifying implications and conditional expressions. This feature is further explained in Section 8.5.5 below, but can be illustrated by some examples (the first also demonstrates unwinding under a universal quantifier):

> SIMP_CONV bool_ss [] “!x. (x = 3) /\ P x ==> Q x /\ P 3”;
val it = ⊢ (∀x. x = 3 ∧ P x ⇒ Q x ∧ P 3) ⇔ P 3 ⇒ Q 3: thm

> SIMP_CONV bool_ss [] “if x <> 3 then P x else Q x”;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ (if x ≠ 3 then P x else Q x) = if x ≠ 3 then P x else Q 3: thm

std_ss

The std_ss simpset is defined in bossLib, and adds rewrite rules pertinent to the types of sums, pairs, options and natural numbers to bool_ss.

> SIMP_CONV std_ss [] “FST (x,y) + OUTR (INR z)”;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = ⊢ FST (x,y) + OUTR (INR z) = x + z: thm

> SIMP_CONV std_ss [] “case SOME x of NONE => P | SOME y => f y”;
<<HOL message: inventing new type variable names: 'a, 'b>>
val it = ⊢ (case SOME x of NONE => P | SOME y => f y) = f x: thm

With the natural numbers, the std_ss simpset can calculate with ground values, and also includes a suite of “obvious rewrites” for formulas including variables.

> SIMP_CONV std_ss [] “P (0 <= x) /\ Q (y + x - y)”;
val it = ⊢ P (0 ≤ x) ∧ Q (y + x − y) ⇔ P T ∧ Q x: thm

> SIMP_CONV std_ss [] “23 * 6 + 7 ** 2 - 31 DIV 3”;
val it = ⊢ 23 * 6 + 7² − 31 DIV 3 = 177: thm

arith_ss

The arith_ss simpset (defined in bossLib) extends std_ss by adding the ability to decide formulas of Presburger arithmetic, and to normalise arithmetic expressions (collecting coefficients, and re-ordering summands). The underlying natural number decision procedure is that described in Section 8.8 below.

These two facets of the arith_ss simpset are demonstrated here:

> SIMP_CONV arith_ss [] ``x < 3 /\ P x ==> x < 20 DIV 2``;
val it = ⊢ x < 3 ∧ P x ⇒ x < 20 DIV 2 ⇔ T: thm

> SIMP_CONV arith_ss [] ``2 * x + y - x + y``;
val it = ⊢ 2 * x + y − x + y = x + 2 * y: thm

Note that subtraction over the natural numbers works in ways that can seem unintuitive. In particular, coefficient normalisation may not occur when first expected:

> SIMP_CONV arith_ss [] ``2 * x + y - z + y``;
Exception- UNCHANGED raised

Over the natural numbers, the expression $2 x + y - z + y$ is not equal to $2 x + 2 y - z$. In particular, these expressions are not equal when $2x + y < z$.

list_ss

The last pure simpset value in bossLib, list_ss adds rewrite theorems about the type of lists to arith_ss. These rewrites include the obvious facts about the list type’s constructors NIL and CONS, such as the fact that CONS is injective:

   (h1 :: t1 = h2 :: t2) = (h1 = h2) /\ (t1 = t2)

Conveniently, list_ss also includes rewrites for the functions defined by primitive recursion over lists. Examples include MAP, FILTER and LENGTH. Thus:

> SIMP_CONV list_ss [] ``MAP (\x. x + 1) [1;2;3;4]``;
val it = ⊢ MAP (λx. x + 1) [1; 2; 3; 4] = [2; 3; 4; 5]: thm

> SIMP_CONV list_ss [] ``FILTER (\x. x < 4) [1;2;y + 4]``;
val it = ⊢ FILTER (λx. x < 4) [1; 2; y + 4] = [1; 2]: thm

> SIMP_CONV list_ss [] ``LENGTH (FILTER ODD [1;2;3;4;5])``;
val it = ⊢ LENGTH (FILTER ODD [1; 2; 3; 4; 5]) = 3: thm

These examples demonstrate how the simplifier can be used as a general purpose symbolic evaluator for terms that look a great deal like those that appear in a functional programming language. Note that this functionality is also provided by computeLib (see Section 8.6 below); computeLib is more efficient, but less general than the simplifier. For example:

> EVAL ``FILTER (\x. x < 4) [1;2;y + 4]``;
val it =
   ⊢ FILTER (λx. x < 4) [1; 2; y + 4] =
     1::2::if y + 4 < 4 then [y + 4] else []: thm

The "stateful" simpset — srw_ss()

The last simpset exported by bossLib is hidden behind a function. The srw_ss value has type unit -> simpset, so that one must type srw_ss() in order to get a simpset value. This use of a function type allows the underlying simpset to be stored in an SML reference, and allows it to be updated dynamically. In this way, referential transparency is deliberately broken. All of the other simpsets will always behave identically: SIMP_CONV\ bool_ss is the same simplification routine wherever and whenever it is called.

In contrast, srw_ss is designed to be updated. When a theory is loaded, when a new type is defined, the value behind srw_ss() changes, and the behaviour of SIMP_CONV applied to (srw_ss()) changes with it. The design philosophy behind srw_ss is that it should always be a reasonable first choice in all situations where the simplifier is used.

This versatility is illustrated in the following example:

> Datatype: tree = Leaf | Node num tree tree
  End
<<HOL warning: Datatype.Hol_datatype: Constructor "Leaf" in new type "tree"
               duplicates constructor in type "btree", which will be
               invalidated by this definition>>
<<HOL warning: Datatype.Hol_datatype: Constructor "Node" in new type "tree"
               duplicates constructor in type "btree", which will be
               invalidated by this definition>>
<<HOL message: Defined type: "tree">>

> SIMP_CONV (srw_ss()) [] “Node x Leaf Leaf = Node 3 t1 t2”;
val it = ⊢ Node x Leaf Leaf = Node 3 t1 t2 ⇔ x = 3 ∧ t1 = Leaf ∧ t2 = Leaf:
   thm

> load "pred_setTheory";
val it = (): unit

> SIMP_CONV (srw_ss()) [] “x IN { y | y < 6}”;
val it = ⊢ x ∈ {y | y < 6} ⇔ x < 6: thm

Users can augment the stateful simpset themselves with the function

   BasicProvers.export_rewrites : string list -> unit

The strings passed to export_rewrites are the names of theorems in the current segment (those that will be exported when export_theory is called). Not only are these theorems added to the underlying simpset in the current session, but they will be added in future sessions when the current theory is reloaded.

> Definition tsize_def:
    (tsize Leaf = 0) /\
    (tsize (Node n t1 t2) = n + tsize t1 + tsize t2)
  End
Definition has been stored under "tsize_def"
val tsize_def =
   ⊢ tsize Leaf = 0 ∧
     ∀n t1 t2. tsize (Node n t1 t2) = n + tsize t1 + tsize t2: thm

> val _ = BasicProvers.export_rewrites ["tsize_def"];

> SIMP_CONV (srw_ss()) [] ``tsize (Node 4 (Node 6 Leaf Leaf) Leaf)``;
val it = ⊢ tsize (Node 4 (Node 6 Leaf Leaf) Leaf) = 10: thm

Alternatively, the user may also flag theorems directly when using store_thm, save_thm, or the Theorem and Definition syntaxes by appending the simp attribute to the name of the theorem. Thus:

Theorem useful_rwt[simp]:
  ...term...
Proof ...tactic...
QED

is a way of avoiding having to write a call to export_rewrites. Equally, the example above could be written:

> Definition tsize_def[simp]:
    (tsize Leaf = 0) /\
    (tsize (Node n t1 t2) = n + tsize t1 + tsize t2)
  End   ... output elided ...

As a general rule, (srw_ss()) includes all of its context’s “obvious rewrites”, as well as code to do standard calculations (such as the arithmetic performed in the above example). It does not include decision procedures that may exhibit occasional poor performance, so the simpset fragments containing these procedures should be added manually to those simplification invocations that need them.

Simpset fragments

The simpset fragment is the basic building block that is used to construct simpset values. There is one basic function that performs this construction:

   op ++  : simpset * ssfrag -> simpset

where ++ is an infix. In general, it is best to build on top of the pure_ss simpset or one of its descendants in order to pick up the default “filter” function for converting theorems to rewrite rules. (This filtering process is described below in Section 8.5.5.3.)

A simpset also carries a (usually empty) set of excluded fragment names, set up by simpLib.exclude_ssfrags (which is what Proof[exclude_frags = \ldots] ultimately calls). When the incoming fragment of ss\ ++\ frag has a name in that set, the addition is a silent no-op and ss is returned unchanged. Use simpLib.force_add, or the SF marker in a thm-list argument to a simplification tactic, to override that prohibition for a particular fragment.

For major theories (or groups thereof), a collection of relevant simpset fragments is usually found in the module <thy>Simps, with <thy> the name of the theory. For example, simpset fragments for the theory of natural numbers are found in numSimps, and fragments for lists are found in listSimps.

Some of the distribution’s standard simpset fragments are described in Table 8.5.4. These and other simpset fragments are described in more detail in the REFERENCE.

Table 8.5.4. Some of HOL’s standard simpset fragments.

Simpset fragments are ultimately constructed with the SSFRAG constructor:

   SSFRAG : {
     convs  : convdata list,
     rewrs  : thm list,
     ac     : (thm * thm) list,
     filter : (controlled_thm -> controlled_thm list) option,
     dprocs : Traverse.reducer list,
     congs  : thm list,
     name   : string option
   } -> ssfrag

A complete description of the various fields of the record passed to SSFRAG, and their meaning is given in REFERENCE. The rewrites function provides an easy route to constructing a fragment that just includes a list of rewrites:

   rewrites : thm list -> ssfrag

Removing rewrites and conversions from simpsets

The -* (infix) function can be used to remove elements from simpsets. This can be done to temporarily affect the simplifier when it is applied to a particular goal. For example:

> SIMP_CONV (srw_ss()) [] “x ++ (y ++ z)”;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ x ⧺ (y ⧺ z) = x ⧺ y ⧺ z: thm

> SIMP_CONV (srw_ss() -* ["APPEND_ASSOC"]) [] “x ++ (y ++ z)”;
Exception- <<HOL message: inventing new type variable names: 'a>>
UNCHANGED raised

The second argument to -* is a list of strings, naming rewrite theorems, conversions or decision procedures. The names to use are visible if simpset values are printed out in the interactive session. The example below demonstrates removing beta-conversion:

> SIMP_CONV (bool_ss -* ["BETA_CONV"]) [] “(\x. x + 3) 10”;
Exception- UNCHANGED raised

Further, because a theorem like AND_CLAUSES

AND_CLAUSES
  ⊢ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧
         (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

has multiple conjuncts, one theorem can generate multiple different rewrites. Specific sub-rewrites can be removed from a simpset without affecting others derived from the same original theorem by appending numbers to the theorem name:

> SIMP_CONV (bool_ss -* ["AND_CLAUSES"]) [] “(T ∧ p) ∧ (q ∧ T)”;
Exception- UNCHANGED raised

> SIMP_CONV (bool_ss -* ["AND_CLAUSES.1"]) [] “(T ∧ p) ∧ (q ∧ T)”;
val it = ⊢ (T ∧ p) ∧ q ∧ T ⇔ (T ∧ p) ∧ q: thm

If using a high-level tactic such as simp, there is no simpset value visible to modify with -*. Instead, one must use a special theorem form (see Section 8.5.6.4 below), Excl to exclude a rewrite. For example, sometimes the associativity of list-append can be annoying (here it masks the rewrite defining list-append):

> g `f (x ++ (h::t ++ y)) = f (x ++ h::(t ++ y))`;   ... output elided ...
> e (simp[]);
OK..
1 subgoal:
val it =
   
   f (x ⧺ h::t ⧺ y) = f (x ⧺ h::(t ⧺ y))

We can prevent the application of this normalising rewrite with the Excl form:

> b();   ... output elided ...
> e (simp[Excl "APPEND_ASSOC"]);
OK..
val it =
   Initial goal proved.
   ⊢ f (x ⧺ (h::t ⧺ y)) = f (x ⧺ h::(t ⧺ y)): proof

One can exclude whole simpset fragments from the high-level tactics with the special ExclSF form, which also takes a string argument. This string is the name of the fragment to be removed, where by convention fragments have the same name as their SML identifier with the _ss suffix removed. Thus, one can use high-level tactics with the arithmetic decision procedure removed:

> g ‘x < 5*2 ==> x < 13’;   ... output elided ...
> e (simp[ExclSF "ARITH"]);
OK..
1 subgoal:
val it =
   
   x < 10 ⇒ x < 13

The exclusion that ExclSF effects is local to the simp call in which it appears. For an exclusion that persists across all the simplification tactics in a proof body, use the Proof[exclude_frags\ =\ \ldots] attribute (the simpLib.exclude_ssfrags function it relies on records the names in the simpset’s excluded set, so subsequent uses of ++ also respect it; see Section 8.5.4). Inside such a proof body, the SF marker can opt back in for an individual simp call.

Rewriting with the simplifier

Rewriting is the simplifier’s “core operation”. This section describes the action of rewriting in more detail.

Basic rewriting

Given a rewrite rule of the form $$ \vdash \ell = r $$ the simplifier will perform a top-down scan of the input term $t$, looking for matches (see Section 8.5.5.4 below) of $\ell$ inside $t$. This match will occur at a sub-term of $t$ (call it $t_0$) and will return an instantiation. When this instantiation is applied to the rewrite rule, the result will be a new equation of the form $$ \vdash t_0 = r' $$ Because the system then has a theorem expressing an equivalence for $t_0$ it can create the new equation $$ \vdash \underbrace{(\dots t_0\dots)}_t = (\dots r' \dots) $$ The traversal of the term to be simplified is repeated until no further matches for the simplifier’s rewrite rules are found. The traversal strategy is

1. While there are any matches for stored rewrite rules at this level, continue to apply them. The order in which rewrite rules are applied can not be relied on, except that when a simpset includes two rewrites with exactly the same left-hand sides, the rewrite added later will get matched in preference. (This allows a certain amount of rewrite-overloading in the construction of simpsets.)
2. Recurse into the term’s sub-terms. The way in which terms are traversed at this step can be controlled by congruence rules (an advanced feature, see Section 8.5.6.1 below).
3. If step 8.5.5.1 changed the term at all, try another phase of rewriting at this level. If this fails, or if there was no change from the traversal of the sub-terms, try any embedded decision procedures (see Section 8.5.6.3). If the rewriting phase or any of the decision procedures altered the term, return to step 8.5.5.1. Otherwise, finish.

Conditional rewriting

The above description is a slight simplification of the true state of affairs. One particularly powerful feature of the simplifier is that it really uses conditional rewrite rules. These are theorems of the form $$ \vdash P \Rightarrow (\ell = r) $$ When the simplifier finds a match for term $\ell$ during its traversal of the term, it attempts to discharge the condition $P$. If the simplifier can simplify the term $P$ to truth, then the instance of $\ell$ in the term being traversed can be replaced by the appropriate instantiation of $r$.

When simplifying $P$ (a term that does not necessarily even occur in the original), the simplifier may find itself applying another conditional rewrite rule. In order to stop excessive recursive applications, the simplifier keeps track of a stack of all the side-conditions it is working on. The simplifier will give up on side-condition proving if it notices a repetition in this stack. There is also a user-accessible variable, Cond_rewr.stack_limit which specifies the maximum size of stack the simplifier is allowed to use.

Conditional rewrites can be extremely useful. For example, theorems about division and modulus are frequently accompanied by conditions requiring the divisor to be non-zero. The simplifier can often discharge these, particularly if it includes an arithmetic decision procedure. For example, the theorem MOD_MOD from the theory arithmetic states $$ \vdash 0 < n \;\Rightarrow \; (k\,\textsf{MOD}\,n)\,\textsf{MOD}\,n = k \,\textsf{MOD}\,n $$ The simplifier (specifically, SIMP_CONV\ arith_ss\ [MOD_MOD]) can use this theorem to simplify the term (k MOD (x + 1)) MOD (x + 1): the arithmetic decision procedure can prove that 0 < x + 1, justifying the rewrite.

Though conditional rewrites are powerful, not every theorem of the form described above is an appropriate choice. A badly chosen rewrite may cause the simplifier’s performance to degrade considerably, as it wastes time attempting to prove impossible side-conditions. For example, the simplifier is not very good at finding existential witnesses. This means that the conditional rewrite $$ \vdash x < y \land y < z \Rightarrow (x < z = \top) $$ will not work as one might hope. In general, the simplifier is not a good tool for performing transitivity reasoning. (Try first-order tools such as PROVE_TAC instead.)

Generating rewrite rules from theorems

There are two routes by which a theorem for rewriting can be passed to the simplifier: either as an explicit argument to one of the SML functions (SIMP_CONV, ASM_SIMP_TAC etc.) that take theorem lists as arguments, or by being included in a simpset fragment which is merged into a simpset. In both cases, these theorems are transformed before being used. The transformations applied are designed to make interactive use as convenient as possible.

In particular, it is not necessary to pass the simplifier theorems that are exactly of the form $$ \vdash P \Rightarrow (\ell = r) $$ Instead, the simplifier will transform its input theorems to extract rewrites of this form itself. The exact transformation performed is dependent on the simpset being used: each simpset contains its own “filter” function which is applied to theorems that are added to it. Most simpsets use the filter function from the pure_ss simpset (see Section 8.5.3.1). However, when a simpset fragment is added to a full simpset, the fragment can specify an additional filter component. If specified, this function is of type controlled_thm\ ->\ controlled_thm\ list, and is applied to each of the theorems produced by the existing simpset’s filter. (A “controlled” theorem is one that is accompanied by a piece of “control” data expressing the limit (if any) on the number of times it can be applied. See Section 8.5.6.4 for how users can introduce these limits. The “control” type appears in the SML module BoundedRewrites.)

The rewrite-producing filter in pure_ss strips away conjunctions, implications and universal quantifications until it has either an equality theorem, or some other boolean form. For example, the theorem ADD_MODULUS states $$ \vdash \begin{array}{l} (\forall n\;x.\;\;0 < n \Rightarrow ((x + n)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n)) \;\;\land\\ (\forall n\;x.\;\;0 < n \Rightarrow ((n + x)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n)) \end{array} $$ This theorem becomes two rewrite rules $$ \begin{array}{l} \vdash 0 < n \Rightarrow ((x + n)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n)\\ \vdash 0 < n \Rightarrow ((n + x)\,\textsf{MOD}\,n = x\,\textsf{MOD}\,n) \end{array} $$

If looking at an equality where there are variables on the right-hand side that do not occur on the left-hand side, the simplifier transforms this to the rule $$ \vdash (\ell = r) = \top $$ Similarly, if a boolean negation $\neg P$, becomes the rule $$ \vdash P = \bot $$ and other boolean formulas $P$ become $$ \vdash P = \top $$

Finally, if looking at an equality whose left-hand side is itself an equality, and where the right-hand side is not an equality as well, the simplifier transforms $(x = y) = P$ into the two rules $$ \begin{array}{l} \vdash (x = y) = P\\ \vdash (y = x) = P \end{array} $$ This is generally useful. For example, a theorem such as $$ \vdash \neg(\textsf{SUC}\,n = 0) $$ will cause the simplifier to rewrite both $(\textsf{SUC}\,n = 0)$ and $(0 = \textsf{SUC}\,n)$ to false.

The restriction that the right-hand side of such a rule not itself be an equality is a simple heuristic that prevents some forms of looping.

Matching rewrite rules

Given a rewrite theorem $\vdash \ell = r$, the first stage of performing a rewrite is determining whether or not $\ell$ can be instantiated so as to make it equal to the term that is being rewritten. This process is known as matching. For example, if $\ell$ is the term $\textsf{SUC}(n)$, then matching it against the term $\textsf{SUC}(3)$ will succeed, and find the instantiation $n\mapsto 3$. In contrast with unification, matching is not symmetrical: a pattern $\textsf{SUC}(3)$ will not match the term $\textsf{SUC}(n)$.

The simplifier uses a special form of higher-order matching. If a pattern includes a variable of some function type ($f$ say), and that variable is applied to an argument $a$ that includes no variables except those that are bound by an abstraction at a higher scope, then the combined term $f(a)$ will match any term of the appropriate type as long as the only occurrences of the bound variables in $a$ are in sub-terms matching $a$.

Assume for the following examples that the variable $x$ is bound at a higher scope. Then, if $f(x)$ is to match $x + 4$, the variable $f$ will be instantiated to $(\lambda x.\; x + 4)$. If $f(x)$ is to match $3 + z$, then $f$ will be instantiated to $(\lambda x.\;3 + z)$. Further $f(x + 1)$ matches $x + 1 < 7$, but does not match $x + 2 < 7$.

Higher-order matching of this sort makes it easy to express quantifier movement results as rewrite rules, and have these rules applied by the simplifier. For example, the theorem $$ \vdash (\exists x. \;P(x)\lor Q(x)) = (\exists x.\;P(x)) \lor (\exists x.\;Q(x)) $$ has two variables of a function-type ($P$ and $Q$), and both are applied to the bound variable $x$. This means that when applied to the input $$ \exists z. \;z < 4 \lor z + x = 5 * z $$ the matcher will find the instantiation $$ \begin{array}{l} P \mapsto (\lambda z.\;z < 4)\\ Q \mapsto (\lambda z.\;z + x = 5 * z) \end{array} $$

Performing this instantiation, and then doing some $\beta$-reduction on the rewrite rule, produces the theorem $$ \vdash (\exists z. \;z < 4 \lor z + x = 5 * z) = (\exists z. \;z < 4) \lor (\exists z.\;z + x = 5 * z) $$ as required.

Another example of a rule that the simplifier will use successfully is $$ \vdash f \circ (\lambda x.\; g(x)) = (\lambda x.\;f(g(x))) $$ The presence of the abstraction on the left-hand side of the rule requires an abstraction to appear in the term to be matched, so this rule can be seen as an implementation of a method to move abstractions up over function compositions.

An example of a possible left-hand side that will not match as generally as might be liked is $(\exists x.\;P(x + y))$. This is because the predicate $P$ is applied to an argument that includes the free variable $y$.

Advanced features

This section describes some of the simplifier’s advanced features.

Congruence rules

Congruence rules control the way the simplifier traverses a term. They also provide a mechanism by which additional assumptions can be added to the simplifier’s context, representing information about the containing context. The simplest congruence rules are built into the pure_ss simpset. They specify how to traverse application and abstraction terms. At this fundamental level, these congruence rules are little more than the rules of inference ABS $$ \frac{\Gamma \vdash t_1 = t_2} {\Gamma \vdash (\lambda x.\;t_1) = (\lambda x.\;t_2)} $$ (where $x\not\in\Gamma$) and MK_COMB $$ \frac{\Gamma \vdash f = g \qquad \qquad \Delta \vdash x = y} {\Gamma \cup \Delta \vdash f(x) = g(y)} $$ When specifying the action of the simplifier, these rules should be read upwards. With ABS, for example, the rule says “when simplifying an abstraction, simplify the body $t_1$ to some new $t_2$, and then the result is formed by re-abstracting with the bound variable $x$.”

Further congruence rules should be added to the simplifier in the form of theorems, via the congs field of the records passed to the SSFRAG constructor. Such congruence rules should be of the form $$ \mathit{cond_1} \Rightarrow \mathit{cond_2} \Rightarrow \dots (E_1 = E_2) $$ where $E_1$ is the form to be rewritten. Each $\mathit{cond}_i$ can either be an arbitrary boolean formula (in which case it is treated as a side-condition to be discharged) or an equation of the general form $$ \forall \vec{v}. \;\mathit{ctxt}_1 \Rightarrow \mathit{ctxt}_2 \Rightarrow \dots (V_1(\vec{v}) = V_2(\vec{v})) $$ where the variable $V_2$ must occur free in $E_2$.

For example, the theorem form of MK_COMB would be $$ \vdash (f = g) \Rightarrow (x = y) \Rightarrow (f(x) = g(y)) $$ and the theorem form of ABS would be $$ \vdash (\forall x. \;f (x) = g (x)) \Rightarrow (\lambda x. \;f(x)) = (\lambda x.\;g(x)) $$ The form for ABS demonstrates how it is possible for congruence rules to handle bound variables. Because the congruence rules are matched with the higher-order match of Section 8.5.5.4, this rule will match all possible abstraction terms.

These simple examples have not yet demonstrated the use of $\mathit{ctxt}$ conditions on sub-equations. An example of this is the congruence rule (found in CONG_ss) for implications. This states $$ \vdash (P = P') \Rightarrow (P' \Rightarrow (Q = Q')) \Rightarrow (P \Rightarrow Q = P' \Rightarrow Q') $$ This rule should be read: “When simplifying $P\Rightarrow Q$, first simplify $P$ to $P'$. Then assume $P'$, and simplify $Q$ to $Q'$. Then the result is $P' \Rightarrow Q'$.”

The rule for conditional expressions is $$ \vdash \begin{array}{l} (P = P') \Rightarrow (P' \Rightarrow (x = x')) \Rightarrow (\neg P' \Rightarrow (y = y')) \;\Rightarrow\\ (\textsf{if}\;P\;\textsf{then}\;x\;\textsf{else}\;y = \textsf{if}\;P'\;\textsf{then}\;x'\;\textsf{else}\;y') \end{array} $$ This rule allows the guard to be assumed when simplifying the true-branch of the conditional, and its negation to be assumed when simplifying the false-branch.

The contextual assumptions from congruence rules are turned into rewrites using the mechanisms described in Section 8.5.5.3.

Congruence rules can be used to achieve a number of interesting effects. For example, a congruence can specify that sub-terms not be simplified if desired. This might be used to prevent simplification of the branches of conditional expressions: $$ \vdash (P = P') \Rightarrow (\textsf{if}\;P\;\textsf{then}\;x\;\textsf{else}\;y = \textsf{if}\;P'\;\textsf{then}\;x\;\textsf{else}\;y) $$ If added to the simplifier, this rule will take precedence over any other rules for conditional expressions (masking the one above from CONG_ss, say), and will cause the simplifier to only descend into the guard. With the standard rewrites (from BOOL_ss): $$ \begin{array}{l} \vdash \;\textsf{if}\;\top\;\textsf{then}\;x\;\textsf{else}\;y \,\;=\,\; x\\ \vdash \;\textsf{if}\;\bot\;\textsf{then}\;x\;\textsf{else}\;y \,\;=\,\; y \end{array} $$ users can choose to have the simplifier completely ignore a conditional’s branches until that conditional’s guard is simplified to either true or false.

As a convenience, congruence rules expressed in the format used by termination analysis in defining recursive functions (see Section 7.6.2.5), can also be passed to the simplifier.

AC-normalisation

The simplifier can be used to normalise terms involving associative and commutative constants. This process is known as AC-normalisation. The simplifier will perform AC-normalisation for those constants which have their associativity and commutativity theorems provided in a constituent simpset fragment’s ac field.

For example, the following simpset fragment will cause AC-normalisation of disjunctions

SSFRAG { name = NONE,
convs = [], rewrs = [], congs = [],
filter = NONE, ac = [(DISJ_ASSOC, DISJ_COMM)],
dprocs = [] }

The pair of provided theorems must state $$ \begin{array}{lcl} x \oplus y &=& y \oplus x\\ x \oplus (y \oplus z) &=& (x \oplus y) \oplus z \end{array} $$ for a constant $\oplus$. The theorems may be universally quantified, and the associativity theorem may be oriented either way. Further, either the associativity theorem or the commutativity theorem may be the first component of the pair. Assuming the simpset fragment above is bound to the SML identifier DISJ_ss, its behaviour is demonstrated in the following example:

> SIMP_CONV (bool_ss ++ DISJ_ss) [] ``p /\ q \/ r \/ P z``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ p ∧ q ∨ r ∨ P z ⇔ r ∨ P z ∨ p ∧ q: thm

The order of operands in the AC-normal form that the simplifer’s AC-normalisation works toward is unspecified. However, the normal form is always right-associated. Note also that the arith_ss simpset, and the ARITH_ss fragment which is its basis, have their own bespoke normalisation procedures for addition over the natural numbers. Mixing AC-normalisation, as described here, with arith_ss can cause the simplifier to go into an infinite loop.

AC theorems can also be added to simpsets via the theorem-list part of the tactic and conversion interface, using the special rewrite form AC:

> SIMP_CONV bool_ss [AC DISJ_ASSOC DISJ_COMM] ``p /\ q \/ r \/ P z``;
<<HOL message: inventing new type variable names: 'a>>
val it = ⊢ p ∧ q ∨ r ∨ P z ⇔ r ∨ P z ∨ p ∧ q: thm

See Section 8.5.6.4 for more on special rewrite forms.

Embedding code

The simplifier features two different ways in which user-code can be embedded into its traversal and simplification of input terms. By embedding their own code, users can customise the behaviour of the simplifier to a significant extent.

User conversions

The simpler of the two methods allows the simplifier to include user-supplied conversions. These are added to simpsets in the convs field of simpset fragments. This field takes lists of values of type

   { name: string,
    trace: int,
      key: (term list * term) option,
     conv: (term list -> term -> thm) -> term list -> term -> thm}

The name and trace fields are used when simplifier tracing is turned on. If the conversion is applied, and if the simplifier trace level is greater than or equal to the trace field, then a message about the conversion’s application (including its name) will be emitted.

The key field of the above record is used to specify the sub-terms to which the conversion should be applied. If the value is NONE, then the conversion will be tried at every position. Otherwise, the conversion is applied at term positions matching the provided pattern. The first component of the pattern is a list of variables that should be treated as constants when finding pattern matches. The second component is the term pattern itself. Matching against this component is not done by the higher-order match of Section 8.5.5.4, but by a higher-order “term-net”. This form of matching does not aim to be precise; it is used to efficiently eliminate clearly impossible matches. It does not check types, and does not check multiple bindings. This means that the conversion will not only be applied to terms that are exact matches for the supplied pattern.

Finally, the conversion itself. Most uses of this facility are to add normal HOL conversions (of type term->thm), and this can be done by ignoring the conv field’s first two parameters. For a conversion myconv, the standard idiom is to write K\ (K\ myconv). If the user desires, however, their code can refer to the first two parameters. The second parameter is the stack of side-conditions that have been attempted so far. The first enables the user’s code to call back to the simplifier, passing the stack of side-conditions, and a new side-condition to solve. The term argument must be of type :bool, and the recursive call will simplify it to true (and call EQT_ELIM to turn a term $t$ into the theorem $\vdash t$). This restriction is lifted for decision procedures (see below), but for conversions the recursive call can only be used for side-condition discharge. Note also that it is the user’s responsibility to pass an appropriately updated stack of side-conditions to the recursive invocation of the simplifier.

A user-supplied conversion should never return the reflexive identity (an instance of $\vdash t = t$). This will cause the simplifier to loop. Rather than return such a result, raise a HOL_ERR or Conv.UNCHANGED exception. (Both are treated the same by the simplifier.)

Context-aware decision procedures

Another, more involved, method for embedding user code into the simplifier is via the dprocs field of the simpset fragment structure. This method is more general than adding conversions, and also allows user code to construct and maintain its own bespoke logical contexts.

The dprocs field requires lists of values of the type Traverse.reducer. These values are constructed with the constructor REDUCER:

constructor REDUCER:
   \{addcontext: context * thm list -> context,
     apply:
     \{context: context,
       conv: term list -> term -> thm,
       relation: term * (term -> thm),
       solver: term list -> term -> thm, stack: term list\} ->
       Traverse.conv, initial: context, name: string option\} ->
     Traverse.reducer

The context type is an alias for the built-in SML type exn, that of exceptions. The exceptions here are used as a “universal type”, capable of storing data of any type. For example, if the desired data is a pair of an integer and a boolean, then the following declaration could be made:

   exception my_data of int * bool

It is not necessary to make this declaration visible with a wide scope. Indeed, only functions accessing and creating contexts of this form need to see it. For example:

  fun get_data c = (raise c) handle my_data (i,b) => (i,b)
  fun mk_ctxt (i,b) = my_data(i,b)

When creating a value of reducer type, the user must provide an initial context, and two functions. The first, addcontext, is called by the simplifier’s traversal mechanism to give every embedded decision procedure access to theorems representing new context information. For example, this function is called with theorems from the current assumptions in ASM_SIMP_TAC, and with the theorems from the theorem-list arguments to all of the various simplification functions. As a term is traversed, the congruence rules governing this traversal may also provide additional theorems; these will also be passed to the addcontext function. (Of course, it is entirely up to the addcontext function as to how these theorems will be handled; they may even be ignored entirely.)

When an embedded reducer is applied to a term, the provided apply function is called. As well as the term to be transformed, the apply function is also passed a record containing a side-condition solver, a more general call-back to the simplifier, the decision procedure’s current context, and the stack of side-conditions attempted so far. The stack and solver are the same as the additional arguments provided to user-supplied conversions. The conv argument is call-back to the simplifier, which given a term $t$ returns a theorem of the form $\vdash t = t'$ or fails. In contrast, the solver either returns the theorem $\vdash t$ or fails. The power of the reducer abstraction is having access to a context that can be built appropriately for each decision procedure.

Decision procedures are applied last when a term is encountered by the simplifier. More, they are applied after the simplifier has already recursed into any sub-terms and tried to do as much rewriting as possible. This means that although simplifier rewriting occurs in a top-down fashion, decision procedures will be applied bottom-up and only as a last resort.

As with user-conversions, decision procedures must raise an exception rather than return instances of reflexivity.

Special rewrite forms

Some of the simplifier’s features can be accessed in a relatively simple way by using SML functions to construct special theorem forms. These special theorems can then be passed in the simplification tactics’ theorem-list arguments.

Two of the simplifier’s advanced features, AC-normalisation and congruence rules can be accessed in this way. Rather than construct a custom simpset fragment including the required AC or congruence rules, the user can instead use the functions AC or Cong:

   AC : thm -> thm -> thm
   Cong : thm -> thm

For example, if the theorem value

   AC DISJ_ASSOC DISJ_COMM

appears amongst the theorems passed to a simplification tactic, then the simplifier will perform AC-normalisation of disjunctions. The Cong function provides a similar interface for the addition of new congruence rules.

Two other functions provide a crude mechanism for controlling the number of times an individual rewrite will be applied.

   Once : thm -> thm
   Ntimes : thm -> int -> thm

A theorem “wrapped” in the Once function will only be applied once when the simplifier is applied to a given term. A theorem wrapped in Ntimes will be applied as many times as given in the integer parameter.

Another pair of special forms allow the user to require that certain rewrites are applied. Both forms check the count of instances of rewrite-redexes appearing in the goal that results after simplification has happened. If the requirement is not satisfied, the relevant tactic fails. In this context, a rewrite redex is the LHS of a theorem being used as a rewrite, so that, for example, the redex of the theorem $\vdash x + 0 = x$ is $x + 0$. The Req0 form checks that the number of redexes of the corresponding rewrite is zero in the resulting goal. For unconditional rewrites, such a requirement is usually redundant, but this form can be useful when rewrites are conditional and the simplifier may have failed to discharge side-conditions. For example:

> val th = arithmeticTheory.ZERO_MOD;
val th = ⊢ ∀n. 0 < n ⇒ 0 MOD n = 0: thm
> simp[Req0 th] ([], ``0 MOD z``);
val it = ([([], “0”)], fn): goal list * validation

> simp[Req0 th] ([], ``0 MOD (z + 1)``)
   (* succeeds because arithmetic d.p. knows z + 1 is nonzero *);
val it = ([([], “0”)], fn): goal list * validation

The ReqD modifier requires that the redex count should have decreased. This is implicitly a check on the original goal as well: it must have a non-zero count of redexes itself.

Both Req0 and ReqD can be combined with Once and Ntimes.

Excluding rewrites

As also described above in Section 8.5.4.1, various built-in (named) components can be removed from invocations of the simplifier through the use of the Excl form. This function is of type string\ ->\ thm, so takes a string naming the rewrite or other component that is to be removed. For example, the standard stateful simpset includes the theorem stating that $x < x + y \Leftrightarrow 0 < y$, with name X_LT_X_PLUS:

> simp[] ([], “x < x + 2 * y”);
val it = ([([], “0 < y”)], fn): goal list * validation

> simp[Excl "X_LT_X_PLUS"] ([], “x < x + 2 * y”);
val it = ([([], “x < x + 2 * y”)], fn): goal list * validation

In addition to rewrites, conversions and decision procedures can also be temporarily excluded in this way:

> simp[Excl "BETA_CONV"] ([], “(λx. x + 10) (6 * z)”);
val it = ([([], “(λx. x + 10) (6 * z)”)], fn): goal list * validation

Excluding assumptions

It is possible to stop tactics such as simp from using assumptions (it otherwise tries to use all of a goal’s assumptions) with the NoAsms and IgnAsm forms. The NoAsms form prevents the use of all of a goal’s assumptions:

> simp[NoAsms] ([“x = 3”], “x < 10”);
val it = ([([“x = 3”], “x < 10”)], fn): goal list * validation

The IgnAsm form takes a quotation argument corresponding to a pattern (where free variables in the pattern that also occur in the goal are forced to take on their types in the goal). Every assumption that matches the pattern is excluded from further simplification. By default, the matching requires the pattern to match the entirety of the assumption statement. However, if the pattern concludes with the comment (* sa *) (with or without the spaces; “sa” stands for “sub-assumption”), the matching succeeds (and the assumption is excluded) if the pattern matches any sub-term of the assumption. Thus:

> simp[IgnAsm‘x = _’] ([“x = F”, “y = T”], “p ∧ x ∧ y”);
val it = ([([“x ⇔ F”, “y ⇔ T”], “p ∧ x”)], fn): goal list * validation

> simp[IgnAsm‘F’] ([“x = F”, “y = T”], “p ∧ x ∧ y”); (* nothing matches *)
val it = ([([“x ⇔ F”, “y ⇔ T”], “F”)], fn): goal list * validation

> simp[IgnAsm‘F(* sa *)’] ([“x = F”, “y = T”], “p ∧ x ∧ y”);
val it = ([([“x ⇔ F”, “y ⇔ T”], “p ∧ x”)], fn): goal list * validation

> simp[IgnAsm‘_ = _’] ([“x = F”, “y = T”, “p:bool”], “p ∧ x ∧ y”);
val it = ([([“x ⇔ F”, “y ⇔ T”, “p”], “x ∧ y”)], fn): goal list * validation

Including simpset fragments

The SF theorem form provides a way to augment a simplification with a simpset fragment. For example, one can rewrite with conjunctions as assumptions using the CONJ_ss fragment:

> g ‘x = 10 ∧ x < 16’;   ... output elided ...
> e (simp[SF CONJ_ss]);
OK..
1 subgoal:
val it =
   
   x = 10

SF also serves as the in-call escape hatch for fragments excluded by an enclosing Proof[exclude_frags\ =\ \ldots] attribute (see Section 8.5.4): writing simp[SF\ X_ss] inside a body where the fragment named "X" has been excluded re-enables it for that one simp call.

Simplifying at particular sub-terms

We have already seen (Section 8.5.6.1 above) that the simplifier’s congruence technology can be used to force the simplifier to ignore particular terms. The example in the section above discussed how a congruence rule might be used to ensure that only the guards of conditional expressions should be simplified.

In many proofs, it is common to want to rewrite only on one side or the other of a binary connective (often, this connective is an equality). For example, this occurs when rewriting with equations from complicated recursive definitions that are not just structural recursions. In such definitions, the left-hand side of the equation will have a function symbol attached to a sequence of variables, e.g.:

   |- f x y = ... f (g x y) z ...

Theorems of a similar shape are also returned as the “cases” theorems from inductive definitions.

Whatever their origin, such theorems are the classic example of something to which one would want to attach the Once qualifier. However, this may not be enough: one may wish to prove a result such as

   f (constructor x) y = ... f (h x y) z ...

(With relations, the goal may often feature an implication instead of an equality.) In this situation, one often wants to expand just the instance of f on the left, leaving the other occurrence alone. Using Once will expand only one of them, but without specifying which one is to be expanded.

The solution to this problem is to use special congruence rules, constructed as special forms that can be passed as theorems like Once. The functions

   SimpL : term -> thm
   SimpR : term -> thm

construct congruence rules to force rewriting to the left or right of particular terms. For example, if opn is a binary operator, SimpL\ ``(opn)``` returns Cong` applied to the theorem

   |- (x = x') ==> (opn x y = opn x' y)

Because the equality case is so common, the special values SimpLHS and SimpRHS are provided to force simplification on the left or right of an equality respectively. These are just defined to be applications of SimpL and SimpR to equality.

Note that these rules apply throughout a term, not just to the uppermost occurrence of an operator. Also, the topmost operator in the term need not be that of the congruence rule. This behaviour is an automatic consequence of the implementation in terms of congruence rules.

Limiting simplification

In addition to the Once and Ntimes theorem-forms just discussed, which limit the number of times a particular rewrite is applied, the simplifier can also be limited in the total number of rewrites it performs. The limit function (in simpLib and bossLib)

   limit : int -> simpset -> simpset

records a numeric limit in a simpset. When a limited simpset then works over a term, it will never apply more than the given number of rewrites to that term. When conditional rewrites are used, the rewriting done in the discharge of side-conditions counts against the limit, as long as the rewrite is ultimately applied. The application of user-provided congruence rules, user-provided conversions and decision procedures also all count against the limit.

When the simplifier yields control to a user-provided conversion or decision procedure it cannot guarantee that these functions will ever return (and they may also take arbitrarily long to work, often a worry with arithmetic decision procedures), but use of limit is otherwise a good method for ensuring that simplification terminates.

Rewriting with arbitrary pre-orders

In addition to simplifying with respect to equality, it is also possible to use the simplifier to “rewrite” with respect to a relation that is reflexive and transitive (a preorder). This can be a very powerful way of working with transition relations in operational semantics.

Imagine, for example, that one has set up a “deep embedding” of the $\lambda$-calculus. This will entail the definition of a new type (lamterm, say) within the logic, as well as definitions of appropriate functions (e.g., substitution) and relations over lamterm. One is likely to work with the reflexive and transitive closure of $\beta$-reduction ($\rightarrow^*_\beta$). This relation has congruence rules such as $$ \begin{array}{c@{\qquad\qquad}c} \frac{M_1 \;\rightarrow^*_\beta\;M_2}{M_1 \,N\;\rightarrow^*_\beta\;M_2\,N} & \frac{N_1 \;\rightarrow^*_\beta\;N_2}{M \,N_1\;\rightarrow^*_\beta\;M\,N_2}\\[3mm] \multicolumn{2}{c}{\frac{M_1\;\rightarrow^*_\beta\;M_2}{(\lambda v.M_1)\;\rightarrow^*_\beta\;(\lambda v.M_2)}} \end{array} $$ and one important rewrite $$ (\lambda v. M)\,N \;\rightarrow^*_\beta\; M[v := N] $$ Having to apply these rules manually in order to show that a given starting term can reduce to particular destination is usually very painful, involving many applications, not only of the theorems above, but also of the theorems describing reflexive and transitive closure (see Section 5.5.3).

Though the $\lambda$-calculus is non-deterministic, it is also confluent, so the following theorem holds: $$ \frac{\beta\textrm{-nf}\;N \qquad M_1 \;\rightarrow^*_\beta\;M_2} {M_1 \;\rightarrow^*_\beta\;N\;\;=\;\;M_2\;\rightarrow^*_\beta\; N} $$ This is the critical theorem that justifies the switch from rewriting with equality to rewriting with $\rightarrow^*_\beta$. It says that if one has a term $M_1\rightarrow^*_\beta N$, with $N$ a $\beta$-normal form, and if $M_1$ rewrites to $M_2$ under $\rightarrow^*_\beta$, then the original term is equal to $M_2\rightarrow^*_\beta N$. With luck, $M_2$ will actually be syntactically identical to $N$, and the reflexivity of $\rightarrow^*_\beta$ will prove the desired result. Theorems such as these, that justify the switch from one rewriting relation to another are known as weakening congruences.

When adjusted appropriately, the simplifier can be modified to exploit the five theorems above, and automatically prove results such as $$ u ((\lambda f\,x. f (f\,x)) v) \rightarrow^*_\beta u (\lambda x. v(v\,x)) $$ (on the assumption that the terms $u$ and $v$ are $\lambda$-calculus variables, making the result a $\beta$-normal form).

In addition, one will quite probably have various rewrite theorems that one will want to use in addition to those specified above. For example, if one has earlier proved a theorem such as $$ K\,x\,y \rightarrow^*_\beta x $$ then the simplifier can take this into account as well.

The function achieving all this is

   simpLib.add_relsimp  : {trans: thm, refl: thm, weakenings: thm list,
                           subsets: thm list, rewrs : thm list} ->
                          simpset -> simpset

The fields of the record that is the first argument are:

trans

The theorem stating that the relation is transitive, in the form $\forall x\;y\;z.\ R\,x\,y \land R\,y\,z \Rightarrow R\,x\,z$.

refl

The theorem stating that the relation is reflexive, in the form $\forall x.\ R\,x\,x$.

weakenings

A list of weakening congruences, of the general form $P_1 \Rightarrow P_2 \Rightarrow \cdots (t_1 = t_2)$, where at least one of the $P_i$ will presumably mention the new relation $R$ applied to a variable that appears in $t_1$. Other antecedents may be side-conditions such as the requirement in the example above that the term $N$ be in $\beta$-normal form.

subsets

Theorems of the form $R'\,x\,y \Rightarrow R\,x\,y$. These are used to augment the resulting simpset’s “filter” so that theorems in the context mentioning $R'$ will derive useful rewrites involving $R$. In the example of $\beta$-reduction, one might also have a relation $\rightarrow_{wh}^*$ for weak-head reduction. Any weak-head reduction is also a $\beta$-reduction, so it can be useful to have the simplifier automatically “promote” facts about weak-head reduction to facts about $\beta$-reduction, and to then use them as rewrites.

rewrs

Possibly conditional rewrites, presumably mostly of the form $P \Rightarrow R\,t_1\,t_2$. Rewrites over equality can also be included here, allowing useful additional facts to be included. For example, when working with the $\lambda$-calculus, one might include both the rewrite for $K$ above, as well as the definition of substitution.

The application of this function to a simpset ss will produce an augmented ss that has all of ss’s existing behaviours, as well as the ability to rewrite with the given relation.

Tracing the Simplifier

There is a trace variable associated with the simplifier that can be used to obtain a log of its activities printed to the screen as simplification proceeds. (The tracing system is described generally in Section 10.2 below.) With the name "simplifier", this trace can be set to have integer values between 0 and 7, inclusive. The default value of 0 means that no logging will be printed. Larger values result in more output.

Tracing can be useful in trying to determine why a simplification theorem is not being applied, perhaps because of a failure to simplify side-conditions. At high values of the trace, output can be particularly voluminous.