# The Interactive Theorem Prover¶

This short guide contributed by a community member illustrates how to prove associativity of addition on `Nat` using the interactive theorem prover.

First we define a module `Foo.idr`

```module Foo

plusAssoc : plus n (plus m o) = plus (plus n m) o
plusAssoc = ?rhs
```

We wish to perform induction on `n`. First we load the file into the Idris `REPL` as follows:

```\$ idris Foo.idr
```

We will be given the following prompt, in future releases the version string will differ:

```     ____    __     _
/  _/___/ /____(_)____
/ // __  / ___/ / ___/     Version 0.9.18.1
_/ // /_/ / /  / (__  )      http://www.idris-lang.org/
/___/\__,_/_/  /_/____/       Type :? for help

Idris is free software with ABSOLUTELY NO WARRANTY.
For details type :warranty.
Type checking ./Foo.idr
Metavariables: Foo.rhs
*Foo>
```

## Explore the Context¶

We start the interactive session by asking Idris to prove the hole `rhs` using the command `:p rhs`. Idris by default will show us the initial context. This looks as follows:

```*Foo> :p rhs
----------                 Goal:                  ----------
{ hole 0 }:
(n : Nat) ->
(m : Nat) ->
(o : Nat) ->
plus n (plus m o) = plus (plus n m) o
```

## Application of Intros¶

We first apply the `intros` tactic:

```-Foo.rhs> intros
----------              Other goals:              ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
----------                 Goal:                  ----------
{ hole 3 }:
plus n (plus m o) = plus (plus n m) o
```

## Induction on `n`¶

Then apply `induction` on to `n`:

```-Foo.rhs> induction n
----------              Other goals:              ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
----------                 Goal:                  ----------
elim_Z0:
plus Z (plus m o) = plus (plus Z m) o
```

## Compute¶

```-Foo.rhs> compute
----------              Other goals:              ----------
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
----------                 Goal:                  ----------
elim_Z0:
plus m o = plus m o
```

## Trivial¶

```-Foo.rhs> trivial
----------              Other goals:              ----------
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
----------                 Goal:                  ----------
elim_S0:
(n__0 : Nat) ->
(plus n__0 (plus m o) = plus (plus n__0 m) o) ->
plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
```

## Intros¶

```-Foo.rhs> intros
----------              Other goals:              ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 5 }:
plus (S n__0) (plus m o) = plus (plus (S n__0) m) o
```

## Compute¶

```-Foo.rhs> compute
----------              Other goals:              ----------
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 5 }:
S (plus n__0 (plus m o)) = S (plus (plus n__0 m) o)
```

## Rewrite¶

```-Foo.rhs> rewrite ihn__0
----------              Other goals:              ----------
{ hole 5 }
{ hole 4 }
elim_S0
{ hole 2 }
{ hole 1 }
{ hole 0 }
----------              Assumptions:              ----------
n : Nat
m : Nat
o : Nat
n__0 : Nat
ihn__0 : plus n__0 (plus m o) = plus (plus n__0 m) o
----------                 Goal:                  ----------
{ hole 6 }:
S (plus n__0 (plus m o)) = S (plus n__0 (plus m o))
```

## Trivial¶

```-Foo.rhs> trivial
rhs: No more goals.
-Foo.rhs> qed
Proof completed!
Foo.rhs = proof
intros
induction n
compute
trivial
intros
compute
rewrite ihn__0
trivial
```

Two goals were created: one for `Z` and one for `S`. Here we have proven associativity, and assembled a tactic based proof script. This proof script can be added to `Foo.idr`.