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. See also to the HOL4 cheatsheet.

- The simpset fragments
`DNF_ss`

and`CONJ_ss`

can simplify some boolean expressions. These are the underlying simpset fragments of the tactics`dsimp[]`

and`csimp[]`

, respectively. - Otherwise useful theorems (e.g. for use with
`Ho_Rewrite.REWRITE_RULE`

and possibly`GSYM`

) are:`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`

`AND_IMP_INTRO`

`∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3`

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, otherwise have a look at

`MK_COMB_TAC`

.`computeLib.EVAL`

calculates a term and generates a theorem, that the term equals its reduction. Now we discuss evaluation with preconditions, that is given a property`P x`

evaluate the term`f x`

. This only makes sense if the term`f x`

branches on a property of`x`

. With`y`

as the result of the evaluation we want to produce the theorem:`P x ⇒ f x = y`

The example with two preconditions

`⊢ ∀g f. g = (λx. x + 2) ⇒ f = (λx. x + 1) ⇒ (f ∘ g) (1 + 2) = 6`

is obtained by the following code.

`fun qeval_ctxt ctxt tm = let val assl = List.map (ASSUME o Term) ctxt; in EVAL $ Term tm |> PROVE_HYP (LIST_CONJ assl) |> CONV_RULE $ RAND_CONV (REWRITE_CONV assl THENC EVAL) |> DISCH_ALL |> GEN_ALLend; qeval_ctxt [`g = λx. x + 2n`,`f = λx. x + 1n`]2` `(f:num -> num) o g $ 1n +`

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

`qrefine : term quotation -> tactic`

(also called`Q.REFINE_EXISTS_TAC`

) Apply`qrefine `[_]``

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`

.There are various tactics to transform a goal

`p ==> q`

to its contrapositive`~q ==> ~p`

:`CONV_TAC $ REWR_CONV $ GSYM CONTRAPOS_THM simp[Once $ GSYM CONTRAPOS_THM] ONCE_REWRITE_TAC [GSYM CONTRAPOS_THM] MATCH_MP_TAC $ iffLR CONTRAPOS_THM CCONTR_TAC`

A theorems (or goal) of the shape (in disjunctive normal form)

`(x = 2 ∧ f x) ∨ (f x ∧ x = 3) ∨ (g 3 = x ∧ f x)`

can be further simplified by rewriting

`f x`

by`x = y`

(or`y = x`

) into`f y`

. The theorem`EQ_SYM_EQ`

(`⊢ ∀x y. x = y ⇔ y = x)`

is handy here in the transformation (or tactic with`SIMP_TAC`

):`SIMP_RULE (bool_ss ++ boolSimps.CONJ_ss) [EQ_SYM_EQ]`

The simplifier prevents infinite applications of

`EQ_SYM_EQ`

. The result of the transformation is:`(x = 2 ∧ f 2) ∨ (f 3 ∧ x = 3) ∨ (x = g 3 ∧ f (g 3))`

Subsequently, certain values of

`f y`

could be further rewritten, maybe even to false`F`

decreasing the number of disjunctions.

Definitions formulated in terms of

`SUC`

can not be used for evaluation with`EVAL`

. For example`3`` EVAL ``x pow`

returns

`⊢ x pow 3 = x pow 3`

. Only after rewriting the definition with`numLib.SUC_TO_NUMERAL_DEFN_CONV`

the evaluation succeeds:`val _ = computeLib.add_thms [CONV_RULE numLib.SUC_TO_NUMERAL_DEFN_CONV realTheory.pow] computeLib.the_compset; 3`` EVAL ``x pow (* val it = ⊢ x pow 3 = x * (x * (x * 1)): thm *)`

The automatic simplification of

`SUC 0`

to`1`

(by a`reduceLib`

conversion) can be a problem. To exclude this rewrite, exclude its full name that is given to the conversion inside the simpset (built inside`numSimps`

), like:`"REDUCE_CONV (arithmetic reduction)"] ``SUC 0`` SIMP_CONV (srw_ss()) [Excl`

Theorems for rewriting records

In the HOL4 and CakeML sources the most commonly used record theorems for rewriting are`<type>_component_equality`

and`<type>_11`

. For the record type`float`

these theorems are:`binary_ieeeTheory.float_component_equality(* ⊢ ∀(f1 :(τ, χ) float) f2. f1 = f2 ⇔ f1.Sign = f2.Sign ∧ f1.Exponent = f2.Exponent ∧ f1.Significand = f2.Significand : thm *) binary_ieeeTheory.float_11(* ⊢ ∀(sign :word1) (exp :χ word) (significand :τ word) sign' exp' significand'. float sign exp significand = float sign' exp' significand' ⇔ sign = sign' ∧ exp = exp' ∧ significand = significand': thm *)`

Constructing record terms

Record types, like rings, semi-rings or floating-point numbers, are registered in the`TypeBase`

structure. A term of record type can be constructed with`TypeBase.mk_record`

, for example:`open binary_ieeeTheory val tm = TypeBase.mk_record (``:('a, 'b) float``,[("Sign",``0w:word1``)]) (* produces: val tm = “<|Sign := 0w|>”: term *)`

Each record field, like the

`Sign`

field, has a dedicated accessor function, here`float_Sign`

, that is not visible to the user (and should probably not be used as such). To obtain the term of the record field, one can apply the accessor function from`TypeBase.fields_of`

to the record. For example:`(* val lookup : 'a -> ('a * 'b) list -> 'b option *) val lookup = fn key => Option.map snd o List.find (curry op = key o fst) (* val acc_fn : string -> hol_type -> term option *) val acc_fn = fn acc => Option.map #accessor o lookup acc o TypeBase.fields_of`

The accessor function of the field

`Sign`

for the record type`float`

is`"Sign" $ type_of tm acc_fn (* produces: SOME (“float_Sign”): term option *) "Sign" $ type_of tm Option.map type_of $ acc_fn (* produces: SOME (“:(τ, χ) float -> word1”): hol_type option *)`

As a trivial example, the term that gets the value of the accessor

`Sign`

is`"Sign" $ type_of tm, tm) EVAL $ mk_icomb (acc_fn (* produces: ⊢ <|Sign := 0w|>.Sign = 0w *)`

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

One can put all goals matching a pattern to the bottom of the list of goals with

`proofManagerLib.expand_list (Q.SELECT_GOAL_LT [`pat1`, `pat2`])`

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`

Different behaviour when running

`hol`

(i.e. interactive use) when running`Holmake`

is probably due to different load order. Difference in load order may strings parse to terms. To inspect the load order supply the`--dbg`

flag to`Holmake`

, and interrupt when diverging. The load order can be inspected from the respective`*Script.uo`

file.To check whether a simpset conversion has the proper shape, use

`SCONV[]`

on a term that should be rewritten. Theorem can be added to the simpset for example with`[simp]`

.