Commit 5b9628df authored by Heiko Becker's avatar Heiko Becker
Browse files

Remove dependency to Tactician

parent 75e8cdab
This diff is collapsed.
================================================================================
== HOL LIGHT TACTICIAN ==
== ==
== by Mark Adams ==
== Copyright (c) Univeristy of Edinburgh, 2012 ==
== Copyright (c) Proof Technologies Ltd, 2012-2015 ==
================================================================================
This is HOL Light Tactician, version 3.1.
All files are distributed under the terms of the GNU General Public License:
they are free and open source and come with no warranty. See the LICENSE file
for details.
Subsequent sections in this README deal with:
1. Directory Contents
2. Overview of Tactician
3. Installation / Loading
4. Using Tactician
5. Examples
6. Author and Acknowledgements
7. Website and Contact Details
* * * * * * *
1. DIRECTORY CONTENTS
The Tactician directory consists of the following files:
LICENSE Disclaimer and terms of the open source licence.
README This file.
USER_GUIDE Guide to using Tactician, including all of its commands.
*.ml ML source code implementing Tactician.
*.mli ML source code implementing Tactician.
and the following directory:
env Adjusted model of OCaml environment for various OCaml versions.
toploops Adjusted OCaml file 'toploop.ml' for various OCaml versions.
* * * * * * *
2. OVERVIEW OF TACTICIAN
Tactician is a utility for refactoring and visualising HOL Light tactic proofs.
It is aimed at HOL Light users of the subgoal package, both for novices wanting
to learn from legacy tactic proofs by stepping through them, and for experts
wanting reduce the effort involved in maintaining their own proof scripts.
Tactician works by dynamically recording tactic proofs as they are executed,
storing them internally as proof trees. The proof tree can then be exported
either as ML source code or as a .dot graph. Export to source code can
optionally involve refactoring the proof into various forms, including:
- flattened out into individual 'e' commands;
- packaged up with 'THEN's and 'THENL's into a single tactic proof.
Tactician works for virtually all the packaged up tactic proofs that occur in
the HOL Light source code. However there are theoretical limitations on what
it will work for. See USER_GUIDE for details.
* * * * * * *
3. INSTALLATION / LOADING
1. Download the source tarball (which includes this README) from the Proof
Technologies Tactician webpage:
http://www.proof-technologies.com/tactician
Change directory to your HOL Light distribution directory and unpack the
Tactician tarball as a subdirectory (called 'Tactician'):
> cd <hollight-dir>
> tar -xzf <download-dir>/hollight_tactician-<version>.tar.gz
2. This step is optional. It makes using Tactician easier, saving you from
having to execute "promote_all_values ();;" before each tactic proof you want
to refactor. However it involves rebuilding OCaml from source, which you
might not want to do.
Firstly, make sure you have a source distribution of OCaml. If you don't,
this can be obtained from the INRIA OCaml webpages at:
http://caml.inria.fr/ocaml/index.en.html
Secondly, overwrite the file 'toplevel/toploop.ml' in OCaml's source
distribution with the relevant file from Tactician's 'toploops' directory
(where "x" is the OCaml version):
> cd <ocaml-x-dir>
> mv toplevel/toploop.ml toplevel/toploop.ml.orig
> cp <hollight-dir>/Tactician/toploops/toploop.<x>.ml toplevel/toploop.ml
Thirdly, rebuild OCaml from source in the normal way:
> ./configure (with any options you want, e.g. --prefix `pwd`)
> make world.opt
> make install (may need to be done as sudoer or root)
> make clean
You should ensure that HOL Light works with your adjusted OCaml. If you are
using the same OCaml version with executables installed in the same directory,
and if you rebuild HOL Light from source each time you use HOL Light (as
opposed to using checkpointing), then there is nothing to do. Otherwise you
will need to ensure that the OCaml executables are in your execution path,
that the correct version of Camlp5 has been installed and/or that HOL Light
has been rebuilt accordingly. See the HOL Light README for details.
3. Start a HOL Light session as you normally do, and incorporate any extra
supporting files that get used in the proofs you want to refactor. For
example, to rebuild HOL Light from source, start an OCaml session in your HOL
Light distribution directory, and then execute the following:
# #use "hol.ml";; (the first '#' indicates the OCaml prompt)
# #use ... (for any subsequent supporting files)
4. Then load Tactician into the HOL Light session by processing the 'main.ml'
file from the 'Tactician' subdirectory:
# #use "Tactician/main.ml";;
* * * * * * *
4. USING TACTICIAN
A brief overview of some commands for basic refactoring of the most recently
processed tactic proof is given here. For full details about all of Tactician's
capabilities, see USER_GUIDE.
1. If a bespoke OCaml toplevel for Tactician (see installation step 2) is *not*
being used, then before executing each tactic proof, it is first necessary to
execute the following command:
# promote_all_values ();;
2. Then process the tactic proof from the proof script, as per normal:
# g `...`;;
# e (...);;
# e (...);;
OR
# prove (`...`,
... THEN ... THENL [...]);;
OR
# prove_by_refinement (`...`,
[ ... ; ... ; ...] );;
3. You can then use the ML output commands to output the proof to screen or
file in the desired form. The most commonly used commands for outputting to
screen are as follows:
# print_ge_proof ();;
- Prints the proof as a flattened series of "g/e" style single-tactic
steps, with no connecting top-level 'THEN' tacticals. Branch-
numbering comments are inserted wherever the proof branches.
# print_pbr_proof ();;
- Like 'print_ge_proof' but outputs in Flyspeck's "prove-by-
refinement" style instead of "g/e" style.
# print_thenl_prove_proof ();;
- Prints the proof as a single-step "prove" style proof, with
tactics that result in single goals connected by 'THEN' and those
that result in multiple goals connected by 'THENL'. This structure
directly reflects the tree structure of the proof as it was executed.
# print_prove_proof ();;
- Like 'print_thenl_prove_proof', but tries to print a more concise
proof, not necessarily reflecting the original tree structure.
This is done by spotting opportunities for replacing 'THENL' with
'THEN'.
# print_original_proof ();;
- Tries to reproduce the inputted proof verbatim, with the same
structure and style as the original.
* * * * * * *
5. EXAMPLES
Here we provide two examples of Tactician in use. For more examples, visit the
Tactician webpages (see Section 7 of this README).
PROOF FLATTENING
First an example of the proof flattening export facility, flattening the
packaged-up "prove" style proof of 'REAL_MUL_LINV_UNIQ' (from HOL Light source
code file 'real.ml') into a "g/e" style proof.
Steping through the following packaged-up proof of 'REAL_MUL_LINV_UNIQ' without
the aid of Tactician can be done by laboriously replacing "... THEN" around each
tactic with "e (...);;" to be ready for HOL Light input. However, usage of
'THEN' in the packaged-up proof obscures where the proof branches are and how
long those branches are, and so it is not obvious which tactics need to be
re-entered and at which point. Thus the user would also have to keep track of
the proof branching points.
# let REAL_MUL_LINV_UNIQ = prove
(`!x y. (x * y = &1) ==> (inv(y) = x)`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `y = &0` THEN
ASM_REWRITE_TAC[REAL_MUL_RZERO; REAL_OF_NUM_EQ; ARITH_EQ] THEN
FIRST_ASSUM(SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV) THEN
ASM_REWRITE_TAC[REAL_EQ_MUL_RCANCEL] THEN
DISCH_THEN(ACCEPT_TAC o SYM));;
Once the above proof has been entered, Tactician flattens it out with a single
command:
# print_ge_proof ();;
This outputs the proof in a form ready to be stepped through by the user:
g `!x y. (x * y = &1) ==> (inv(y) = x)`;;
e (REPEAT GEN_TAC);;
e (ASM_CASES_TAC `y = &0`);;
(* *** Branch 1 *** *)
e (ASM_REWRITE_TAC [REAL_MUL_RZERO;REAL_OF_NUM_EQ;ARITH_EQ]);;
(* *** Branch 2 *** *)
e (ASM_REWRITE_TAC [REAL_MUL_RZERO;REAL_OF_NUM_EQ;ARITH_EQ]);;
e (FIRST_ASSUM (SUBST1_TAC o SYM o MATCH_MP REAL_MUL_LINV));;
e (ASM_REWRITE_TAC [REAL_EQ_MUL_RCANCEL]);;
e (DISCH_THEN (ACCEPT_TAC o SYM));;
The flattened proof reveals that 'ASM_CASES_TAC' causes the proof to branch into
two, and that the first 'ASM_REWRITE_TAC' gets applied to each resulting
subgoal, finishing off the first.
PROOF PACKAGING
Now an example of the proof packaging facility, packaging up a flat "g/e" style
proof into a "prove" style proof. This "g/e" style proof is a flattened version
of the proof of 'REAL_LE_LCANCEL_IMP' (from HOL Light source code file
'real.ml').
Without the aid of Tactician, packaging up the following proof not only invovles
replacing "e(...)" lines with "... THEN", but also keeping track of branching
points, by stepping through the proof, and putting the branches into a 'THENL'
list. To produce a concise version, it is then necessary to review the
resulting proof to find where branches have common proofs, and thus where
duplicated 'THENL' list elements can be removed. Finally, it is nice to
reformat the resulting optimised proof so that it occupies fewer lines but still
remains readable.
# g `!x y z. &0 < x /\ x * y <= x * z ==> y <= z`;;
# e (REPEAT GEN_TAC);;
# e (REWRITE_TAC [REAL_LE_LT; REAL_EQ_MUL_LCANCEL]);;
# e (ASM_CASES_TAC `x = &0`);;
# e (ASM_REWRITE_TAC [REAL_LT_REFL]);;
# e (ASM_REWRITE_TAC [REAL_LT_REFL]);;
# e (STRIP_TAC);;
# e (ASM_REWRITE_TAC []);;
# e (DISJ1_TAC);;
# e (MATCH_MP_TAC REAL_LT_LCANCEL_IMP);;
# e (EXISTS_TAC `x:real`);;
# e (ASM_REWRITE_TAC []);;
# e (ASM_REWRITE_TAC []);;
The proof actually branches at two points: firstly after 'ASM_CASES_TAC' on line
4 of the proof; secondly in the second branch after 'STRIP_TAC' on line 7. The
first branch from 'ASM_CASES_TAC' is finished in a single step, which is also
the first step of the second branch, and so there is no need for a 'THENL' list
for this branching point. Also, the second branch from 'STRIP_TAC' is finished
in a single step, which is also the first step of the first branch, and so
neither does this branching point require a 'THENL' list.
Tactician packages up the above proof, finds where 'THENL' lists can be
optimised and reformats the result, all in a single command:
# print_prove_proof ();;
prove
(`!x y z. &0 < x /\ x * y <= x * z ==> y <= z`,
REPEAT GEN_TAC THEN REWRITE_TAC [REAL_LE_LT; REAL_EQ_MUL_LCANCEL] THEN
ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC [REAL_LT_REFL] THEN
STRIP_TAC THEN ASM_REWRITE_TAC [] THEN DISJ1_TAC THEN
MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `x:real` THEN
ASM_REWRITE_TAC []);;
* * * * * * *
6. AUTHOR AND ACKNOWLEDGEMENTS
Tactician is written by Mark Adams, Proof Technologies Ltd. The original
version was written whilst working for David Aspinall at the Department of
Informatics, University of Edinburgh, and was funded by the University of
Edinburgh. Some of the subsequent work has been written whilst working for
Josef Urban at Radboud University, funded by Tom Hales and Radboud University.
* * * * * * *
7. WEBSITE AND CONTACT DETAILS
The Proof Technologies website has pages dedicated to Tactician, including the
download for the latest version, at:
http://www.proof-technologies.com/tactician
Users are encouraged to contact Proof Technologies with any problems found in
Tactician, or with any suggestions for improvements.
You can contact us via the website Tactician pages. Alternatively, you can
e-mail us:
tactician@proof-technologies.com
This diff is collapsed.
This diff is collapsed.
(* ========================================================================== *)
(* BIOLAYOUT EXPORT (HOL Light Tactician) *)
(* - Support for BioLayout graph display of recorded tactics *)
(* *)
(* by Mark Adams *)
(* Copyright (c) University of Edinburgh, 2012 *)
(* Copyright (c) Proof Technologies Ltd, 2012-2013 *)
(* ========================================================================== *)
(* biolayout_nodename *)
let biolayout_nodename n =
"Node" ^ string_of_int n;;
(* Biolayout graph printer *)
let pp_goaltree_biolayout_graph gtr =
let nns = goaltree_graph gtr in
let pp_line (n1,n2) =
(pp_string (biolayout_nodename n1);
pp_string "\t";
pp_string (biolayout_nodename n2);
pp_string "\n") in
(do_list pp_line nns);;
(* File export utility *)
let export_to_biolayoutfile name pp_fn info =
let path = !ttn_export_dir in
let suffix = ".layout" in
export_to_file (path,name,suffix) pp_fn info;;
(* ** USER-LEVEL COMMANDS ** *)
(* Printers *)
let print_biolayout_graph () =
print_to_screen pp_goaltree_biolayout_graph (latest_goaltree ());;
let print_biolayout_graph_of name =
print_to_screen pp_goaltree_biolayout_graph (get_named_goaltree name);;
(* Exporters *)
let export_biolayout_graph () =
export_to_biolayoutfile "proof" pp_goaltree_biolayout_graph
(latest_goaltree ());;
let export_biolayout_graph_of name =
export_to_biolayoutfile name pp_goaltree_biolayout_graph
(get_named_goaltree name);;
(* ========================================================================== *)
(* COMMAND PROMOTION (HOL Light Tactician) *)
(* - Promotion of HOL Light command bindings *)
(* *)
(* by Mark Adams *)
(* Copyright (c) University of Edinburgh, 2012 *)
(* Copyright (c) Proof Technologies Ltd, 2012-2013 *)
(* ========================================================================== *)
(* This file promotes the theorem- and tactic-related commands. This is *)
(* done by trivially overwriting the bindings with their already-defined *)
(* promoted variants. *)
(* Subgoal package commands *)
let set_goal (tms,tm) = xset_goal (tms,tm);;
let g tm = xg tm;;
let e = xe;;
let r = xr;;
let b = xb;;
let p = xp;;
let top_goal = xtop_goal;;
let top_thm = xtop_thm;;
let prove (tm,tac) = xprove (tm,tac);;
let prove_by_refinement (tm,tacs) = xprove_by_refinement (tm,tacs);;
(* Theorem destructors and equality *)
let concl = xconcl;;
let hyp = xhyp;;
let dest_thm = xdest_thm;;
let equals_thm = equals_xthm;;
let thm_frees = xthm_frees;;
(* Goal constructors and destructors *)
let mk_goal (xasl,w) : xgoal =
let asl = snd_map xthm_thm xasl in
new_xgoal (asl,w);;
let dest_goal gl = (xgoal_hyp gl, xgoal_concl gl);;
let goal_hyp = xgoal_hyp;;
let goal_concl = xgoal_concl;;
(* ========================================================================== *)
(* DETECTION FUNCTIONS (HOL Light Tactician) *)
(* - Functions for detecting the meta-arguments of meta-functions *)
(* *)
(* by Mark Adams *)
(* Copyright (c) University of Edinburgh, 2012 *)
(* Copyright (c) Proof Technologies Ltd, 2012-2013 *)
(* ========================================================================== *)
(* Detection functions are used in 'wrappers.ml' for the promotion of meta- *)
(* functions (i.e. functions that take a function as an argument, called a *)
(* "meta-argument"). They solve the problem of capturing what the meta- *)
(* argument is. Generic detection functions are defined in this file, and *)
(* are specialised in 'wrappers.ml'. *)
(* Our approach only applies to meta-arguments that are themselves *)
(* promotable, and is based on the assumption that a given meta-argument is *)
(* actually executed at some point in the execution of the meta-function. *)
(* Note that when the promoted form of the meta-function gets executed, it is *)
(* of course supplied with a meta-argument that is already in promoted form. *)
(* Thus the promotion of the meta-function must involve first demoting the *)
(* meta-argument, before applying the original unpromoted meta-function to *)
(* it to get the result and then incorporating this into the promoted result. *)
(* Our technique involves adapting the meta-argument during its demotion, so *)
(* that when it is executed, the meta-argument is captured and stored in a *)
(* temporary state variable. The information in this state variable is then *)
(* used in the promotion of the result. *)
(* ** FUNCTION DETECTION ** *)
(* As explained already, our technique involves demoting the supplied meta- *)
(* argument. When this demoted meta-argument is executed as part of the *)
(* execution of the supplied meta-function, it will get passed a demoted *)
(* argument, which must first be promoted before the original promoted meta- *)
(* argument can be applied to it. The creation of a promoted argument is *)
(* performed by a "prepare function", which returns a promoted argument and a *)
(* "seed". The result of applying the promoted meta-argument to the promoted *)
(* argument then needs to be demoted to be returned as the result of the *)
(* demoted meta-argument. The demotion of this result is performed by a *)
(* "destruct function", which takes the seed as an extra argument, allowing *)
(* the meta-argument to be captured and stored in the state variable. The *)
(* state variable holds a list of these captured meta-arguments, which are *)
(* unified after the execution of meta-function has completed, to give as *)
(* complete a picture as possible of the meta-argument. *)
(* Primitive detection functions *)
(* First we define primitive detection functions - one for each number of *)
(* meta-arguments to be detected: single, pair, triple and list. *)
let detect_1func_app ((null_margobj:mlobject),
(prepare:'a->'A*'x),(destruct:'x->'B->'b*mlobject))
(mfunc:('a->'b)->'c) (xmarg:'A->'B) : 'c*mlobject =
let temp = ref ([]:(mlobject)list) in
let marg (arg:'a) : 'b =
let (xarg,seed) = prepare arg in
let xres = xmarg xarg in
let (res,margobj) = destruct seed xres in
(temp := margobj::!temp;
res) in
let fullres = mfunc marg in
let margobj = if (is_empty !temp)
then null_margobj
else mlobject_list_unify !temp in
(fullres,margobj);;
let detect_2func_app
((null_margobj1:mlobject),
(prepare1:'a1->'A1*'x1),(destruct1:'x1->'B1->'b1*mlobject))
((null_margobj2:mlobject),
(prepare2:'a2->'A2*'x2),(destruct2:'x2->'B2->'b2*mlobject))
(mfunc:('a1->'b1)->('a2->'b2)->'c)
(xmarg1:'A1->'B1) (xmarg2:'A2->'B2) : ('c*(mlobject*mlobject)) =
let temp1 = ref ([]:(mlobject)list) in
let marg1 (arg:'a) : 'b1 =
let (xarg,seed) = prepare1 arg in
let xres = xmarg1 xarg in
let (res,funobj) = destruct1 seed xres in
(temp1 := funobj::!temp1;
res) in
let temp2 = ref ([]:(mlobject)list) in
let marg2 (arg:'a2) : 'b2 =
let (xarg,seed) = prepare2 arg in
let xres = xmarg2 xarg in
let (res,funobj) = destruct2 seed xres in
(temp2 := funobj::!temp2;
res) in
let fullres = mfunc marg1 marg2 in
let margobj1 = if (is_empty !temp1)
then null_margobj1
else mlobject_list_unify !temp1 in
let margobj2 = if (is_empty !temp2)
then null_margobj2
else mlobject_list_unify !temp2 in
(fullres,(margobj1,margobj2));;
let detect_3func_app
((null_margobj1:mlobject),
(prepare1:'a1->'A1*'x1),(destruct1:'x1->'B1->'b1*mlobject))
((null_margobj2:mlobject),
(prepare2:'a2->'A2*'x2),(destruct2:'x2->'B2->'b2*mlobject))
((null_margobj3:mlobject),
(prepare3:'a3->'A3*'x3),(destruct3:'x3->'B3->'b3*mlobject))
(mfunc:('a1->'b1)->('a2->'b2)->('a3->'b3)->'c)
(xmarg1:'A1->'B1) (xmarg2:'A2->'B2) (xmarg3:'A3->'B3)
: ('c*(mlobject*mlobject*mlobject)) =
let temp1 = ref ([]:(mlobject)list) in
let marg1 (arg:'a1) : 'b1 =
let (xarg,seed) = prepare1 arg in
let xres = xmarg1 xarg in
let (res,funobj) = destruct1 seed xres in
(temp1 := funobj::!temp1;
res) in
let temp2 = ref ([]:(mlobject)list) in
let marg2 (arg:'a2) : 'b2 =
let (xarg,seed) = prepare2 arg in
let xres = xmarg2 xarg in
let (res,funobj) = destruct2 seed xres in
(temp2 := funobj::!temp2;
res) in
let temp3 = ref ([]:(mlobject)list) in
let marg3 (arg:'a3) : 'b3 =
let (xarg,seed) = prepare3 arg in
let xres = xmarg3 xarg in
let (res,funobj) = destruct3 seed xres in
(temp3 := funobj::!temp3;
res) in
let fullres = mfunc marg1 marg2 marg3 in
let margobj1 = if (is_empty !temp1)
then null_margobj1
else mlobject_list_unify !temp1 in
let margobj2 = if (is_empty !temp2)
then null_margobj2
else mlobject_list_unify !temp2 in
let margobj3 = if (is_empty !temp3)
then null_margobj3
else mlobject_list_unify !temp3 in
(fullres,(margobj1,margobj2,margobj3));;
let detect_funclist_app ((null_margobj:mlobject),
(prepare:'a->'A*'x),(destruct:'x->'B->'b*mlobject))
(mfunc:('a->'b)list->'c) (xmargs:('A->'B)list)
: ('c*(mlobject)list) =
let n = length xmargs in
let temps = ref (copy n ([]:(mlobject)list)) in
let foo (xmarg,i) arg =
let (xarg,seed) = prepare arg in
let xres = xmarg xarg in
let (res,funobj) = destruct seed xres in
(temps := assign (i, funobj::(el (i-1) !temps)) !temps;
res) in
let margs = map foo (zip xmargs (1 -- n)) in
let fullres = mfunc margs in
let unifyfoo objs = if (is_empty objs)
then null_margobj
else mlobject_list_unify objs in
let margobjs = map unifyfoo !temps in
(fullres,margobjs);;
(* Derived detection functions *)
(* We can now define derived detection functions for meta-arguments that take *)
(* multiple arguments, by packaging up the multiple arguments into tuples. *)
let detect_1bfunc_app ((null_margobj:mlobject),
(prepare1:'a1->'A1*'x1),(prepare2:'a2->'A2*'x2),
(destruct:'x1*'x2->'B->'b*mlobject))
(bmfunc:('a1->'a2->'b)->'c) (xbmarg:'A1->'A2->'B) : 'c*mlobject =
let prepare (arg1,arg2) =
let (xarg1,seed1) = prepare1 arg1 in
let (xarg2,seed2) = prepare2 arg2 in
((xarg1,xarg2),(seed1,seed2)) in
let mfunc marg = bmfunc (curry marg) in
let xmarg = uncurry xbmarg in
detect_1func_app (null_margobj,prepare,destruct)
mfunc xmarg;;
let detect_2bfunc_app
((null_margobj1:mlobject),
(prepare11:'a11->'A11*'x11),(prepare12:'a12->'A12*'x12),
(destruct1:('x11*'x12)->'B1->'b1*mlobject))
((null_margobj2:mlobject),
(prepare21:'a21->'A21*'x21),(prepare22:'a22->'A22*'x22),
(destruct2:('x21*'x22)->'B2->'b2*mlobject))
(bmfunc:('a11->'a12->'b1)->('a21->'a22->'b2)->'c)
(xbmarg1:'A11->'A12->'B1) (xbmarg2:'A21->'A22->'B2)
: ('c*(mlobject*mlobject)) =
let prepare1 (arga,argb) =
let (xarga,seeda) = prepare11 arga in
let (xargb,seedb) = prepare12 argb in
((xarga,xargb),(seeda,seedb)) in
let prepare2 (arga,argb)