This page gives some examples of Tactician in use. Note that these examples are to be run in a HOL Light session that has Tactician already loaded.
First we illustrate how a single-tactic, packaged-up proof that branches into multiple subgoals can be flattened out into a series of "g and e" style interactive tactic steps.
Enter the following tactic proof into the HOL Light session (the
# indicates the OCaml prompt, which should not itself be
entered):
# prove (`(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`,
REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
To output a flattened version of this proof, with comments pointing out each branching point, enter the following:
# print_ge_proof ();;
This results in the following being outputted to screen:
g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
e (REPEAT CONJ_TAC);;
(* *** Branch 1 *** *)
e (GEN_TAC);;
e (REFL_TAC);;
(* *** Branch 2 *** *)
e (GEN_TAC);;
e (REFL_TAC);;
(* *** Branch 3 *** *)
e (GEN_TAC);;
e (REFL_TAC);;
Next we illustrate outputting an incomplete "g and e" style proof and packaging up a completed proof into a "prove" style proof.
Enter the following incomplete proof into the HOL Light session:
# g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
# e (REPEAT CONJ_TAC);;
# e (GEN_TAC);;
# r 1;;
# e (GEN_TAC);;
# e (REFL_TAC);;
To output a summary of the current proof, enter the following:
# print_executed_ge_proof ();;
This results in the following being outputted to screen, where elipsis indicates an incomplete subgoal:
g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
e (REPEAT CONJ_TAC);;
(* *** Branch 1 *** *)
e (GEN_TAC);;
e (...);;
(* *** Branch 2 *** *)
e (GEN_TAC);;
e (REFL_TAC);;
(* *** Branch 3 *** *)
e (...);;
Now complete the proof by filling out the remaining steps, starting where the proof was left off, at Branch 3. Enter the following:
# e (GEN_TAC);;
# e (REFL_TAC);;
# e (REFL_TAC);;
To output a packaged-up version of the completed proof as a single tactic, enter the following:
# print_prove_proof ();;
This results in the following being outputted:
prove
(`(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`,
REPEAT CONJ_TAC THEN GEN_TAC THEN REFL_TAC);;
The following example is taken from the HOL Light source code file
'real.ml'. It shows how packaged-up proofs that join tactics just by using
the THEN combinator don't reveal where the proof branches are, let
alone how long each branch is. It also shows usage of tactics that take
arguments, such as terms, theorem lists and rules. Rule arguments can be
compositions of rules, or even meta-rules that themselves take rule
arguments.
Enter the following packaged-up tactic proof into the HOL Light session:
# 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));;
Output a flattened version of the proof to reveal its structure:
# print_ge_proof ();;
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 the first ASM_REWRITE_TAC
gets applied to the two subgoals that result from ASM_CASES_TAC,
and finishes off the first subgoal.
We finish with another example taken from the HOL Light source code file
'real.ml'. The packaged-up proof joins tactics by using THENL as
well as THEN, and is tricky to unpick into a flattened proof by
hand.
Enter the following packaged-up tactic proof into the HOL Light session:
# let REAL_LT_INV = prove
(`!x. &0 < x ==> &0 < inv(x)`,
GEN_TAC THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `inv(x)` REAL_LT_NEGTOTAL) THEN
ASM_REWRITE_TAC[] THENL
[RULE_ASSUM_TAC(REWRITE_RULE[REAL_INV_EQ_0]) THEN ASM_REWRITE_TAC[];
DISCH_TAC THEN SUBGOAL_THEN `&0 < --(inv x) * x` MP_TAC THENL
[MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[];
REWRITE_TAC[REAL_MUL_LNEG]]] THEN
SUBGOAL_THEN `inv(x) * x = &1` SUBST1_TAC THENL
[MATCH_MP_TAC REAL_MUL_LINV THEN
UNDISCH_TAC `&0 < x` THEN REAL_ARITH_TAC;
REWRITE_TAC[REAL_LT_RNEG; REAL_ADD_LID; REAL_OF_NUM_LT; ARITH]]);;
Flattening is easy work with Tactician:
# print_ge_proof ();;
g `!x. &0 < x ==> &0 < inv(x)`;;
e (GEN_TAC);;
e (REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC (SPEC `inv x` REAL_LT_NEGTOTAL));;
(* *** Branch 1 *** *)
e (ASM_REWRITE_TAC []);;
e (RULE_ASSUM_TAC (REWRITE_RULE [REAL_INV_EQ_0]));;
e (ASM_REWRITE_TAC []);;
(* *** Branch 2 *** *)
e (ASM_REWRITE_TAC []);;
(* *** Branch 3 *** *)
e (ASM_REWRITE_TAC []);;
e (DISCH_TAC);;
e (SUBGOAL_THEN `&0 < --inv x * x` MP_TAC);;
(* *** Branch 3.1 *** *)
e (MATCH_MP_TAC REAL_LT_MUL);;
e (ASM_REWRITE_TAC []);;
(* *** Branch 3.2 *** *)
e (REWRITE_TAC [REAL_MUL_LNEG]);;
e (SUBGOAL_THEN `inv x * x = &1` SUBST1_TAC);;
(* *** Branch 3.2.1 *** *)
e (MATCH_MP_TAC REAL_MUL_LINV);;
e (UNDISCH_TAC `&0 < x`);;
e (CONV_TAC REAL_ARITH);;
(* *** Branch 3.2.2 *** *)
e (REWRITE_TAC [REAL_LT_RNEG;REAL_ADD_LID;REAL_OF_NUM_LT;ARITH]);;
The flattened proof shows that the application of REPEAT_TCL
resulted in three subgoals, with the first subgoal finishing in the first branch
of the first THENL, the second subgoal finished off by
ASM_REWRITE_TAC prior to the first THENL, and the
third subgoal continuing beyond the second branch of the first
THENL to split and continue to the end of the packaged proof.