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

Join the

`#hol`

channel on the CakeML Slack.- Learn how to interact with HOL4 using the documentation.
- For Emacs, the short guide or complete documentation.
- For Vim, the plugin documentation. At first, you should use the
`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):

This allows you to use the following in your HOL4 REPL:`val m = Hol_pp.print_apropos; val f = Hol_pp.print_find;`

`m ```

to search for theorems with subterms matching the supplied pattern.*pattern*```f "`

to search for theorems with names matching the supplied string.*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 "`

in the HOL4 REPL to examine documentation for ML-level identifiers.*string*"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.- Remember that HOL4 exposes various useful ML bindings, including:
`f o g`

- function composition`x |> f`

- function application (i.e.`f x`

), useful for chaining`f $ 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*]- 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.

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`

.

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 `

. There are many conversions and conversion combinators - an exhaustive list can be found in the HOL4 documentation, mostly listed under the *conversion*`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*- 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.
`Excl`

*theorem*- Do not use the supplied theorem when rewriting. This allows temporary exclusion of a theorem from the stateful simpset.
`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{LR,RL}`

*theorem*- Turns a bi-implication into an implication, going left-to-right or right-to-left respectively.
`SRULE [`

*rewrites*]*theorem*- Uses the stateful simpset and supplied rewrites to rewrite the theorem.
`Cong`

*theorem*- Uses the supplied theorem as a
*congruence rule*instead of a rewrite. Congruence rules tell the simplifier how to traverse terms, so they can be useful for rewriting within subterms. For example, using`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]`

.

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>*- 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.

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).

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 ``

to specify a particular induction theorem for use. For example,*term*``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.
`measureInduct_on ``

*term*`- Begins strong/complete induction using the supplied measure. This should be in the form of a measure function (one which returns a natural number) applied to an input variable which is currently free in the goal. For example,
`measureInduct_on `LENGTH l``

begins induction over the length of the list`l`

from the current goal. `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.

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. `pairarg_tac`

- Searches the goal and assumptions for
`(λ(x,y,...). body) arg`

, and introduces the assumption`arg = (x,y,...)`

. This can often provide better naming than`PairCases_on`

. `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()]`

.

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

*tactic1*>>*tactic2**tactic1*\\*tactic2**tactic1*THEN*tactic2*- Performs
and then performs`tactic1`

on all subgoals produced.`tactic2`

*tactic1*>-*tactic2**tactic1*THEN1*tactic2*- Performs
and then uses`tactic1`

to solve the first subgoal produced. This fails if the second tactic does not completely solve the subgoal.`tactic2`

```

*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. *tactic*>~ [`*pat*`s]- Performs
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`

*tactic*>>~ [`*pat*`s]- Like
`>~`

, but can match/rename multiple goals and bring them all to the top of the goal-stack. *tactic1*>>~- ([`*pat*`s],*tactic2*)- Like
`>>~`

, but tries to solve the matched/renamed goals using. This fails if any of the goals are not completely solved.`tactic2`

`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.

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. `disj{1,2}_tac`

- Reduces a goal of the form
`p \/ q`

into`p`

or`q`

respectively. `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`

. `MK_COMB_TAC`

- Reduces a goal of the form
`f x = g y`

to two subgoals,`f = g`

and`x = y`

. `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 ``

*term*`- Instantiates a top-level
`∃`

quantifier with the supplied term. `qexistsl ``

*terms*`- Like
`qexists`

, but accepts a list of terms to instantiate multiple`∃`

quantifiers. `qrefine ``

*term*`- Refines a top-level
`∃`

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 ``

*terms*`- Like
`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 [``

produces the new goal*`,`SUC c`,`*`,`n + m`]`∃ a c' m. a + SUC c = c' + (n + m)`

. `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.

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

, applies*fun*: term -> tacticto the current goal (i.e. a`fun`

`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`

. `ASSUME_NAMED_TAC "`

*label*"*theorem*- Found in
`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*- Found in
`markerLib`

. Select the labelled assumption`label :- assumption`

and apply

.*thm_tactic*assumption `L "`

*label*"- Found in
`markerLib`

. When used in a stateful simplifier, produces the theorem`assumption`

from labelled assumption`label :- 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*- 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).

There are positional variants of `irule`

and `drule`

.

`irule_at`

*position theorem*- Applies
`irule`

within the goal, matching the conclusion at the position given by*theorem*.`position`

`drule_at`

*position theorem*- Applies
`drule`

, but attempts to match/instantiate the conjunct given by*theorem*.`position`

The

is expressed as a value of type *position*`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

) to the list of conjuncts.*fun*: term list -> term`Pos hd`

,`Pos last`

, and`Pos $ el`

are common uses.*integer* `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.

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*`- When used in a stateful simplifier, 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`

). `namedCases_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,`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.

**Introduction and instantiation of theorems.**`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.

**Assumption selection followed by instantiation.**These patterns arise very commonly, particularly during inductive proof. Almost any assumption selection function can be used with almost any theorem-tactic - here are a few examples.`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`

.*and so on*

**Case splits followed by simplification and renaming.**Case splits introduce fresh variable names and equalities. Simplification can use the equalities, and renaming cleans up the fresh names.`TOP_CASE_TAC >> gvs[] >> rename1 `...``

`Cases_on _ >> simp[] >> qmatch_goalsub_abbrev_tac `...``

*and so on*

**Simpler targeted simplification.**Sometimes when`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[]`

- We can select single assumptions to use as rewrites too:
`qpat_x_assum `...` $ rw o single`

, leveraging the ML-level`single`

function which creates a singleton list.

- We can select single assumptions to use as rewrites too:
**Rewrites which don't seem to do anything.**Sometimes it may seem that you have an assumption which should trigger simplification in the goal on rewriting - however, it doesn't seem to be doing anything. Often this is due to a type mismatch - i.e. your assumption involves more general types than your goal. To diagnose it you can turn types annotations on using for instance`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`