Tactician Examples

Tactician Examples

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.

Example 1

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):

# g `(!x. x = x) /\ (!y.y = y) /\ (!z.z = z)`;;
# e (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);;

Example 2

Next we illustrate outputting a partial "g and e" style proof and packaging up a completd 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);;

Example 3

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

Example 4

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.