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.

Boolean expressions

• 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

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, 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 termf 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_ALL
    end;
  qeval_ctxt [`g = λx. x + 2n`,`f = λx. x + 1n`]
    `(f:num -> num) o g $ 1n + 2`

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

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

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.

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

Numbers

• Definitions formulated in terms of SUC can not be used for evaluation with EVAL. For example

  EVAL ``x pow 3``

  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;
  EVAL ``x pow 3``
  (*  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:

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

Records

• 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

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

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

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

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

• 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

  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

• 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].