Adapted from Magnus Myreen's cheatsheet. See also Arve Gengelbach's tips and tricks.
Join the #hol channel on the CakeML Slack.
vimhol.sh script to run side-by-side Vim and HOL4 using tmux.Add the following to your .hol-config.sml (in your home directory):
val m = Hol_pp.print_apropos;
val f = Hol_pp.print_find;m ``pattern`` to search for theorems with subterms matching the supplied pattern.f "string" to search for theorems with names matching the supplied string.You can also add the following if you wish:
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 theoremNtimes theorem intExcl "theorem_name"Excl "conversion_name"Simp{L,R}HS theoremReq{0,D} theoremReq0 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} theoremcj n theoremnth 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] theoremCong theoremCong 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].
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_ssx = 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_ssDNF_ssIn some cases, a decision procedure can save you some work.
metis_tac[theorems]decide_tacintLib.COOPER_TACdecide_tac but for integers.
blastLib.BBLAST_TACword32 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 theoremInduct 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 theoremho_match_mp_tac theoremIt 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_TACcase expression in the goal.
FULL_CASE_TACCASE_TAC, but picks the smallest case expression in the goal and assumptions.
TOP_CASE_TACCASE_TAC, but picks the top-most case expression.
every_case_taccase expression. This can be slow and explode the number of subgoals!
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 >> tactic2tactic1 \\ tactic2tactic1 THEN tactic2tactic1 and then performs tactic2 on all subgoals produced.
tactic1 >- tactic2tactic1 THEN1 tactic2tactic1 and then uses tactic2 to solve the first subgoal produced. This fails if the second tactic does not completely solve the subgoal.
`term` by tacticqsuff_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 tacticqsuff_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 tacticTRY tacticTRY 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. Often rpt strip_tac (which repeats strip_tac as many times as possible) is used.
conj_tacconj_asm{1,2}_tacconj_tac, but adds the first/second conjunct (respectively) as an assumption for the other subgoal.
disj{1,2}_tacp \/ q into p or q respectively.
gen_tac∀-quantified variable.
AP_TERM_TACf x = f y to x = y.
AP_THM_TACf x = g x to f = g.
MK_COMB_TACf x = g y to two subgoals, f = g and x = y.
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.
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 theoremmp_tac theoremgoal into theorem ==> goal).
disch_then thm_tacticA ==> B, strips off A (i.e. discharges it) and applies the supplied theorem-tactic to it.
first_assum thm_tacticfirst_x_assum thm_tacticlast_assum thm_tacticlast_x_assum thm_tacticpop_assum thm_tacticqpat_assum `pat` thm_tacticqpat_x_assum `pat` thm_tacticgoal_term term_tacticfun : 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_tacticspose_not_then thm_tacticgoal_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" theoremmarkerLib. Add the theorem as an labelled assumption: label :- theorem. E.g. pop_assum $ ASSUME_NAMED_TAC "...".
LABEL_ASSUM "label" thm_tacticLABEL_X_ASSUM "label" thm_tacticmarkerLib. 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_tacK 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 theoremdrule which attempts to match all the conjuncts P1, ..., Pn.
drule_then theorem thm_tacticdrule which processes the resulting instantiated theorem using a theorem-tactic, rather than adding it as an implication to the goal.
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 theoremirule, 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 thmqspec_then, but instantiates multiple ∀-quantified variables.
imp_res_tac theoremres_tacimp_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 theoremirule theorem within the goal, matching the conclusion at the position given by position.
drule_at position theoremdrule 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:
AnyPat `pattern`Pos funfun : 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_TAClet x = e1 in e2, abbreviates e1 to x and transforms the goal to e2.
unabbrev_all_tacAbbr `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. If this is the case, 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