``` ```

NOTE: This tutorial describes an old version of Idris. For an up to date tutorial, see here.

## Theorem Proving

Equality | Simple theorems | Interactive theorem proving | Tactics | Theorems in the library | Proving by pattern matching.

### Equality

Idris allows propositional equalities to be declared, allowing theorems about programs to be stated and proved. Equality is built in, but conceptually has the following definition:

`data (=) : a -> b -> Set where`
`   refl x : x = x;`

Equalities can be proposed between any values of any types, but the only way to construct a proof of equality is if values actually are equal.

`Idris> refl 5`
`refl 5 : 5=5`

### Simple theorems

When type checking dependent types, the type itself gets normalised. So imagine we want to prove the following theorem about the reduction behaviour of `plus`:

`plusReduces : (n:Nat) -> (plus O n = n);`

We've written down the statement of the theorem as a type, in just the same way as we would write the type of a program. In fact there is no real distinction between proofs and programs. A proof, as far as we are concerned here, is merely a program with a precise enough type to guarantee a particular property of interest.

We won't go into details here, but the Curry-Howard correspondence explains this relationship.

The proof itself is trivial, because `plus O n` normalises to `n` by the definition of `plus`:

`plusReduces n = refl n;`

It is slightly harder if we try the arguments the other way, because `plus` is defined by recursion on its first argument. The proof also works by recursion on the first argument to `plus`, namely `n`.

`plusReducesO : (n:Nat) -> (n = plus n O);`
`plusReducesO O = refl _;`
`plusReducesO (S k) = eq_resp_S (plusReducesO k);`

`eq_resp_S` is a function defined in the library which states that equality respects successor:

`eq_resp_S : (m=n) -> ((S m) = (S n));`

We can do the same for the reduction behaviour of `plus` on successors:

`plusReducesS : (n:Nat) -> (m:Nat) -> (S (plus n m) = plus n (S m));`
`plusReducesS O m = refl _;`
`plusReducesS (S k) m = eq_resp_S (plusReducesS k m);`

Even for trival theorems like these, the proofs are a little tricky to construct in one go. When things get even slightly more complicated, it becomes too much to think about to construct proofs in this 'batch mode'. Idris therefore provides an interactive proof mode.

### Interactive theorem proving

Instead of writing the proof in one go, we can write it interactively, by declaring the type then starting up Idris.

`plusReducesO' : (n:Nat) -> (n = plus n O);`

Using the `:p` command enters interactive proof mode:

`Idris> :p plusReducesO'`

`--------------------------------`
`H0 ? (n : Nat) -> n=plus n O`

`plusReducesO'> `

This gives us a list of premisses, above the line (there are none here, yet), and the current goal (named `H0` here) below the line. At the prompt we can enter tactics to direct the construction of a proof. For a goal of a function type, `intro` will introduce the argument as a premiss:

`plusReducesO'> intro`

`n : Nat`

`--------------------------------`
`H0 ? n=plus n O`

We implemented `plus` by recursion on its first argument, so it makes sense to continue the proof by induction on its first argument, `n`. The `induction` tactic splits the goal into subgoals for each constructor of `n`:

`plusReducesO'> induction n`

`n : Nat`

`--------------------------------`
`H2 ? O=plus O O`

This goal can be solved by reflexivity (the `refl` tactic), because `plus O O` normalises to `O`:

`plusReducesO'> refl`

`n : Nat`

`--------------------------------`
`H1 ? (k:Nat) -> (k=plus k O) -> S k=plus (S k) O`

This goal is for the successor case. The goal to be proved is a function of two arguments. The first, `k`, is the argument to the successor. The second is an induction hypothesis, which states that the theorem we are trying to prove holds for `k`. We'll introduce these as premisses:

`plusReducesO'> intro k,ih`

`n : Nat`
`k : Nat`
`ih : k=plus k O`

`--------------------------------`
`H1 ? S k=plus (S k) O`

It helps here to reduce the goal to normal form, so that we can see that the induction hypothesis can be applied. The `compute` tactic achieves this:

`plusReducesO'> compute`

`n : Nat`
`k : Nat`
`ih : k=plus k O`

`--------------------------------`
`H1 ? S k=S (plus k O)`

The induction hypothesis `ih` states that `k=plus k O`, so we can use it to replace the instance of `plus k O` in the goal with `k`. The `rewrite p` tactic, given a premiss `p` of type `x=y` will replace any instance of `y` in the goal with `x`. (Alternatively, `rewrite <- p`, for some proof `p`, will apply the rule backwards.)

`plusReducesO'> rewrite ih`

`n : Nat`
`k : Nat`
`ih : k=plus k O`

`--------------------------------`
`H3 ? S k=S k`

This final goal is easily proved by `refl`:

`plusReducesO'> refl`

`No more goals`

On completing a proof, entering `qed` will verify the resulting proof and output a proof script. This script can be pasted directly into the original program:

`plusReducesO'> qed`

`plusReducesO' proof {`
`        %intro;`
`        %induction n;`
`        %refl;`
`        %intro k,ih;`
`        %compute;`
`        %rewrite ih;`
`        %refl;`
`        %qed;`
`};`

### Tactics

There are several tactics available, some of which have been used above. The tactics are briefly described here:

• `intro`: If the goal is of the form `(a:A) -> B`, introduce a premiss `a`, and replace the goal with `B`.
• `intro x,y,...`: Introduce several premisses at once.
• `compute`: Normalise the goal
• `refl`: Solve a goal of the form `x=y` where `x` and `y` have the same normal form.
• `induction t`: Solve a goal by induction on `t`. Creates subgoals for each possible constructor of `t`.
• `rewrite t`: If `t` has type `x=y` replace any instance of `y` in the goal with `x`
• `rewrite <- t`: If `t` has type `x=y` replace any instance of `x` in the goal with `y`
• `fill x`: If `x` has type `T`, then `fill x` solves a goal of type `T`.
• `refine x`: If `x` has a function type, returning a value of type `T`, `refine x` introduces subgoals for each argument of `x`, attempting to solve as many as possible automatically by unification.
• `trivial`: If there is a premiss which solves the goal immediately, use it.
• `undo`: Undo the previous tactic.
• `generalise t`: Abstract the goal over a variable `x` and replace any occurence of the term `t` in the goal with `x`
• `unfold n`: Replace any occurrence of the name `n` in the goal with its definition, if possible.
• `decide t`: This is a slightly complicated tactic, but can be useful for creating and applying decision procedures. If the goal is of the form ```T a b c```, and `t` has type `t : (a:A) -> (b:B) -> (c:C) -> Maybe (T a b c)`, apply `t a b c`. If the result is `Just x`, solve the goal with `x`, otherwise fail.

A few other more advanced tactics are also available (`believe`, `use` and `mktac`) and will be described later. In proof mode, `:q` will return to the `Idris>` prompt.

### Theorems in the library

The library includes a variety of useful theorems about natural number arithmetic. These include some about addition...

`plus_nO    : (n:Nat) -> ((plus n O) = n);`
`plus_nSm   : (plus n (S m) = (S (plus n m)));`
`plus_comm  : (x:Nat, y:Nat) -> (plus x y)= plus y x);`
`plus_assoc : (m:Nat, n:Nat, p:Nat) -> `
`             (plus m (plus n p) = plus (plus m n) p);`

`mult_nO      : (n:Nat) -> ((mult n O) = O);`
`mult_nSm     : (n:Nat ,m:Nat) -> ((mult n (S m)) = (plus n (mult n m)));`
`mult_comm    : (x:Nat, y:Nat) -> ((mult x y) = (mult y x));`
`mult_distrib : (m:Nat, n:Nat, p:Nat) ->`
`               (plus (mult m p) (mult n p) = mult (plus m n) p);`

### Proving by pattern matching.

Of course we're not limited to theorems about `Nat`. We can state the following theorem about associativity of list append:

`app_assoc : (xs:List a) -> (ys:List a) -> (zs:List a) ->`
`            (app xs (app ys zs) = app (app xs ys) zs);`

For reference, `app` is implemented in the library, as follows, by pattern matching and recursion on the first argument:

`app : List a -> List a -> List a;`
`app  Nil        xs = xs;`
`app (Cons x xs) ys = Cons x (app xs ys);`

Proofs of a function's properties will typically be easier to write if they follow the structure of the function itself. It's therefore easier to break this one down by writing down a pattern matching definition, and using the theorem prover to add the final details. We can do this by leaving holes (or metavariables) in the proof, marked by `?name`:

`app_assoc Nil ys zs = ?app_assocNil;`
`app_assoc (Cons x xs) ys zs = ?app_assocCons;`

Holes can also be given without a name, i.e. just with `?`, in which case the system will choose a name based on the top level function. When we start up Idris, we can ask what proof obligations remain with the `:m` command (short for `:metavariables`):

`Idris> :m`
`Proof obligations:`
`        [app_assocNil,app_assocCons]`

Again, we use `:p` to build interactive proofs. `app_assocNil` is straightforward:

`app_assocNil proof {`
`        %intro;`
`        %refl;`
`        %qed;`
`};`

When doing proofs in this way, we need to make recursive calls (to get the induction hypothesis) explicit, since we'll have no access to `app_assoc` in the proof script. We can do this as follows:

`app_assoc (Cons x xs) ys zs = let rec = app_assoc xs ys zs in ?app_assocCons;`

Now we can prove `app_assocCons` by rewriting by `rec`:

`app_assocCons proof {`
`        %intro;`
`        %rewrite rec;`
`        %refl;`
`        %qed;`
`};`

`app_assoc` is also in the library, in `list.idr`.

Source for this chapter

``` ```