# Interactive Theorem Proving¶

Idris also supports interactive theorem proving via tactics. This is generally not recommended to be used directly, but rather used as a mechanism for building proof automation which is beyond the scope of this tutorial. In this section, we briefly discus tactics.

One way to write proofs interactively is to write the general *structure* of
the proof, and use the interactive mode to complete the details.
Consider the following definition, proved in Theorem Proving:

```
plusReduces : (n:Nat) -> plus Z n = n
```

We’ll be constructing the proof by *induction*, so we write the cases for `Z`

and `S`

, with a recursive call in the `S`

case giving the inductive
hypothesis, and insert *metavariables* for the rest of the definition:

```
plusReducesZ' : (n:Nat) -> n = plus n Z
plusReducesZ' Z = ?plusredZ_Z
plusReducesZ' (S k) = let ih = plusReducesZ' k in
?plusredZ_S
```

On running , two global names are created, `plusredZ_Z`

and
`plusredZ_S`

, with no definition. We can use the `:m`

command at the
prompt to find out which metavariables are still to be solved (or, more
precisely, which functions exist but have no definitions), then the
`:t`

command to see their types:

```
*theorems> :m
Global metavariables:
[plusredZ_S,plusredZ_Z]
```

```
*theorems> :t plusredZ_Z
plusredZ_Z : Z = plus Z Z
*theorems> :t plusredZ_S
plusredZ_S : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
```

The `:p`

command enters interactive proof mode, which can be used to
complete the missing definitions.

```
*theorems> :p plusredZ_Z
---------------------------------- (plusredZ_Z) --------
{hole0} : Z = plus Z Z
```

This gives us a list of premises (above the line; there are none here)
and the current goal (below the line; named `{hole0}`

here). At the
prompt we can enter tactics to direct the construction of the proof. In
this case, we can normalise the goal with the `compute`

tactic:

```
-plusredZ_Z> compute
---------------------------------- (plusredZ_Z) --------
{hole0} : Z = Z
```

Now we have to prove that `Z`

equals `Z`

, which is easy to prove by
`Refl`

. To apply a function, such as `Refl`

, we use `refine`

which
introduces subgoals for each of the function’s explicit arguments
(`Refl`

has none):

```
-plusredZ_Z> refine Refl
plusredZ_Z: no more goals
```

Here, we could also have used the `trivial`

tactic, which tries to
refine by `Refl`

, and if that fails, tries to refine by each name in
the local context. When a proof is complete, we use the `qed`

tactic
to add the proof to the global context, and remove the metavariable from
the unsolved metavariables list. This also outputs a trace of the proof:

```
-plusredZ_Z> qed
plusredZ_Z = proof
compute
refine Refl
```

```
*theorems> :m
Global metavariables:
[plusredZ_S]
```

The `:addproof`

command, at the interactive prompt, will add the proof
to the source file (effectively in an appendix). Let us now prove the
other required lemma, `plusredZ_S`

:

```
*theorems> :p plusredZ_S
---------------------------------- (plusredZ_S) --------
{hole0} : (k : Nat) -> (k = plus k Z) -> S k = plus (S k) Z
```

In this case, the goal is a function type, using `k`

(the argument
accessible by pattern matching) and `ih`

— the local variable
containing the result of the recursive call. We can introduce these as
premisses using the `intro`

tactic twice (or `intros`

, which
introduces all arguments as premisses). This gives:

```
k : Nat
ih : k = plus k Z
---------------------------------- (plusredZ_S) --------
{hole2} : S k = plus (S k) Z
```

Since plus is defined by recursion on its first argument, the term
`plus (S k) Z`

in the goal can be simplified, so we use `compute`

.

```
k : Nat
ih : k = plus k Z
---------------------------------- (plusredZ_S) --------
{hole2} : S k = S (plus k Z)
```

We know, from the type of `ih`

, that `k = plus k Z`

, so we would
like to use this knowledge to replace `plus k Z`

in the goal with
`k`

. We can achieve this with the `rewrite`

tactic:

```
-plusredZ_S> rewrite ih
k : Nat
ih : k = plus k Z
---------------------------------- (plusredZ_S) --------
{hole3} : S k = S k
-plusredZ_S>
```

The `rewrite`

tactic takes an equality proof as an argument, and tries
to rewrite the goal using that proof. Here, it results in an equality
which is trivially provable:

```
-plusredZ_S> trivial
plusredZ_S: no more goals
-plusredZ_S> qed
plusredZ_S = proof {
intros;
rewrite ih;
trivial;
}
```

Again, we can add this proof to the end of our source file using the
`:addproof`

command at the interactive prompt.