Adapted from Magnus Myreen's cheatsheet. See also Arve Gengelbach's tips and tricks.

Preliminaries

Rewriting

HOL4 has a powerful rewriting engine, and the cleanest proofs let it do the heavy lifting. Note that a stateful set of rewrites is maintained by HOL4 - the stateful simpset.

General purpose tactics

simp[theorems]
Simplifies the goal using current assumptions, the stateful simpset, and decision procedures for the natural numbers.
fs[theorems]
Like simp, but also uses newer assumptions to rewrite older ones.
rfs[theorems]
Like fs, but reversed: uses older assumptions to rewrite newer ones.
gs[theorems]
Effectively repeats fs and rfs until no further change.
gvs[theorems]
Like gs, but also uses substitution to eliminate assumptions concerning equalities on variables.
rw[theorems]
Like simp, but also deconstructs the goal (stripping and ==>, and splitting conjuncts into subgoals)
DEP_REWRITE_TAC[theorems]
Rewrites the goal using the supplied dependent rewrites, introducing dependencies as conjuncts in the goal. For example, given a goal P and a rewrite thm = ⊢ R ==> P = Q, DEP_REWRITE_TAC[thm] will transform the goal into R /\ Q. DEP_ASM_REWRITE_TAC is a variant which additionally uses the assumptions as rewrites. Note that this can loop more often than other rewriting tactics.

More fine-grained tactics

In some cases, the general purpose tactics above do too much simplification, or can loop. Instead, there are more precise tactics we can use.

pure_rewrite_tac[theorems]
Rewrites the goal using only the supplied theorems (i.e. no stateful simpset rewrites).
{,asm_}rewrite_tac[theorems]
Like pure_rewrite_tac, but also uses basic boolean expression rewrites. The asm_rewrite_tac variant additionally uses the assumptions as potential rewrites.
once_{,asm_}rewrite_tac[theorems]
Like {,asm_}rewrite_tac, but performs a top-down descent of the goal and rewrites at most once per subtree.
DEP_ONCE_REWRITE_TAC[theorems]
Is to DEP_REWRITE_TAC what once_rewrite_tac is to rewrite_tac. DEP_ONCE_ASM_REWRITE_TAC is analogous to once_asm_rewrite_tac.

Conversions

If these are still too blunt, we can use conversions to carry out surgical rewrites. Conversions are functions of type term -> thm, such that applying a conversion to a term t produces a theorem ⊢ t = t'. These can be converted into tactics using CONV_TAC conversion. There are many conversions and conversion combinators - an exhaustive list can be found in the HOL4 documentation, mostly listed under the Conv structure. Good starting points are REWRITE_CONV, THENC, RAND_CONV, RATOR_CONV, LHS_CONV, RHS_CONV, QCHANGED_CONV, DEPTH_CONV, PAT_CONV, and PATH_CONV.

Rewrite modifiers

These are used when rewriting: they modify the rewrite behaviour of the theorem to which they are applied.

Once theorem
Uses the supplied theorem at most once when rewriting.
Ntimes theorem int
Uses the supplied theorem at most the given number of times when rewriting.
Simp{L,R}HS theorem
Uses the supplied theorem to simplify on the left-/right-hand side of equalities.
Req{0,D} theorem
Requires the supplied theorem to be used a number of times, by checking the number of subterms matching the LHS of the rewrite after simplification. Req0 requires no matching subterms after simplification, ReqD requires the number to have strictly decreased - otherwise, an exception is thrown. This is most useful for ensuring that conditional rewrites have fired.


Also commonly used when rewriting are:

GSYM theorem
Flips equalities in the conclusion of the theorem. This works even when the equality is nested below implications and/or -quantification.
iff{L,R} theorem
Turns a bi-implication into an implication, going left-to-right or right-to-left respectively.


Note that GSYM and iff{L,R} are termed rules - these transform theorems to other theorems, allowing the above to be combined (e.g. simp[Once $ GSYM thm]). There are many other useful rules - see the HOL4 documentation for more details.

In some cases we may wish to use a set of rewrites for simplification. One way to do this is to use the SF modifier in our list of rewrites, e.g. simp[SF CONJ_ss].

SF <simpset fragment>
Turns the simpset fragment into a theorem encapsulating its rewrite behaviour, which can be passed in a list of rewrites.


This is most useful for certain simpset fragments:

CONJ_ss
Rewrites over conjuncts. This can deduplicate conjuncts, and use each conjunct to help simplify the others. For example, the goal x = SUC n /\ if x = 0 then P else Q transforms to x = SUC n /\ Q using simp[SF CONJ_ss].
SFY_ss
Rewrites to prove simple -quantified goals using instantiations from assumptions/rewrites.
ETA_ss
Rewrites to remove eta-expansion.
DNF_ss
Rewrites to convert to disjunctive normal form.

Provers

In some cases, a decision procedure can save you some work.

metis_tac[theorems]
First-order decision procedure using the supplied theorems. Note that this can easily loop if given too much information.
decide_tac
Linear arithmetic over the natural numbers.
intLib.COOPER_TAC
Like decide_tac but for integers.
blastLib.BBLAST_TAC
Bit-blasting (i.e. SAT) for goals concerning concrete word types (i.e. word32 and others).

Induction

Many proofs rely on induction, and there are several ways to induct in HOL4.

Induct
Inducts over the first variable in a -quantified goal, based on the type of the variable. For example, applying Induct to ∀ n : num. P n begins induction over the natural number n, giving a base case 0 and a step/successor case.
Induct_on `term`
Inducts over the given term, based on its type. This can be used similarly to Induct - e.g. to prove P (n : num) we can use Induct_on `n`. However, we can also induct over an inductive relation - given a relation is_even and a goal is_even n, we can use Induct_on `is_even`.
_ using theorem
Used as as suffix to Induct or Induct_on `term` to specify a particular induction theorem for use. For example, Induct_on `l` using SNOC_INDUCT begins induction over list l from the tail, rather than the head (SNOC is the reverse of CONS).
completeInduct_on `term`
Begins strong/complete induction on the supplied natural number. In other words, the inductive hypothesis is over all numbers strictly less than the goal instance.
recInduct theorem
ho_match_mp_tac theorem
Induction using the supplied theorem, which usually arises from definition of a recursive function or an inductive relation.

Case splits

It is often useful to perform case splits over the course of a proof.

Cases
Case splits on the first variable in a -quantified goal.
Cases_on `term`
Case splits on the supplied term.
PairCases_on `var`
Given a variable p of a pair type, instantiates p to (p0,p1,...,pn). This provides better naming than Cases_on, and requires fewer case splits for n-tuples where n is greater than 2.
CASE_TAC
Case splits the smallest case expression in the goal.
FULL_CASE_TAC
Like CASE_TAC, but picks the smallest case expression in the goal and assumptions.
TOP_CASE_TAC
Like CASE_TAC, but picks the top-most case expression.
every_case_tac
Splits every possible case expression. This can be slow and explode the number of subgoals!
CaseEq "string"
Returns a theorem of the form (case x of ...) = v <=> ..., where the type of x is given by the supplied string. This is intended for use with simplification, where it can help remove tautologies/absurdities in case expressions.
AllCaseEqs()
Like CaseEq, but returns a conjunction of all currently-available cases theorems. Most commonly used as gvs[AllCaseEqs()].

Subgoal management

Maintainable and readable files require organised proofs - in particular, careful management of subgoals.

tactic1 >> tactic2
tactic1 \\ tactic2
tactic1 THEN tactic2
Performs tactic1 and then performs tactic2 on all subgoals produced.
tactic1 >- tactic2
tactic1 THEN1 tactic2
Performs tactic1 and then uses tactic2 to solve the first subgoal produced. This fails is the second tactic does not completely solve the subgoal.
`term` by tactic
Creates a new subgoal from the given term, and solves it with the given tactic. The proved subgoal is added as an assumption for the rest of the proof.
qsuff_tac `term`
In some ways a dual of by above: attempts a "suffices by" proof. Adds the supplied term as an implication to the current goal, and adds the term itself as a new subgoal.
`term` suffices_by tactic
Like qsuff_tac, but solves the first subgoal (i.e. that the supplied term implies the goal) using the given tactic.
tactic1 >~ [`pat`s]
Performs tactic1 and then searches for the first subgoal with subterms matching the supplied patterns. Renames these subterms to match the patterns, and brings the goal into focus as the current goal.
tactic1 >>~ [`pat`s]
Like >~, but can match/rename multiple goals and bring them all to the top of the goal-stack.
rpt tactic
Repeats the given tactic until it fails.
TRY tactic
Attempts to apply the given tactic - but if it fails, leaves the goal unchanged.
NB use of TRY is generally regarded as poor style.

Goal deconstruction

In many cases, we may want to state exactly how the goal should be taken apart (rather than simply applying rw[] or similar).

strip_tac
Splits a top-level conjunct into two subgoals, or move a top-level implication antecedent into the assumptions, or remove a top-level -quantified variable. Often rpt strip_tac (which repeats strip_tac as many times as possible) is used.
conj_tac
Splits a top-level conjunct into two subgoals.
conj_asm{1,2}_tac
Like conj_tac, but adds the first/second conjunct (respectively) as an assumption for the other subgoal.
gen_tac
Removes a top-level -quantified variable.
AP_TERM_TAC
Reduces a goal of the form f x = f y to x = y.
AP_THM_TAC
Reduces a goal of the form f x = g x to f = g.
impl_tac
For a goal of the form (A ==> B) ==> C, splits into the two subgoals A and B ==> C. impl_keep_tac is a variant which keeps A as an assumption in the B ==> C subgoal.
qexists_tac `term`
Instantiates a top-level quantifer with the supplied term.
Q.REFINE_EXISTS_TAC `term`
Refines a top-level quantifer using the supplied term - any free variables in the term become-quantified. For example, for a goal ∃ n : num. if n = 0 then P n else Q n, applying Q.REFINE_EXISTS_TAC `SUC k` >> simp[] produces the goal ∃ k : num. Q (SUC k) (where SUC is the successor function).
goal_assum $ drule_at Any
For a goal of the form ∃ vars . P1 /\ ... /\ Pn (where the vars may be free in the Pi), attempts to match the Pi against the assumptions. If a match is found for some Pk, the relevant vars are instantiated and Pk is removed from the goal.

Assumption management

Managing assumptions is key to making progress in many goal states. This involves both the introduction and selection of assumptions.

Note that when we select an assumption, we usually want to process it further. In these cases, we use functions of type (thm -> tactic) -> tactic - i.e. they select an assumption (of type thm), apply the given function (of type thm -> tactic, pronounced "theorem-tactic", and abbreviated thm_tactic) to it, and return the resulting tactic. These functions tend to have at least two variants: one which leaves the original assumption untouched (only operating on a copy), and one which removes the original assumption. The latter usually have a "_x_" in their names.

assume_tac theorem
Introduces the supplied theorem into the assumptions.
mp_tac theorem
Introduces the supplied theorem into the goal as an implication (i.e. transforms the goal into theorem ==> goal).
disch_then thm_tactic
Given a goal of the form A ==> B, strips off A (i.e. discharges it) and applies the supplied theorem-tactic to it.
first_assum thm_tactic
first_x_assum thm_tactic
Applies the theorem-tactic to the first/newest assumption on which it succeeds.
last_assum thm_tactic
last_x_assum thm_tactic
Applies the theorem-tactic to the last/oldest assumption on which it succeeds.
pop_assum thm_tactic
Removes the first/newest assumption and applies the theorem-tactic to it.
qpat_assum `pat` thm_tactic
qpat_x_assum `pat` thm_tactic
Attempts to find an assumption matching the supplied pattern and applies the theorem-tactic to it.
goal_term term_tactic
Given fun : term -> tactic, applies fun to the current goal (i.e. a term). This is useful for programmatically selecting/specialising tactics based on the goal.
goal_assum thm_tactic
Applies the given theorem-tactic to the negated goal - i.e. select the goal as a negated assumption.
spose_not_then thm_tactic
Like goal_assum, but geared towards proof-by-contradiction: negates the goal and pushes the negation inwards, before applying the given theorem-tactic to the result. A common usage is spose_not_then assume_tac.

Instantiations and generalisations

It is common to require instantiation of general inductive hypotheses or lemmas to more specific forms. In some cases, it is useful to generalise a goal in order to use a suitable induction theorem.

drule theorem
Given a theorem of the form ∀vars. P1 /\ ... /\ Pn ==> Q, look through the assumptions (newest to oldest) to find a matching for P1. If a match is found the relevant vars are instantiated, and the remaining ∀vars'. P2 /\ ... /\ Pn => Q is added as an implication to the goal. rev_drule looks through assumptions in the opposite order.
drule_all theorem
A variant of drule which attempts to match all the conjuncts P1, ..., Pn.
drule_then theorem thm_tactic
A variant of drule which processes the resulting instantiated theorem using a theorem-tactic, rather than adding it as an implication to the goal.
irule theorem
Attempts to convert the supplied theorem into the form ∀vars. P1 /\ ... /\ Pn ==> Q, matches Q against the goal, and if successful instantiates the necessary variables to turn the goal into ∃vars'. P1 /\ ... /\ Pn. This is effectively the reverse of modus ponens.
ho_match_mp_tac theorem
Like irule, but carries out higher-order matching and does not attempt to convert the input theorem. Wherever possible, irule should be used - however when the goal itself is -quantified, it may be necessary to use ho_match_mp_tac.
qspec_then `tm` thm_tactic thm
Instantiates the supplied (-quantified) theorem with the given term, and applies the theorem-tactic to the result.
qspecl_then [`tm`s] thm_tactic thm
Like qspec_then, but instantiates multiple -quantified variables.
imp_res_tac theorem
Adds add all immediate consequences of the supplied theorem to the assumptions (i.e. performs resolution). The theorem should be an implication or bi-implication. Note that this can cause an explosion in the number of assumptions.
res_tac
Like imp_res_tac, but resolves all assumptions with each other (it takes no input theorem). This can easily cause an explosion in the number of assumptions.
qid_spec_tac `variable`
Generalises the supplied variable in the goal (i.e. introduces a quantifier).

Positional modifiers

There are positional variants of irule and drule.

irule_at position theorem
Applies irule theorem within the goal, matching the conclusion at the position given by position.
drule_at position theorem
Applies drule theorem, but attempts to match/instantiate the conjunct given by position.


The position is expressed as a value of type match_position, with values and meanings:

Any
Any position which succeeds.
Pat `pattern`
Any position which matches the pattern.
Pos fun
The position given by applying the supplied function (where fun : term list -> term) to the list of conjuncts. Pos hd, Pos last, and Pos $ el integer are common uses.
Concl
Match against the negated conclusion, i.e. use the implication in a contrapositive way.


By way of example, given a goal ∃x y. P x /\ Q y and a theorem thm = ⊢ R a b ==> P b, irule_at Any thm produces the goal ∃a y. R a b /\ Q y. irule_at (Pos hd) thm is equivalent in this case.

Renaming and abbreviating

HOL4 automatically generates fresh names where necessary, e.g. for case splits and existential witnesses. This is usually by appending apostrophes, and the resulting names become ugly. Sometimes large terms are generated too, and these are unwieldy.

Small changes to proofs can change variable naming and large expression structure quite easily - explicitly relying on automatically-chosen variable names or the exact phrasing of large expressions can lead to brittle proofs. Both are therefore bad style. Instead, we can rename variables appropriately, and abbreviate large terms.

rename1 `pattern`
Matches the pattern against a subterm in the goal or assumptions, and renames the subterm to match the pattern. For example, rename1 `n + _ <= foo` renames a + b <= c + d into n + b <= foo. Note that we have lost information here on the RHS.
qmatch_goalsub_abbrev_tac `pattern`
Matches the pattern to a subterm in the goal, abbreviating the matching subterm to fit the pattern. Unlike renaming, abbreviating preserves information - assumptions are introduced which keep track of the abbreviations.
qmatch_asmsub_abbrev_tac `pattern`
Like qmatch_goalsub_abbrev_tac, but looks for matches in the assumptions only.
qabbrev_tac `var = term`
Abbreviates an exact given term to the supplied variable.
qpat_abbrev_tac `var = pattern`
Matches the pattern to a subterm of the goal, and abbreviates the matching subterm to the supplied variable.
LET_ELIM_TAC
Given a goal of the form let x = e1 in e2, abbreviates e1 to x and transforms the goal to e2.
unabbrev_all_tac
Unabbreviates all existing abbreviations.
Abbr `var`
Produces a rewrite theorem which unabbreviates the supplied variable. For example, if x is an abbreviation in the goal-state, using simp[Abbr `x`] will unabbreviate x in the goal.
qx_gen_tac `var`
Like gen_tac, but specialises the -quantified variable using the given name.
qx_choose_then `var` thm_tactic thm
Takes the theorem supplied, which should be -quantified, and "chooses" the witness for the quantification to be the supplied variable. Processes the result using the supplied theorem tactic (often mp_tac or assume_tac).
tmCases_on `tm` ["string"s]
Like Cases_on, but allows naming of introduced variables. Each string in the list corresponds to a case, and multiple names are separated by a space. For example, tmCases_on `l` ["", "head tail"] performs a case split on list l, naming the head and tail appropriately in the non-empty list case.

Examples and common patterns

Some patterns arise very often in proofs.