Adapted from Magnus Myreen’s cheatsheet. See also Arve Gengelbach’s tips and tricks.
This cheatsheet has been ported to the HOL4 website, with its source maintained in the HOL4 GitHub repository. Contributions welcome!
Table of contents
Join the #hol
channel on the CakeML Discord.
vimhol.sh
script to run side-by-side Vim and HOL4 using tmux
..hol-config.sml
(in your home directory):
val m = Hol_pp.print_apropos;
val f = Hol_pp.print_find;
This allows you to use the following in your HOL4 REPL:
m ``pattern``
to search for theorems with subterms matching the supplied pattern.f "string"
to search for theorems with names matching the supplied string.local
val pp = print o Hol_pp.data_list_to_string;
in
fun ff x y = DB.find y |> DB.find_in x |> pp;
fun mm x y = DB.apropos y |> DB.apropos_in x |> pp;
fun fm x y = DB.apropos y |> DB.find_in x |> pp;
fun mf x y = DB.find y |> DB.apropos_in x |> pp;
end;
These functions combine the functionality of m
and f
above, allowing you to nest two searches.
Use help "string"
in the HOL4 REPL to examine documentation for ML-level identifiers.
Bookmark the HOL4 online helpdocs, for quick access to interactive documentation. This is particularly useful for discovering useful definitions in theories.
You can also search for constants by type, using find_consts ``:type``
.
Be sure to open HolKernel boolLib bossLib BasicProvers dep_rewrite
interactively.
Otherwise, some of the tactics below may not be in scope.
f o g
- function compositionx |> f
- function application (i.e. f x
), useful for chainingf $ g x
- right-associative function application (i.e. f (g x)
, as in Haskell)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.
simp[theorems]
fs[theorems]
simp
, but also uses newer assumptions to rewrite older ones.rfs[theorems]
fs
, but reversed: uses older assumptions to rewrite newer ones.gs[theorems]
fs
and rfs
until no further change.gvs[theorems]
gs
, but also uses substitution to eliminate assumptions concerning equalities on variables.rw[theorems]
simp
, but also deconstructs the goal (stripping ∀
and ==>
, and splitting conjuncts into subgoals)DEP_REWRITE_TAC[theorems]
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.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]
{,asm_}rewrite_tac[theorems]
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]
{,asm_}rewrite_tac
, but performs a top-down descent of the goal and rewrites at most once per subtree.DEP_ONCE_REWRITE_TAC[theorems]
DEP_REWRITE_TAC
what once_rewrite_tac
is to rewrite_tac
.
DEP_ONCE_ASM_REWRITE_TAC
is analogous to once_asm_rewrite_tac
.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 SCONV
, REWRITE_CONV
, THENC
, RAND_CONV
, RATOR_CONV
, LHS_CONV
, RHS_CONV
, QCHANGED_CONV
, DEPTH_CONV
, PAT_CONV
, and PATH_CONV
.
These are used when rewriting: they modify the rewrite behaviour of the theorem to which they are applied.
Once theorem
Ntimes theorem int
Excl "theorem_name"
Excl "conversion_name"
Simp{L,R}HS theorem
Req{0,D} theorem
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
∀
-quantification.iff{LR,RL} theorem
cj n theorem
n
th conjunct of the theorem, handling universal quantifiers and implications.
For example, for thm = ⊢ ∀ P Q R . P ==> Q /\ R
, cj 2 thm
gives ⊢ ∀ P R . P ==> R)
.
NB indexing begins at 1
.SRULE [rewrites] theorem
Cong theorem
Cong AND_CONG
allows use of each conjunct in a conjunction to rewrite the others; and
the goal (∀ e. MEM e l ==> f e = g e) ==> h (MAP f l) = h (MAP g l)
is solved by simp[Cong MAP_CONG]
.oneline theorem
case
-expressions.
For example, oneline listTheory.MAP
gives ⊢ MAP f v = case v of [] => [] | h::t => f h::MAP f t
.lambdify theorem
⊢ ∀ x y z. f x y z = ...
into one of the form ⊢ f = (λx y z. ...)
.
Note that the above 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>
This is most useful for certain simpset fragments:
CONJ_ss
x = SUC n /\ if x = 0 then P else Q
transforms to x = SUC n /\ Q
using simp[SF CONJ_ss]
.SFY_ss
∃
-quantified goals using instantiations from assumptions/rewrites.ETA_ss
DNF_ss
Conversely, ExclSF
is like Excl
above, but can be used to exclude a set of rewrites.
ExclSF "simpset fragment name"
In some cases, a decision procedure can save you some work.
metis_tac[theorems]
decide_tac
intLib.COOPER_TAC
decide_tac
but for integers.blastLib.BBLAST_TAC
word32
and others).Many proofs rely on induction, and there are several ways to induct in HOL4.
Induct
∀
-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`
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
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`
measureInduct_on `term`
measureInduct_on `LENGTH l`
begins induction over the length of the list l
from the current goal.recInduct theorem
ho_match_mp_tac theorem
name_ind_cases theorem
>~
).It is often useful to perform case splits over the course of a proof.
Cases
∀
-quantified goal.Cases_on `term`
PairCases_on `var`
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.pairarg_tac
(λ(x,y,...). body) arg
, and introduces the assumption arg = (x,y,...)
.
This can often provide better naming than PairCases_on
.CASE_TAC
case
expression in the goal.FULL_CASE_TAC
CASE_TAC
, but picks the smallest case
expression in the goal and assumptions.TOP_CASE_TAC
CASE_TAC
, but picks the top-most case
expression.every_case_tac
case
expression.
This can be slow and explode the number of subgoals!IF_CASES_TAC
if ... then ... else ...
expression in the goal.CaseEq "string"
(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()
CaseEq
, but returns a conjunction of all currently-available cases theorems.
Most commonly used as gvs[AllCaseEqs()]
.Maintainable and readable files require organised proofs - in particular, careful management of subgoals.
tactic1 >> tactic2
tactic1 \\ tactic2
tactic1 THEN tactic2
tactic1
and then performs tactic2
on all subgoals produced.tactic1 >- tactic2
tactic1 THEN1 tactic2
tactic1
and then uses tactic2
to solve the first subgoal produced.
This fails if the second tactic does not completely solve the subgoal.`term` by tactic
qsuff_tac `term`
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
qsuff_tac
, but solves the first subgoal (i.e. that the supplied term implies the goal) using the given tactic.tactic >~ [`pat`s]
tactic
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.tactic >>~ [`pat`s]
>~
, but can match/rename multiple goals and bring them all to the top of the goal-stack.tactic1 >>~- ([`pat`s], tactic2)
>>~
, but tries to solve the matched/renamed goals using tactic2
.
This fails if any of the goals are not completely solved.rpt tactic
TRY tactic
TRY
is generally regarded as poor style.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
∀
-quantified variable, or splits a top-level conjunct into two subgoals.
When stripping an implication, strip_tac
breaks apart conjunctions, disjunctions, and existentials (e.g. stripping P /\ Q
introduces two assumptions, P
and Q
).conj_tac
conj_asm{1,2}_tac
conj_tac
, but adds the first/second conjunct (respectively) as an assumption for the other subgoal.disj{1,2}_tac
p \/ q
into p
or q
respectively.gen_tac
∀
-quantified variable.AP_TERM_TAC
f x = f y
to x = y
.AP_THM_TAC
f x = g x
to f = g
.MK_COMB_TAC
f x = g y
to two subgoals, f = g
and x = y
.iff_tac
eq_tac
P <=> Q
to two subgoals, P ==> Q
and Q ==> P
.impl_tac
(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 `term`
∃
quantifier with the supplied term.qexistsl [`term`s]
qexists
, but accepts a list of terms to instantiate multiple ∃
quantifiers.qrefine `term`
∃
quantifier 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 qrefine `SUC k` >> simp[]
produces the goal ∃ k : num. Q (SUC k)
(where SUC
is the successor function).qrefinel [`term`s]
qrefine
, but accepts a list of terms to instantiate multiple ∃
quantifiers.
Also can be passed underscores, to avoid refining selected ∃
quantifiers.
For example, for a goal n = 2 /\ c = 5 ==> ∃ a b c d. a + b = c + d
, the tactic strip_tac >> qrefinel [`_`,`SUC c`,`_`,`n + m`]
produces the new goal ∃ a c' m. a + SUC c = c' + (n + m)
.goal_assum $ drule_at Any
∃ 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.wlog_tac `term` [`variable`s]
wlog_tac
are additionally quantified over in the first subgoal.
See help "wlog_tac"
for examples.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
strip_assume_tac theorem
assume_tac
and strip_tac
: introduces the supplied theorem into the assumptions after deconstructing its conjunctions, disjunctions, and existentials.mp_tac theorem
goal
into theorem ==> goal
).disch_then thm_tactic
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
last_assum thm_tactic
last_x_assum thm_tactic
pop_assum thm_tactic
qpat_assum `pat` thm_tactic
qpat_x_assum `pat` thm_tactic
goal_term term_tactic
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
spose_not_then thm_tactic
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
.ASSUME_NAMED_TAC "label" theorem
markerLib
.
Add the theorem as an labelled assumption: label :- theorem
.
E.g. pop_assum $ ASSUME_NAMED_TAC "..."
.LABEL_ASSUM "label" thm_tactic
LABEL_X_ASSUM "label" thm_tactic
markerLib
.
Select the labelled assumption label :- assumption
and apply thm_tactic assumption
.L "label"
markerLib
.
When used in a stateful simplifier, produces the theorem assumption
from labelled assumption label :- assumption
.kall_tac
K ALL_TAC
, i.e. accepts any input and leaves the goal unchanged.
Most useful to delete assumptions, e.g. pop_assum kall_tac
removes the most recent assumption.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
∀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
drule
which attempts to match all the conjuncts P1, ..., Pn
.
This has a rev_drule_all
variant.drule_then theorem thm_tactic
drule
which processes the resulting instantiated theorem using a theorem-tactic, rather than adding it as an implication to the goal.
This has a rev_drule_then
variant.dxrule theorem
dxrule_all theorem
dxrule_then theorem thm_tactic
rev_*
variants.irule theorem
∀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
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
∀
-quantified) theorem with the given term, and applies the theorem-tactic to the result.qspecl_then [`tm`s] thm_tactic thm
qspec_then
, but instantiates multiple ∀
-quantified variables.imp_res_tac theorem
res_tac
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`
∀
quantifier).There are positional variants of irule
and drule
.
irule_at position theorem
irule theorem
within the goal, matching the conclusion at the position given by position
.drule_at position theorem
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
Pat `pattern`
Pos fun
fun : term list -> term
) to the list of conjuncts.
Pos hd
, Pos last
, and Pos $ el integer
are common uses.Concl
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.
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`
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`
qmatch_asmsub_abbrev_tac `pattern`
qmatch_goalsub_abbrev_tac
, but looks for matches in the assumptions only.qabbrev_tac `var = term`
qpat_abbrev_tac `var = pattern`
LET_ELIM_TAC
let x = e1 in e2
, abbreviates e1
to x
and transforms the goal to e2
.unabbrev_all_tac
Abbr `var`
x
is an abbreviation in the goal-state, using simp[Abbr `x`]
will unabbreviate x
in the goal.qx_gen_tac `var`
gen_tac
, but specialises the ∀
-quantified variable using the given name.qx_choose_then `var` thm_tactic thm
∃
-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
).namedCases_on `tm` ["string"s]
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, namedCases_on `l` ["", "head tail"]
performs a case split on list l
, naming the head
and tail
appropriately in the non-empty list case.Some patterns arise very often in proofs.
drule thm
- instantiates an antecedent of the theorem with an assumption.qspecl_then [...] assume_tac thm
- specialises a theorem and adds it to the assumptions.qspecl_then [...] mp_tac thm
- specialises a theorem and adds it as an implication to the goal.first_x_assum drule
- instantiates the first antecedent of an implicational assumption with another assumption (taking the newest if there are multiple).qpat_x_assum `...` $ irule_at Any
- select the implicational assumption matching the pattern, and match its conclusion against some part of the goal.
Remove that part of the goal, and add the (appropriately instantiated) antecedents of the assumptions to the goal.last_x_assum $ qspecl_then [...] mp_tac
- select an assumption which can be instantiated with the given variables, and add it as an implication to the goal (taking the oldest if there are multiple).pop_assum $ drule_then assume_tac
- drule
the newest assumption, and add it back as an assumption.disch_then drule
provides a useful continuation to drule
: takes A
from a goal of the form A ==> B
and effectively attempts drule A
.TOP_CASE_TAC >> gvs[] >> rename1 `...`
Cases_on ... >> simp[] >> qmatch_goalsub_abbrev_tac `...`
fs
, gvs
, and so on do too much, it can be useful to select an assumption, move it to the goal as an implication, and then use simp
instead.
This can prevent looping rewrites between assumptions.
E.g. qpat_x_assum `...` mp_tac >> simp[]
qpat_x_assum `...` $ rw o single
, leveraging the ML-level single
function which creates a singleton list.show_types := true
in your REPL and search for a discrepancy.
You cannot instantiate type variables once introduced into your goal-state for soundness reasons, so you must instead type-instantiate the assumption when it is introduced.
You can use INST_TYPE
for this, for example:assume_tac $ INST_TYPE [``:'a`` |-> ``:num``] listTheory.MAP