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

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

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

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

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

.