# HOL4 tactics and tips & tricks

In the following we document tactics and tips & tricks for the HOL4 theorem prover. Some of those are extracted from discussions on the CakeML Slack, some are found in code and some are own work.

# Boolean expressions

• Overall useful theorems (e.g. for use with `Ho_Rewrite.REWRITE_RULE` and possibly `GSYM`)
• `FORALL_AND_THM`
`⊢ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x`
• `DISJ_EQ_IMP`
`⊢ ∀A B. A ∨ B ⇔ ¬A ⇒ B`
• `IMP_CONJ_THM`
`⊢ ∀P Q R. P ⇒ Q ∧ R ⇔ (P ⇒ Q) ∧ (P ⇒ R)`
• `DISJ_IMP_THM`
`⊢ ∀P Q R. P ∨ Q ⇒ R ⇔ (P ⇒ R) ∧ (Q ⇒ R)`
• `PULL_EXISTS`, `PULL_FORALL`

## Equalities

• Goals involving set equivalences may often be solved by

``fs[pred_setTheory.EXTENSION] >> metis_tac[]``

For example `∀s. s = EMPTY ⇔ ∀x. x IN s ⇒ F`.

• A goal `f a b c x d = f a b c y d` may be reduced to `x = y` with the tactic

``rpt (AP_TERM_TAC ORELSE AP_THM_TAC)``

This tactic might be too aggressive.

## Quantifiers

• `goal_assum \$ drule_at Any` (or earlier written: `goal_assum \$ first_assum o mp_then Any mp_tac`) is more flexible than `asm_exists_tac`, which is defined as

``first_assum \$ match_exists_tac o concl``

From the documentation:

The `goal_assum` selector is worth special mention since it’s especially useful with mp_then: it turns an existentially quantified goal `∃x. P x` into the assumption `∀x. P x⇒ F` thereby providing a theorem with antecedents to match on.

• Selective instantiation of a theorem with a universal prefix

``````fun CLOSED_INST theta th =
let val bvars = fst (strip_forall (concl th))
val domvars = map #redex theta
val bvars' = filter (not o C (op_mem aconv) domvars) bvars
in GENL bvars' (INST theta (SPEC_ALL th))
end``````

Example application to `⊢ ∀m n p. m + (n + p) = m + n + p`

``````CLOSED_INST [``p:num`` |-> ``0n``, ``m:num`` |-> ``1n``] arithmeticTheory.ADD_ASSOC;
(* ⊢ ∀n. 1 + (n + 0) = 1 + n + 0: thm *)``````
• Alternatively

``````fun subst_var v t thm =
let val (bv, rem) = dest_forall (concl thm);
in if (term_eq bv v) then SPEC t thm
else GEN bv (subst_var v t (SPEC bv thm))
end;
(* val it = ⊢ ∀n. 1 + n = n + 1: thm *)
(* val it = ⊢ ∀m. m + 1 = 1 + m: thm *)``````
• Use the contrapositive of a universal quantifier

``PRED_ASSUM is_forall (imp_res_tac o REWRITE_RULE[Once MONO_NOT_EQ])``
• Reorder the quantifiers of an existentially or universally quantified goal with `RESORT_EXISTS_CONV` or `RESORT_FORALL_CONV`, for example:

• `CONV_TAC \$ RESORT_EXISTS_CONV rev` to reverse the order
• `CONV_TAC \$ RESORT_EXISTS_CONV \$ Listsort.sort Term.compare` to sort alphabetically

The conversions `SWAP_EXISTS_CONV` and `SWAP_FORALL_CONV` might also come in handy to swap two quantifiers.

• Quantifiers may be partially instantiated.

• Existentially `Q.REFINE_EXISTS_TAC : term quotation -> tactic`
Apply `Q.REFINE_EXISTS_TAC `[_]`` to a goal `∃ls. ~NULL ls` which results in the new goal `∃_0. ~NULL [_0]`.

• Universally

``(fn tm => qspec_then tm (assume_tac o GEN_ALL)): term quotation -> thm -> tactic``

For example an assumption `∀x:'a list. A x` could be adjusted with

``first_x_assum (qspec_then `_::_::_` (assume_tac o GEN_ALL))``

rewriting it to `∀_2 _1 _0. A (_0::_1::_2)`.

• For instantiation of several existential quantifiers use `map_every qexists [`a`,`b`,`c`]`.

• For generalisation (e.g. prior an induction) use `map_every qid_spec_tac [`a`,`b`,`c`]` where `qid_spec_tac` is equivalent to `W(curry Q.SPEC_TAC)`.

• Rewriting within a quantifier

• Consider `irule_at Any EQ_REFL` to solve goals like `?x. f x = f y`.
• Or `irule_at (Pos hd) \$ DECIDE "p ==> p \/ q"`, which would rewrite a goal `?x. A \/ B` to `?x. A`.

## Boolean connectives

• Reduce a goal `A ∧ B ∧ X ⇔ A ∧ B ∧ Y` to `A ∧ B ⊢ X ⇔ Y` with the tactic

``rpt (match_mp_tac AND_CONG >> rw[])``
• If `A ⇒ B` is provable by `my_tac` and `B` is the goal, the tactic ``A` suffices_by my_tac` will make `A` the new goal.

• Prove the first conjunct and add it to the assumptions. Split `E ⊢ A ∧ B` into two goals `E ⊢ A` and `E,A ⊢ B` with `conj_asm1_tac`.

• Get a specific conjunct of the conclusion of a theorem, i.e.  for `my_thm = ∀x y z. A ⇒ B ∧ C ∧ D`:
`cj 1 my_thm` gives `∀x y z. A ⇒ B`. Or one can do the same by hand with

``CONJUNCTS \$ Ho_Rewrite.REWRITE_RULE[IMP_CONJ_THM,FORALL_AND_THM] my_thm``

gives a list of the implications `∀x y z. A ⇒ B`, `∀x y z. A ⇒ C` and `∀x y z. A ⇒ D`.

# Tactics on assumptions

• Remove all assumptions that mention a specific constant
• One possibility

``````rpt (PRED_ASSUM (exists (curry op = "the")
o map (fst o dest_const) o find_terms is_const) kall_tac)``````
• With a pre-defined function `has_const` and `WEAKEN_TAC`:

``````fun has_const t = Lib.can (find_term (same_const t))
e (rpt (WEAKEN_TAC (has_const ``the``)));``````
• Stow away a troublesome assumption (which for example should not be used in rewrites)
• Apply some tactic `my_tac` in absence of the troublesome pattern

``qpat_x_assum `troublesome pattern` (fn x => my_tac >> assume_tac x)``
• Hide the troublesome pattern in an abbreviation (does not necessarily work with recent versions of HOL)

``````qpat_x_assum `troublesome pattern` (assume_tac o ONCE_REWRITE_RULE[GSYM markerTheory.Abbrev_def])
>> my_tac
>> fs[markerTheory.Abbrev_def]``````

# Cases

• Prove a statement for finitely many cases

``````fun goal_term (f: term -> tactic) (s,g) = f g (s,g);
Triviality test:
∀ s . s < 31 ⇒ ((1w : 32 word) << s ≠ 0w)
Proof
rpt (goal_term (fn tm => Cases_on '^(find_term is_var tm)') \\ fs [])
QED``````

Or consider

``````(REWRITE_CONV [GSYM rich_listTheory.COUNT_LIST_COUNT,
GSYM pred_setTheory.IN_COUNT]
THENC EVAL) ``n < (31 : num)``;``````
• If the goal has the shape `if foo then ... else ...` where `foo` is nasty but one can prove `foo` easily. One could reduce cases by…

• `qmatch_abbrev_tac `COND foo` >> `foo` by my_tac`
• `reverse IF_CASES_TAC >- my_tac`
• One may reuse same case definition with views:

``````case view foo of
| Onething => onething
| _ => anotherthing
where view x =
case x of NONE => Onething
| SOME (_, []) => Onething
| _ => Other``````

# Taming `hol`

• For faster processing of proofs one can temporarily set

``Tactical.set_prover (fn (goal, _) => mk_thm ([], goal));``

to prove any theorem without checking (thus also `T = F`). Restore afterwards with `Tactical.restore_prover();`

• Run HOL4 and vim wrapped in tmux, or use the backwards compatible `vimhol.sh` script

• Highlighting issues may occur for `hol` running in a tmux session. Check if the ANSI escape codes (colours) are printed correctly with

``PP.pp_to_string 70 Parse.pp_term ``p /\ q``;``

Otherwise within the hol session (or `.hol-session.sml`) set

``Parse.current_backend := PPBackEnd.vt100_terminal``