Chapter 6: Goal Oriented Proof: Tactics and Tacticals

The style of forward proof described in the previous chapter is unnatural and too `low level' for many applications. An important advance in proof generating methodology was made by Robin Milner in the early 1970s when he invented the notion of tactics. A tactic is a function that does two things.

Splits a `goal' into `subgoals'.
Keeps track of the reason why solving the subgoals will solve the goal.

Consider, for example, the rule of Ù-introduction ¹ shown below:

G₁ |- t₁ G₂ |- t₂

G₁ÈG₂ |- t₁ Ù t₂

In HOL, Ù-introduction is represented by the ML function CONJ:

CONJ (G₁ |- t₁) (G₂ |- t₂) ® (G₁ÈG₂ |- t₁ Ù t₂)

This is illustrated in the following new session (note that the session number has been reset to 1, but we'll assume that the same setup (from the previous chapter's session 0, has been invoked):

- show_assums := true;
val it = () : unit

- val Th1 = ASSUME ``A:bool`` and Th2 = ASSUME ``B:bool``;
> val Th1 =  [A] |- A : thm
  val Th2 =  [B] |- B : thm

- val Th3 = CONJ Th1 Th2;
> val Th3 =  [A, B] |- A /\ B : thm

Suppose the goal is to prove A Ù B, then this rule says that it is sufficient to prove the two subgoals A and B, because from |- A and |- B the theorem |- A Ù B can be deduced. Thus:

To prove |- A Ù B it is sufficient to prove |- A and |- B.
The justification for the reduction of the goal |- A Ù B to the two subgoals |- A and |- B is the rule of Ù-introduction.

A goal in HOL is a pair ([t₁;...;t_n],t) of ML type term list * term. An achievement of such a goal is a theorem t₁,...,t_n |- t. A tactic is an ML function that when applied to a goal generates subgoals together with a justification function or validation, which will be an ML derived inference rule, that can be used to infer an achievement of the original goal from achievements of the subgoals.

If T is a tactic (i.e. an ML function of type goal -> (goal list * (thm list -> thm))) and g is a goal, then applying T to g (i.e. evaluating the ML expression T g) will result in an object which is a pair whose first component is a list of goals and whose second component is a justification function, i.e. a value with ML type thm list -> thm.

An example tactic is CONJ_TAC which implements (i) and (ii) above. For example, consider the utterly trivial goal of showing T /\ T, where T is a constant that stands for true:

- val goal1 =([]:term list, ``T /\ T``);
> val goal1 = ([], ``T /\ T``) : term list * term

- CONJ_TAC goal1;
> val it =
    ([([], ``T``), ([], ``T``)], fn)
    : (term list * term) list * (thm list -> thm)

- val (goal_list,just_fn) = it;
> val goal_list =
    [([], ``T``), ([], ``T``)]
    : (term list * term) list
  val just_fn = fn : thm list -> thm

CONJ_TAC has produced a goal list consisting of two identical subgoals of just showing ([],"T"). Now, there is a preproved theorem in HOL, called TRUTH, that achieves this goal:

- TRUTH;
> val it = [] |- T : thm

Applying the justification function just_fn to a list of theorems achieving the goals in goal_list results in a theorem achieving the original goal:

- just_fn [TRUTH,TRUTH];
> val it =  [] |- T /\ T : thm

Although this example is trivial, it does illustrate the essential idea of tactics. Note that tactics are not special theorem-proving primitives; they are just ML functions. For example, the definition of CONJ_TAC is simply:

   fun CONJ_TAC (asl,w) = let
     val (l,r) = dest_conj w
   in
     ([(asl,l), (asl,r)], fn [th1,th2] => CONJ th1 th2)
   end

The ML function dest_conj splits a conjunction into its two conjuncts: If (asl,``t₁/\t₂``) is a goal, then CONJ_TAC splits it into the list of two subgoals (asl,t₁) and (asl,t₂). The justification function, fn [th1,th2] => CONJ th1 th2 takes a list [th₁,th₂] of theorems and applies the rule CONJ to th₁ and th₂.

To summarize: if T is a tactic and g is a goal, then applying T to g will result in a pair whose first component is a list of goals and whose second component is a justification function, with ML type thm list -> thm.

Suppose T g = ([g₁,...,g_n],p). The idea is that g₁ , ... , g_n are subgoals and p is a `justification' of the reduction of goal g to subgoals g₁ , ... , g_n. Suppose further that the subgoals g₁ , ... , g_n have been solved. This would mean that theorems th₁ , ... , th_n had been proved such that each th_i (1£ i£ n) `achieves' the goal g_i. The justification p (produced by applying T to g) is an ML function which when applied to the list [th₁,...,th_n] returns a theorem, th, which `achieves' the original goal g. Thus p is a function for converting a solution of the subgoals to a solution of the original goal. If p does this successfully, then the tactic T is called valid. Invalid tactics cannot result in the proof of invalid theorems; the worst they can do is result in insolvable goals or unintended theorems being proved. If T were invalid and were used to reduce goal g to subgoals g₁ , ... , g_n, then effort might be spent proving theorems th₁ , ... , th_n to achieve the subgoals g₁ , ... , g_n, only to find out after the work is done that this is a blind alley because p[th₁,...,th_n] doesn't achieve g (i.e. it fails, or else it achieves some other goal).

A theorem achieves a goal if the assumptions of the theorem are included in the assumptions of the goal and if the conclusion of the theorems is equal (up to the renaming of bound variables) to the conclusion of the goal. More precisely, a theorem

t₁, ..., t_m |- t

achieves a goal

([u₁,...,u_n],u)

if and only if {t₁,...,t_m} is a subset of {u₁,...,u_n} and t is equal to u (up to renaming of bound variables). For example, the goal ([``x=y``, ``y=z``, ``z=w``], ``x=z``) is achieved by the theorem [x=y, y=z] |- x=z (the assumption ``z=w`` is not needed).

A tactic solves a goal if it reduces the goal to the empty list of subgoals. Thus T solves g if T g = ([],p). If this is the case and if T is valid, then p[] will evaluate to a theorem achieving g. Thus if T solves g then the ML expression snd(T g)[] evaluates to a theorem achieving g.

Tactics are specified using the following notation:

goal

goal₁ goal₂ ··· goal_n

For example, a tactic called CONJ_TAC is described by


t₁ `/\` t₂

t₁	t₂

Thus CONJ_TAC reduces a goal of the form (G,``t₁/\t₂``) to subgoals (G,``t₁``) and (G,``t₂``). The fact that the assumptions of the top-level goal are propagated unchanged to the two subgoals is indicated by the absence of assumptions in the notation.

Another example is numLib.INDUCT_TAC, the tactic for doing mathematical induction on the natural numbers:


`!`n`.`t[n]

t[`0`]	{t[n]} t[`SUC` n]

INDUCT_TAC reduces a goal (G,``!n.t[n]``) to a basis subgoal (G,``t[0]``) and an induction step subgoal (GÈ{``t[n]``},``t[SUC n]``). The extra induction assumption ``t[n]`` is indicated in the tactic notation with set brackets.

- numLib.INDUCT_TAC([], ``!m n. m+n = n+m``);
> val it =
    ([([], ``!n. 0 + n = n + 0``),
      ([``!n. m + n = n + m``], ``!n. SUC m + n = n + SUC m``)], fn)
    : (term list * term) list * (thm list -> thm)

The first subgoal is the basis case and the second subgoal is the step case.

Tactics generally fail (in the ML sense, i.e. raise an exception) if they are applied to inappropriate goals. For example, CONJ_TAC will fail if it is applied to a goal whose conclusion is not a conjunction. Some tactics never fail, for example ALL_TAC

is the `identity tactic'; it reduces a goal (G,t) to the single subgoal (G,t)---i.e. it has no effect. ALL_TAC is useful for writing complex tactics using tacticals.

6.1 Using tactics to prove theorems

Suppose goal g is to be solved. If g is simple it might be possible to immediately think up a tactic, T say, which reduces it to the empty list of subgoals. If this is the case then executing:

val (gl,p) = T g

will bind p to a function which when applied to the empty list of theorems yields a theorem th achieving g. (The declaration above will also bind gl to the empty list of goals.) Thus a theorem achieving g can be computed by executing:

val th = p[]

This will be illustrated using REWRITE_TAC which takes a list of equations (empty in the example that follows) and tries to prove a goal by rewriting with these equations together with basic_rewrites:

- val goal2 = ([]:term list, ``T /\ x ==> x \/ (y /\ F)``);
> val goal2 = ([], ``T /\ x ==> x \/ y /\ F``) : (term list # term)

- REWRITE_TAC [] goal2;
> val it = ([], -) : (term list * term) list * (thm list -> thm)

- #2 it [];
> val it =  [] |- T /\ x ==> x \/ y /\ F : thm

Proved theorems are usually stored in the current theory so that they can be used in subsequent sessions.

The built-in function store_thm of ML type (string * term * tactic) -> thm facilitates the use of tactics: store_thm("foo",t,T) proves the goal ([],t) (i.e. the goal with no assumptions and conclusion t) using tactic T and saves the resulting theorem with name foo on the current theory.

If the theorem is not to be saved, the function prove of type (term * tactic) -> thm can be used. Evaluating prove(t,T) proves the goal ([],t) using T and returns the result without saving it. In both cases the evaluation fails if T does not solve the goal ([],t).

When conducting a proof that involves many subgoals and tactics, it is necessary to keep track of all the justification functions and compose them in the correct order. While this is feasible even in large proofs, it is tedious. HOL provides a package for building and traversing the tree of subgoals, stacking the justification functions and applying them properly; this package was originally implemented for LCF by Larry Paulson.

The subgoal package implements a simple framework for interactive proof. A proof tree is created and traversed top-down. The current goal can be expanded into subgoals using a tactic; the subgoals are pushed onto a goal stack and the justification function onto a proof stack. Subgoals can be considered in any order. If the tactic solves a subgoal (i.e. returns an empty subgoal list), then the package proceeds to the next subgoal in the tree.

The function set_goal of type goal -> void initializes the subgoal package with a new goal. Usually top-level goals have no assumptions; the function g is useful in this case.

To illustrate the subgoal package the trivial theorem |- " m. m+0=m will be proved from the definition of addition (we first open the theory of arithmetic and numLib, to bring the theorems and INDUCT_TAC to the top level):

- open arithmeticTheory numLib;
> ...
- ADD;
> val it = |- (!n. 0 + n = n) /\ (!m n. (SUC m) + n = SUC(m + n)) : thm

Notice that ADD specifies 0+m=m but not m+0=m. Of course, " m n. m+n = n+m is true, but the first step of the proof is to show " m. m+0=m from the definition of addition. Notice that the function g does not take a term as an argument, but rather a quotation, with only one set of back-quotes.

- g `!m. m+0=m`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !m. m + 0 = m

This sets up the goal. Next the goal is split into a basis and step case with INDUCT_TAC. To do this the function e (or, equivalently, expand) is used. This applies a tactic to the top goal on the stack, then pushes the resulting subgoals onto the goal stack, then prints the resulting subgoals. If there are no subgoals, the justification function is applied to the theorems solving the subgoals that have been proved and the resulting theorems are printed.

- e INDUCT_TAC;;
OK..
2 subgoals:
> val it =
    SUC m + 0 = SUC m
    ------------------------------------
      m + 0 = m

    0 + 0 = 0

The top of the goal stack is printed last. The basis case is an instance of the definition of addition, so is solved by rewriting with ADD.

- e(REWRITE_TAC[ADD]);
OK..

Goal proved.
 [] |- 0 + 0 = 0

Remaining subgoals:
> val it =
    SUC m + 0 = SUC m
    ------------------------------------
      m + 0 = m

The basis is solved and the goal stack popped so that its top is now the step case, namely showing that (SUC m) + 0 = SUC m under the assumption m + 0 = m. This goal can be solved by rewriting first with the definition of addition:

- e(REWRITE_TAC[ADD]);
OK..
1 subgoal:
> val it =
    SUC (m + 0) = SUC m
    ------------------------------------
      m + 0 = m

and then with the assumption m+0=m. The tactic ASM_REWRITE_TAC is used to rewrite with the assumptions of a goal. It is just like REWRITE_TAC except that it adds the assumptions to the list of equations used for rewriting. For the example here no equations besides the assumptions are needed, so ASM_REWRITE_TAC is given the empty list of equations.

- e(ASM_REWRITE_TAC[]);
OK..

Goal proved.
 [m + 0 = m] |- SUC (m + 0) = SUC m

Goal proved.
 [m + 0 = m] |- SUC m + 0 = SUC m
> val it =
    Initial goal proved.
     [] |- !m. m + 0 = m
    : GoalstackPure.goalstack

The top goal is solved, hence the preceding goal (the step case) is solved too, and since the basis is already solved, the main goal is solved.

The theorem achieving the goal can be extracted from the subgoal package with top_thm:

- top_thm();
val it = [] |- !m. m + 0 = m : thm

The proof just done can be `optimized'. For example, instead of first rewriting with ADD (box 4) and then with the assumptions (box 5), a single rewriting with ADD and the assumptions would suffice. To illustrate, the last two steps of the proof will be `undone' using the function backup (also, b) which restores the previous state of the goal and theorem stacks.

- b();
> val it =
    SUC (m + 0) = SUC m
    ------------------------------------
      m + 0 = m

- b();
> val it =
    SUC m + 0 = SUC m
    ------------------------------------
      m + 0 = m

The proof can now be completed in one step instead of two:

- e(ASM_REWRITE_TAC[ADD]);
OK..

Goal proved.
 [m + 0 = m] |- SUC m + 0 = SUC m
> val it =
    Initial goal proved.
     [] |- !m. m + 0 = m
    : GoalstackPure.goalstack

The order in which goals are attacked can be adjusted using rotate n (alternatively, r) which rotates the goal stack by n. For example:

- b(); b();
> ...

> val it =
    SUC m + 0 = SUC m
    ------------------------------------
      m + 0 = m

    0 + 0 = 0

- r 1;
> val it =
    0 + 0 = 0


    SUC m + 0 = SUC m
    ------------------------------------
      m + 0 = m

The top goal is now the step case not the basis case, so expanding with a tactic will apply the tactic to the step case.

- e(ASM_REWRITE_TAC[ADD]);
OK..

Goal proved.
 [m + 0 = m] |- SUC m + 0 = SUC m

Remaining subgoals:
> val it =
    0 + 0 = 0

It is possible to do the whole proof in one step, but this requires a compound tactic built using the tactical² THENL. Tacticals are higher order operations for combining tactics.

6.2 Tacticals

A tactical is an ML function that returns a tactic (or tactics) as result. Tacticals may take various parameters; this is reflected in the various ML types that the built-in tacticals have. Some important tacticals in the HOL system are listed below.

6.2.1 `THENL : tactic -> tactic list -> tactic`

If tactic T produces n subgoals and T₁, ... , T_n are tactics then T THENL [T₁;...;T_n] is a tactic which first applies T and then applies T_i to the ith subgoal produced by T. The tactical THENL is useful if one wants to do different things to different subgoals.

THENL can be illustrated by doing the proof of |- " m. m+0=m in one step.

- g `!m. m + 0 = m`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !m. m + 0 = m

- e(INDUCT_TAC THENL [REWRITE_TAC[ADD], ASM_REWRITE_TAC[ADD]]);
OK..
> val it =
    Initial goal proved.
     [] |- !m. m + 0 = m

The compound tactic INDUCT_TAC THENL [REWRITE_TAC[ADD];ASM_REWRITE_TAC[ADD]] first applies INDUCT_TAC and then applies REWRITE_TAC[ADD] to the first subgoal (the basis) and ASM_REWRITE_TAC[ADD] to the second subgoal (the step).

The tactical THENL is useful for doing different things to different subgoals. The tactical THEN can be used to apply the same tactic to all subgoals.

6.2.2 `THEN : tactic -> tactic -> tactic`

The tactical THEN is an ML infix. If T₁ and T₂ are tactics, then the ML expression T₁ THEN T₂ evaluates to a tactic which first applies T₁ and then applies T₂ to all the subgoals produced by T₁.

In fact, ASM_REWRITE_TAC[ADD] will solve the basis as well as the step case of the induction for " m. m+0=m, so there is an even simpler one-step proof than the one above:

- g `!m. m+0 = m`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !m. m + 0 = m

- e(INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);
OK..
> val it =
    Initial goal proved.
     [] |- !m. m + 0 = m

This is typical: it is common to use a single tactic for several goals. Here, for example, are the first four consequences of the definition ADD of addition that are pre-proved when the built-in theory arithmetic HOL is made.

   val ADD_0 = prove (
     ``!m. m + 0 = m``,
     INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);

   val ADD_SUC = prove (
     ``!m n. SUC(m + n) = m + SUC n``,
     INDUCT_TAC THEN ASM_REWRITE_TAC[ADD]);

   val ADD_CLAUSES = prove (
     ``(0 + m = m)              /\
       (m + 0 = m)              /\
       (SUC m + n = SUC(m + n)) /\
       (m + SUC n = SUC(m + n))``,
     REWRITE_TAC[ADD, ADD_0, ADD_SUC]);

   val ADD_COMM = prove (
     ``!m n. m + n = n + m``,
     INDUCT_TAC THEN ASM_REWRITE_TAC[ADD_0, ADD, ADD_SUC]);

These proofs are performed when the HOL system is made and the theorems are saved in the theory arithmetic. The complete list of proofs for this built-in theory can be found in the file src/num/arithmeticScript.sml.

6.2.3 `ORELSE : tactic -> tactic -> tactic`

The tactical ORELSE is an ML infix. If T₁ and T₂ are tactics, then T₁ ORELSE T₂ evaluates to a tactic which applies T₁ unless that fails; if it fails, it applies T₂. ORELSE is defined in ML as a curried infix by ³

(T₁ ORELSE T₂) g = T₁ g handle _ => T₂ g

6.2.4 `REPEAT : tactic -> tactic`

If T is a tactic then REPEAT T is a tactic which repeatedly applies T until it fails. This can be illustrated in conjunction with GEN_TAC, which is specified by:

!x.t[x]

t[x']

Where x' is a variant of x not free in the goal or the assumptions.

GEN_TAC strips off one quantifier; REPEAT GEN_TAC strips off all quantifiers:

- g `!x y z. x+(y+z) = (x+y)+z`;
> val it =
    Proof manager status: 1 proof.
    1. Incomplete:
         Initial goal:
         !x y z. x + (y + z) = x + y + z

- e GEN_TAC;
OK..
1 subgoal:
> val it =
    !y z. x + (y + z) = x + y + z

- e(REPEAT GEN_TAC);
OK..
1 subgoal:
> val it =
    x + (y + z) = x + y + z

6.3 Some tactics built into HOL

This section contains a summary of some of the tactics built into the HOL system (including those already discussed). The tactics given here are those that are used in the parity checking example.

Before beginning, allow the ML type thm_tactic to abbreviate thm->tactic, and the type conv⁴ to abbreviate term->thm.

6.3.1 `REWRITE_TAC : thm list -> tactic`

Summary: REWRITE_TAC[th₁,...,th_n] simplifies the goal by rewriting it with the explicitly given theorems th₁, ... , th_n, and various built-in rewriting rules.

{t₁, ... , t_m}t

{t₁, ... , t_m}t'

where t' is obtained from t by rewriting with
1. th₁, ... , th_n and
2. the standard rewrites held in the ML variable basic_rewrites.
Uses: Simplifying goals using previously proved theorems.
Other rewriting tactics:
1. ASM_REWRITE_TAC adds the assumptions of the goal to the list of theorems used for rewriting.
2. PURE_REWRITE_TAC uses neither the assumptions nor the built-in rewrites.
3. bossLib.RW_TAC of type simpLib.simpset -> thm list -> tactic. A simpset is a special collection of rewriting theorems and other theorem-proving functionality. Values defined by HOL include bossLib.base_ss, which has basic knowledge of the boolean connectives, bossLib.arith_ss which ``knows'' all about arithmetic, and HOLSimps.hol_ss, which includes theorems appropriate for lists, pairs, and arithmetic. Additional theorems for rewriting can be added using the second argument of RW_TAC.

6.3.2 `CONJ_TAC : tactic`

Summary: Splits a goal ``t₁/\t₂`` into two subgoals ``t₁`` and ``t₂``.

t₁ /\ t₂

t₁ t₂
Uses: Solving conjunctive goals. CONJ_TAC is invoked by STRIP_TAC (see below).

6.3.3 `EQ_TAC : tactic`

Summary: EQ_TAC splits an equational goal into two implications (the `if-case' and the `only-if' case):

u = v

u ==> v v ==> u
Use: Proving logical equivalences, i.e. goals of the form ``u=v'' where u and v are boolean terms.

6.3.4 `DISCH_TAC : tactic`

Summary: Moves the antecedent of an implicative goal into the assumptions.

u ==> v

{u}v
Uses: Solving goals of the form ``u ==> v`` by assuming ``u`` and then solving ``v``. STRIP_TAC (see below) will invoke DISCH_TAC on implicative goals.

6.3.5 `GEN_TAC : tactic`

Summary: Strips off one universal quantifier.

!x.t[x]

t[x']

Where x' is a variant of x not free in the goal or the assumptions.
Uses: Solving universally quantified goals. REPEAT GEN_TAC strips off all universal quantifiers and is often the first thing one does in a proof. STRIP_TAC (see below) applies GEN_TAC to universally quantified goals.

6.3.6 `bossLib.PROVE_TAC : thm list -> tactic`

Summary: Used to do first order reasoning, solving the goal completely if successful, failing otherwise. Using the provided theorems and the assumptions of the goal, PROVE_TAC does a search for possible proofs of the goal. Eventually fails if the search fails to find a proof shorter than a reasonable depth.
Uses: To finish a goal off when it is clear that it is a consequence of the assumptions and the provided theorems.

6.3.7 `STRIP_TAC : tactic`

Summary: Breaks a goal apart. STRIP_TAC removes one outer connective from the goal, using CONJ_TAC, DISCH_TAC, GEN_TAC, etc. If the goal is t₁/\···/\t_n ==> t then DISCH_TAC makes each t_i into a separate assumption.
Uses: Useful for splitting a goal up into manageable pieces. Often the best thing to do first is REPEAT STRIP_TAC.

6.3.8 `SUBST_TAC : thm list -> thm`

Summary: SUBST_TAC[|-u₁=v₁,...,|-u_n=v_n] converts a goal t[u₁,... ,u_n] to the subgoal form t[v₁,... ,v_n].
Uses: To make replacements for terms in situations in which REWRITE_TAC is too general or would loop.

6.3.9 `ACCEPT_TAC : thm -> tactic`

Summary: ACCEPT_TAC th is a tactic that solves any goal that is achieved by th.
Use: Incorporating forward proofs, or theorems already proved, into goal directed proofs. For example, one might reduce a goal g to subgoals g₁, ..., g_n using a tactic T and then prove theorems th₁ , ..., th_n respectively achieving these goals by forward proof. The tactic

T THENL[ACCEPT_TAC th₁,...,ACCEPT_TAC th_n]

would then solve g, where THENL is the tactical that applies the respective elements of the tactic list to the subgoals produced by T.

6.3.10 `ALL_TAC : tactic`

Summary: Identity tactic for the tactical THEN (see DESCRIPTION).
Uses:
1. Writing tacticals (see description of REPEAT in DESCRIPTION).
2. With THENL; for example, if tactic T produces two subgoals and we want to apply T₁ to the first one but to do nothing to the second, then the tactic to use is T THENL[T₁;ALL_TAC].

6.3.11 `NO_TAC : tactic`

Summary: Tactic that always fails.
Uses: Writing tacticals.

1: In higher order logic this is a derived rule; in first order logic it is usually primitive. In HOL the rule is called CONJ and its derivation is given in DESCRIPTION.
2: This word was invented by Robin Milner: `tactical' is to `tactic` as `functional' is to `function'.
3: This is a minor simplification.
4: The type conv comes from Larry Paulson's theory of conversions [9].


u `=` v

u `==>` v	v `==>` u

Chapter 6: Goal Oriented Proof: Tactics and Tacticals

6.1 Using tactics to prove theorems

6.2 Tacticals

6.2.1 THENL : tactic -> tactic list -> tactic

6.2.2 THEN : tactic -> tactic -> tactic

6.2.3 ORELSE : tactic -> tactic -> tactic

6.2.4 REPEAT : tactic -> tactic

6.3 Some tactics built into HOL

6.3.1 REWRITE_TAC : thm list -> tactic

6.3.2 CONJ_TAC : tactic

6.3.3 EQ_TAC : tactic

6.3.4 DISCH_TAC : tactic

6.3.5 GEN_TAC : tactic

6.3.6 bossLib.PROVE_TAC : thm list -> tactic

6.3.7 STRIP_TAC : tactic

6.3.8 SUBST_TAC : thm list -> thm

6.3.9 ACCEPT_TAC : thm -> tactic

6.3.10 ALL_TAC : tactic

6.3.11 NO_TAC : tactic