HOL4 tactic cheatsheet
======================
*Rewriting* -- The nicest HOL proofs are ones where rewriting does
most of the job. The most frequently used tactics are:
simp [thms] -- simplifies goal using assumptions, stateful simpset
and decision procedures for natural numbers
fs [thms] -- similar to simp but also simplifies assumptions from
bottom upwards (newer assumptions rewrite old ones)
rfs [thms] -- is the same as fs but applies to assumptions in
reverse order i.e. from top downwards
rw [thms] -- similar to simp, but this does more in that it
deconstructs the goal, e.g. it tries to split the goal
into several subgoals
If those above are doing too much, then try:
pure_rewrite_tac [thms] -- this just applies the given theorems as
rewrite rules (no smarts with arithmetic etc)
rewrite_tac [thms] -- almost the same as above, except this will also
do basic simplification of boolean expressions
asm_rewrite_tac [thms] -- same as above but uses assumptions of the
current goal as rewrites in addition to
given theorems
once_rewrite_tac [thms] and
once_asm_rewrite_tac [thms] -- perform a top-down descent and
perform at most one rewrite per
subtree
If these are still too blunt, then one can resort to the equivalent of
"assembly programming" for rewriting:
CONV_TAC conversion -- applies the given conversion to the current
goal; a conversion is a function of type
term -> thm such that given a term t it produces
a theorem |- t = t', for some reformulation t';
there are many conversion combinators,
e.g. RAND_CONV, RATOR_CONV, THENC, and
some for rewriting, e.g. REWRITE_CONV [thms].
*Provers* -- If you are lucky a decision procedure can prove your
goal.
decide_tac -- proves linear arithmetic over the natural numbers
(type: num)
intLib.COOPER_TAC -- proves similar goals for intergers (type: int)
metis_tac [thms] -- attempts to find a solution using a first-order
logic prover using the given theorems, thms
blastLib.BBLAST_TAC -- bit-blasting (i.e. SAT) for goals about only
words (wordsTheory), note: all types must be
concrete, e.g. word32 instead of 'a word
*Induction* -- Many proofs start by applying an induction theorem.
Induct_on `term` -- starts an induction theorem based on the type of
the given term, e.g. Induct_on `n` in a goal
`∀k n:num. n ≤ k + n` will produce two subgoals
one for the base case 0 and one for the step case.
Induct -- does the same but uses the first variable in a
∀-quantified goal for the induction. An application of
Induct to the example goal above would produce an
induction on k.
completeInduct_on `term` -- starts a strong (or complete) induction
on the natural numbers, i.e. only one
subgoal but one gets to assume the goal
for all instances strictly less than the
goal instance.
recInduct ind_thm and
ho_match_mp_tac ind_thm -- starts an induction based on an induction
theorem, i.e. a theorem one gets from the
definition of a recursive function or an
inductive relation
*Case splits* -- Tactics for performing case splits.
Cases_on `term` -- performs a case split on the given term
Cases -- performs a case split on the first ∀-quantified variable in
the goal; requires goal to have top-level ∀-quantifier
PairCases_on `p` -- given a variable p of a pair type, this tactic
instantiates p with (p1,p2,...,pn) if p is an
n-tuple. (This usually provides better names
than repeated applications of Cases_on)
CASE_TAC -- looks for case statements in the goal and performs a
case split on the smallest case expression
TOP_CASE_TAC -- performs a case split on the top-most case
expression
every_case_tac -- performs a case split on every case expression;
this is handy but can be slow and can cause an
explosion of cases.
*Subgoals and tactic combinators* -- The following will help you
organise proofs with subgoals.
\\ and THEN and >> -- are names for THEN, which is used to compose
two tactics and make one, e.g. tac1 // tac2
runs tac1 and then tac2; if tac1 produces
several subgoals then tac2 is run on all new
subgoals
THEN1 and >- -- both mean the same, tac1 THEN1 tac2 applies tac2 to
the first subgoal and fails if tac2 fails to finish
the proof of the first subgoal
sg `goal` -- starts a new subgoal and inserts goal as an assumption
in the goal that existed before calling sg
`goal` by tactic -- this starts a new subgoal and proves it
immediately with the tactic provided; it fails
if the tactic fails to prove the local goal
rpt tactic -- repeats the given tactic until it fails
TRY tactic -- apply the given tactic once; in case the tactic fails,
then rewind the goal
*Goal deconstruction* -- Longer and more delicate proofs require
manually stating how the goal is to be taken apart.
rpt strip_tac -- repeats strip_tac, which attempts to split a
top-level conjunct into two subgoals, move an
implication into the assumptions or remove a
top-level ∀-quantified variable.
conj_tac -- splits a top-level conjunction into two subgoals
impl_tac -- given a goal of the form `(A ==> B) ==> C`, impl_tac
produces two subgoals: `A` and `B ==> C`; this is often
handy in combination with drule, see below
qexists_tac `term` -- instantiates a top-level existential quantifier
with the given term
asm_exists_tac -- if the goal has the form `∃vars. P vars /\ Q ...`
then asm_exists_tac tries to find a match for `P
vars` in the assumptions, if it finds a match it
then instantiates vars and removes `P vars` from
the goal
*Instantiations* -- Occasionally, inductive hypothesis or lemmas need
to be manually instantiated. The following are the most common ways
of instantion:
drule thm -- if thm has the form `∀vars. P /\ Q /\ ... ==> ..` then
drule thm will look through the assumptions (bottom up)
in search for one that matches P. If a match is found,
then drule instantiates vars so that P can be
discharged, the result is added as an implication to
the current goal
disch_then drule -- is a nice continuation of drule from above,
disch_then picks `A` from the goal if it has the
shape `A ==> B`; in the example above,
disch_then drule will attempt to find a match
for Q and instantiate the remaining vars
accordingly, again leaving the result as an
implication on the current goal
pop_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac)
first_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac)
first_x_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac)
qpat_assum `pat` (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac)
qpat_x_assum `pat` (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac)
-- these pick an assumption from the assumptions list and
instantiate its ∀-quantified variables with the terms `t1`,
`t2` etc. the resulting term is added as a new implication onto
the current goal, due to mp_tac; alternatively, one can use
assume_tac or strip_assume_tac to instead introduce the new
term as a new assumption. Difference between all of these is in
how they pick the assumption to instantiate:
- pop_assum: always picks the last assumption, and removes it
- first_assum: picks the first for which qspecl_then succeeds
- first_x_assum: same as above but also removes the assumption
- qpat_assum: picks an assumption that matches the pattern pat
- qpat_x_assum: same as above but also removes the assumption
Note: it is common to use qspecl_then .. for pop_assum, first_assum
etc. However, any ML function of type thm -> tactic will suffice,
e.g. it can be handy to write first_x_assum drule.
imp_res_tac thm -- tries to add all immediate consequences of the
given theorem, thm, to the assumptions of the
current goal; the thm needs to be an implication;
warning: imp_res_tac can cause an explosion in
the number of assumptions
res_tac -- is similar to imp_res_tac but takes no argument, instead
res_tac attempts to find all consequences of combining
all of the assumptions via modus ponens; res_tac should
be used carefully to make sure the assumptions list does
not get too long or full of junk
*Renaming and abbreviating* -- HOL4 sometimes generates names, e.g. q'
or r''', and large expression. These can be annoying and can lead to
brittle proofs.
rename1 `pat` -- will look to match pat with something in the goal,
assumptions or some part of them; it renames all
variables to match those given in the pattern,
e.g. rename1 `n + _ <= _` turns an assumption `q''
+ k <= 4` into `n + k <= 4`, if the goal did not
have something that matched `n + _ <= _`
qmatch_asmsub_rename_tac `pat` -- is more specific than rename1: it
looks for some match in an
assumption and ignores the goal
qmatch_goalsub_rename_tac `pat` -- same as above but for the goal
only, ignores assumptions
qabbrev_tac `foo = large-term-here` -- replaces a large term with a
given name, e.g. foo
qpat_abbrev_tac `foo = pat` -- same as above but tries to find the
exact term from the goal, e.g. if pat
is `_ + _` then foo might abbreviate
`n+4`