Tactician

Tactician

What is Tactician?

Tactician is a tool for helping you maintain and/or understand HOL Light proof scripts. Its main function is to refactor the ML of a tactic proof, typically to package up a "g/e" style proof into a "prove" style proof, or vice versa, to flatten out a "prove" style proof into a series of "g/e" style interactive steps. This can help experienced users maintain their proof scripts, and help novices learn from existing proof scripts.

Once loaded into a HOL Light session, it runs in the background, dynamically capturing tactic proofs as they are executed, and outputting upon user request. It is capable of refactoring tactic proofs written in the following styles:

See here for some simple examples of its refactoring capability.

See here for a paper describing some of the ideas behind Tactician's implementation.

Tactician also supports various other related activities, such as visualising the structure of a tactic proof, spotting slow tactic applications and duplicate theorems, and viewing the dependencies between theorems. These facilities are particularly useful when managing large proof projects.

Download and Installation

A source tarball for the latest version can be downloaded here: hollight_tactician-3.1.tgz (released 2015-01-10).

Unpack the downloaded tarball as a subdirectory of your existing HOL Light installation directory, by executing the following command from a terminal window, to result in a directory called Tactician:

tar -xzf hollight_tactician-3.0.tgz -C your-hollight-dir

Users are encouraged to rebuild OCaml specially for Tactician usage. Doing this avoids the need to execute promote_all_values before each proof you want to refactor (see below). See 'toploops/README' for full details on how to rebuild.

Tactician can be loaded into an existing HOL Light session in about 5 to 30 seconds (depending on your system hardware and how many theorems have already been proved in the session) by executing the following ML directive in the HOL Light session (where the first # indicates the OCaml prompt):

# #use "Tactician/main.ml";;

Tactician is then ready to record and refactor proofs in terms of the ML bindings referred to in the original proof script.

Usage

The main refactoring operations supported are packaging up a series of tactic steps into a single compound tactic joined by THEN and THENL tacticals, and the reverse operation, for flattening out a packaged-up proof into a series of atomic tactic steps. Note that such operations are not just trivial syntactic transformations of the proof script, because the RHS tactic of a THEN tactical application can get applied to more than one subgoal.

Unless you have rebuilt OCaml with an adjusted toploop (see above), then before refactoring a given tactic proof, you first need to update the ML theorem bindings recognised by Tactician by executing the following command in the HOL Light session (where the # indicates the OCaml prompt):

# promote_all_values ();;

Then execute the tactic proof as normal.

To output a flattened version of the proof in the "g and e" style, enter the following:

# print_ge_proof ();;

To output a flattened version of the proof in the Flyspeck project's "prove-by-refinement" style, enter the following:

# print_pbr_proof ();;

To output the proof as a single packaged-up tactic in the "prove" style, enter the following:

# print_prove_proof ();;

See here for some examples of Tactician in action.