Proof Technologies Ltd

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

``` # 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);; ```

## Example 2

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);; ```

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

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