HOL4 tactic cheatsheet ====================== *Rewriting* -- The nicest HOL proofs are ones where rewriting does most of the job. The most frequently used tactics are: simp [thms] -- simplifies goal using assumptions, stateful simpset and decision procedures for natural numbers fs [thms] -- similar to simp but also simplifies assumptions from bottom upwards (newer assumptions rewrite old ones) rfs [thms] -- is the same as fs but applies to assumptions in reverse order i.e. from top downwards rw [thms] -- similar to simp, but this does more in that it deconstructs the goal, e.g. it tries to split the goal into several subgoals If those above are doing too much, then try: pure_rewrite_tac [thms] -- this just applies the given theorems as rewrite rules (no smarts with arithmetic etc) rewrite_tac [thms] -- almost the same as above, except this will also do basic simplification of boolean expressions asm_rewrite_tac [thms] -- same as above but uses assumptions of the current goal as rewrites in addition to given theorems once_rewrite_tac [thms] and once_asm_rewrite_tac [thms] -- perform a top-down descent and perform at most one rewrite per subtree If these are still too blunt, then one can resort to the equivalent of "assembly programming" for rewriting: CONV_TAC conversion -- applies the given conversion to the current goal; a conversion is a function of type term -> thm such that given a term t it produces a theorem |- t = t', for some reformulation t'; there are many conversion combinators, e.g. RAND_CONV, RATOR_CONV, THENC, and some for rewriting, e.g. REWRITE_CONV [thms]. *Provers* -- If you are lucky a decision procedure can prove your goal. decide_tac -- proves linear arithmetic over the natural numbers (type: num) intLib.COOPER_TAC -- proves similar goals for intergers (type: int) metis_tac [thms] -- attempts to find a solution using a first-order logic prover using the given theorems, thms blastLib.BBLAST_TAC -- bit-blasting (i.e. SAT) for goals about only words (wordsTheory), note: all types must be concrete, e.g. word32 instead of 'a word *Induction* -- Many proofs start by applying an induction theorem. Induct_on `term` -- starts an induction theorem based on the type of the given term, e.g. Induct_on `n` in a goal `∀k n:num. n ≤ k + n` will produce two subgoals one for the base case 0 and one for the step case. Induct -- does the same but uses the first variable in a ∀-quantified goal for the induction. An application of Induct to the example goal above would produce an induction on k. completeInduct_on `term` -- starts a strong (or complete) induction on the natural numbers, i.e. only one subgoal but one gets to assume the goal for all instances strictly less than the goal instance. recInduct ind_thm and ho_match_mp_tac ind_thm -- starts an induction based on an induction theorem, i.e. a theorem one gets from the definition of a recursive function or an inductive relation *Case splits* -- Tactics for performing case splits. Cases_on `term` -- performs a case split on the given term Cases -- performs a case split on the first ∀-quantified variable in the goal; requires goal to have top-level ∀-quantifier PairCases_on `p` -- given a variable p of a pair type, this tactic instantiates p with (p1,p2,...,pn) if p is an n-tuple. (This usually provides better names than repeated applications of Cases_on) CASE_TAC -- looks for case statements in the goal and performs a case split on the smallest case expression TOP_CASE_TAC -- performs a case split on the top-most case expression every_case_tac -- performs a case split on every case expression; this is handy but can be slow and can cause an explosion of cases. *Subgoals and tactic combinators* -- The following will help you organise proofs with subgoals. \\ and THEN and >> -- are names for THEN, which is used to compose two tactics and make one, e.g. tac1 // tac2 runs tac1 and then tac2; if tac1 produces several subgoals then tac2 is run on all new subgoals THEN1 and >- -- both mean the same, tac1 THEN1 tac2 applies tac2 to the first subgoal and fails if tac2 fails to finish the proof of the first subgoal sg `goal` -- starts a new subgoal and inserts goal as an assumption in the goal that existed before calling sg `goal` by tactic -- this starts a new subgoal and proves it immediately with the tactic provided; it fails if the tactic fails to prove the local goal rpt tactic -- repeats the given tactic until it fails TRY tactic -- apply the given tactic once; in case the tactic fails, then rewind the goal *Goal deconstruction* -- Longer and more delicate proofs require manually stating how the goal is to be taken apart. rpt strip_tac -- repeats strip_tac, which attempts to split a top-level conjunct into two subgoals, move an implication into the assumptions or remove a top-level ∀-quantified variable. conj_tac -- splits a top-level conjunction into two subgoals impl_tac -- given a goal of the form `(A ==> B) ==> C`, impl_tac produces two subgoals: `A` and `B ==> C`; this is often handy in combination with drule, see below qexists_tac `term` -- instantiates a top-level existential quantifier with the given term asm_exists_tac -- if the goal has the form `∃vars. P vars /\ Q ...` then asm_exists_tac tries to find a match for `P vars` in the assumptions, if it finds a match it then instantiates vars and removes `P vars` from the goal *Instantiations* -- Occasionally, inductive hypothesis or lemmas need to be manually instantiated. The following are the most common ways of instantion: drule thm -- if thm has the form `∀vars. P /\ Q /\ ... ==> ..` then drule thm will look through the assumptions (bottom up) in search for one that matches P. If a match is found, then drule instantiates vars so that P can be discharged, the result is added as an implication to the current goal disch_then drule -- is a nice continuation of drule from above, disch_then picks `A` from the goal if it has the shape `A ==> B`; in the example above, disch_then drule will attempt to find a match for Q and instantiate the remaining vars accordingly, again leaving the result as an implication on the current goal pop_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac) first_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac) first_x_assum (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac) qpat_assum `pat` (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac) qpat_x_assum `pat` (qspecl_then [`t1`,`t2`,...,`tn`] mp_tac) -- these pick an assumption from the assumptions list and instantiate its ∀-quantified variables with the terms `t1`, `t2` etc. the resulting term is added as a new implication onto the current goal, due to mp_tac; alternatively, one can use assume_tac or strip_assume_tac to instead introduce the new term as a new assumption. Difference between all of these is in how they pick the assumption to instantiate: - pop_assum: always picks the last assumption, and removes it - first_assum: picks the first for which qspecl_then succeeds - first_x_assum: same as above but also removes the assumption - qpat_assum: picks an assumption that matches the pattern pat - qpat_x_assum: same as above but also removes the assumption Note: it is common to use qspecl_then .. for pop_assum, first_assum etc. However, any ML function of type thm -> tactic will suffice, e.g. it can be handy to write first_x_assum drule. imp_res_tac thm -- tries to add all immediate consequences of the given theorem, thm, to the assumptions of the current goal; the thm needs to be an implication; warning: imp_res_tac can cause an explosion in the number of assumptions res_tac -- is similar to imp_res_tac but takes no argument, instead res_tac attempts to find all consequences of combining all of the assumptions via modus ponens; res_tac should be used carefully to make sure the assumptions list does not get too long or full of junk *Renaming and abbreviating* -- HOL4 sometimes generates names, e.g. q' or r''', and large expression. These can be annoying and can lead to brittle proofs. rename1 `pat` -- will look to match pat with something in the goal, assumptions or some part of them; it renames all variables to match those given in the pattern, e.g. rename1 `n + _ <= _` turns an assumption `q'' + k <= 4` into `n + k <= 4`, if the goal did not have something that matched `n + _ <= _` qmatch_asmsub_rename_tac `pat` -- is more specific than rename1: it looks for some match in an assumption and ignores the goal qmatch_goalsub_rename_tac `pat` -- same as above but for the goal only, ignores assumptions qabbrev_tac `foo = large-term-here` -- replaces a large term with a given name, e.g. foo qpat_abbrev_tac `foo = pat` -- same as above but tries to find the exact term from the goal, e.g. if pat is `_ + _` then foo might abbreviate `n+4`