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.

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

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.

`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

Credits Konrad Slind:

`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; 1:num`` ADD_COMM; subst_var ``m:num`` ``(* val it = ⊢ ∀n. 1 + n = n + 1: thm *) 1:num`` ADD_COMM; subst_var ``n:num`` ``(* 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`

.

- Consider

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`

.

- Remove all assumptions that mention a specific constant
One possibility

`op = "the") rpt (PRED_ASSUM (exists (curry 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`fn x => my_tac >> assume_tac x) qpat_x_assum `troublesome pattern` (`

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

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`

`hol`

For faster processing of proofs one can temporarily set

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

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`

scriptHighlighting issues may occur for

`hol`

running in a tmux session. Check if the ANSI escape codes (colours) are printed correctly with`70 Parse.pp_term ``p /\ q``; PP.pp_to_string`

Otherwise within the hol session (or

`.hol-session.sml`

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