# Theorem Proving¶

## Equality¶

Idris allows propositional equalities to be declared, allowing theorems about programs to be stated and proved. An equality type is defined as follows in the Prelude:

```
data Equal : a -> b -> Type where
Refl : Equal x x
```

As a notational convenience, `Equal x y`

can be written as `x = y`

.
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.
For example:

```
fiveIsFive : 5 = 5
fiveIsFive = Refl
twoPlusTwo : 2 + 2 = 4
twoPlusTwo = Refl
```

If we try…

```
twoPlusTwoBad : 2 + 2 = 5
twoPlusTwoBad = Refl
```

…then we’ll get an error:

```
Proofs.idr:8:17--10:1:While processing right hand side of Main.twoPlusTwoBad at Proofs.idr:8:1--10:1:
When unifying 4 = 4 and (fromInteger 2 + fromInteger 2) = (fromInteger 5)
Mismatch between:
4
and
5
```

## The Empty Type¶

There is an empty type, `Void`

, which has no constructors. It is therefore
impossible to construct a canonical element of the empty type. We can therefore
use the empty type to prove that something is impossible, for example zero is
never equal to a successor:

```
disjoint : (n : Nat) -> Z = S n -> Void
disjoint n prf = replace {p = disjointTy} prf ()
where
disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void
```

Don’t worry if you don’t get all the details of how this works just yet -
essentially, it applies the library function `replace`

, which uses an
equality proof to transform a predicate. Here we use it to transform a
value of a type which can exist, the empty tuple, to a value of a type
which can’t, by using a proof of something which can’t exist.

Once we have an element of the empty type, we can prove anything.
`void`

is defined in the library, to assist with proofs by
contradiction.

```
void : Void -> a
```

## Proving 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 Z 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 [1]
explains this relationship. The proof itself is immediate, because
`plus Z n`

normalises to `n`

by the definition of `plus`

:

```
plusReduces n = Refl
```

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`

.

```
plusReducesZ : (n:Nat) -> n = plus n Z
plusReducesZ Z = Refl
plusReducesZ (S k) = cong S (plusReducesZ k)
```

`cong`

is a function defined in the library which states that equality
respects function application:

```
cong : (f : t -> u) -> a = b -> f a = f b
```

To see more detail on what’s going on, we can replace the recursive call to
`plusReducesZ`

with a hole:

```
plusReducesZ (S k) = cong S ?help
```

Then inspecting the type of the hole at the REPL shows us:

```
Main> :t help
k : Nat
-------------------------------------
help : k = (plus k Z)
```

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 Z m = Refl
plusReducesS (S k) m = cong S (plusReducesS k m)
```

Even for small 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 provides interactive editing capabilities, which can help with building proofs. For more details on building proofs interactively in an editor, see Theorem Proving.

## Theorems in Practice¶

The need to prove theorems can arise naturally in practice. For example,
previously (Views and the “with” rule) we implemented `natToBin`

using a function
`parity`

:

```
parity : (n:Nat) -> Parity n
```

We provided a definition for `parity`

, but without explanation. We might
have hoped that it would look something like the following:

```
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = Even {n=S j}
parity (S (S (S (j + j)))) | Odd = Odd {n=S j}
```

Unfortunately, this fails with a type error:

```
With.idr:26:17--27:3:While processing right hand side of Main.with block in 2419 at With.idr:24:3--27:3:
Can't solve constraint between:
plus j (S j)
and
S (plus j j)
```

The problem is that normalising `S j + S j`

, in the type of `Even`

doesn’t result in what we need for the type of the right hand side of
`Parity`

. We know that `S (S (plus j j))`

is going to be equal to
`S j + S j`

, but we need to explain it to Idris with a proof. We can
begin by adding some *holes* (see Totality and Covering) to the definition:

```
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = let result = Even {n=S j} in
?helpEven
parity (S (S (S (j + j)))) | Odd = let result = Odd {n=S j} in
?helpOdd
```

Checking the type of `helpEven`

shows us what we need to prove for the
`Even`

case:

```
j : Nat
result : Parity (S (plus j (S j)))
--------------------------------------
helpEven : Parity (S (S (plus j j)))
```

We can therefore write a helper function to *rewrite* the type to the form
we need:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
```

The `rewrite ... in`

syntax allows you to change the required type of an
expression by rewriting it according to an equality proof. Here, we have
used `plusSuccRightSucc`

, which has the following type:

```
plusSuccRightSucc : (left : Nat) -> (right : Nat) -> S (left + right) = left + S right
```

We can see the effect of `rewrite`

by replacing the right hand side of
`helpEven`

with a hole, and working step by step. Beginning with the following:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = ?helpEven_rhs
```

We can look at the type of `helpEven_rhs`

:

```
j : Nat
p : Parity (S (plus j (S j)))
--------------------------------------
helpEven_rhs : Parity (S (S (plus j j)))
```

Then we can `rewrite`

by applying `plusSuccRightSucc j j`

, which gives
an equation `S (j + j) = j + S j`

, thus replacing `S (j + j)`

(or,
in this case, `S (plus j j)`

since `S (j + j)`

reduces to that) in the
type with `j + S j`

:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in ?helpEven_rhs
```

Checking the type of `helpEven_rhs`

now shows what has happened, including
the type of the equation we just used (as the type of `_rewrite_rule`

):

```
Main> :t helpEven_rhs
j : Nat
p : Parity (S (plus j (S j)))
-------------------------------------
helpEven_rhs : Parity (S (plus j (S j)))
```

Using `rewrite`

and another helper for the `Odd`

case, we can complete
`parity`

as follows:

```
helpEven : (j : Nat) -> Parity (S j + S j) -> Parity (S (S (plus j j)))
helpEven j p = rewrite plusSuccRightSucc j j in p
helpOdd : (j : Nat) -> Parity (S (S (j + S j))) -> Parity (S (S (S (j + j))))
helpOdd j p = rewrite plusSuccRightSucc j j in p
parity : (n:Nat) -> Parity n
parity Z = Even {n=Z}
parity (S Z) = Odd {n=Z}
parity (S (S k)) with (parity k)
parity (S (S (j + j))) | Even = helpEven j (Even {n = S j})
parity (S (S (S (j + j)))) | Odd = helpOdd j (Odd {n = S j})
```

Full details of `rewrite`

are beyond the scope of this introductory tutorial,
but it is covered in the theorem proving tutorial (see Theorem Proving).

## Totality Checking¶

If we really want to trust our proofs, it is important that they are
defined by *total* functions — that is, a function which is defined for
all possible inputs and is guaranteed to terminate. Otherwise we could
construct an element of the empty type, from which we could prove
anything:

```
-- making use of 'hd' being partially defined
empty1 : Void
empty1 = hd [] where
hd : List a -> a
hd (x :: xs) = x
-- not terminating
empty2 : Void
empty2 = empty2
```

Internally, Idris checks every definition for totality, and we can check at
the prompt with the `:total`

command. We see that neither of the above
definitions is total:

```
Void> :total empty1
Void.empty1 is not covering due to call to function empty1:hd
Void> :total empty2
Void.empty2 is possibly not terminating due to recursive path Void.empty2
```

Note the use of the word “possibly” — a totality check can never be certain due to the undecidability of the halting problem. The check is, therefore, conservative. It is also possible (and indeed advisable, in the case of proofs) to mark functions as total so that it will be a compile time error for the totality check to fail:

```
total empty2 : Void
empty2 = empty2
```

Reassuringly, our proof in Section The Empty Type that the zero and successor constructors are disjoint is total:

```
Main> :total disjoint
Main.disjoint is Total
```

The totality check is, necessarily, conservative. To be recorded as
total, a function `f`

must:

- Cover all possible inputs
- Be
*well-founded*— i.e. by the time a sequence of (possibly mutually) recursive calls reaches`f`

again, it must be possible to show that one of its arguments has decreased. - Not use any data types which are not
*strictly positive* - Not call any non-total functions

### Directives and Compiler Flags for Totality¶

Warning

Not all of this is implemented yet for Idris 2

By default, Idris allows all well-typed definitions, whether total or not. However, it is desirable for functions to be total as far as possible, as this provides a guarantee that they provide a result for all possible inputs, in finite time. It is possible to make total functions a requirement, either:

- By using the
`--total`

compiler flag. - By adding a
`%default total`

directive to a source file. All definitions after this will be required to be total, unless explicitly flagged as`partial`

.

All functions *after* a `%default total`

declaration are required to
be total. Correspondingly, after a `%default partial`

declaration, the
requirement is relaxed.

Finally, the compiler flag `--warnpartial`

causes to print a warning
for any undeclared partial function.

### Totality checking issues¶

Please note that the totality checker is not perfect! Firstly, it is
necessarily conservative due to the undecidability of the halting
problem, so many programs which *are* total will not be detected as
such. Secondly, the current implementation has had limited effort put
into it so far, so there may still be cases where it believes a function
is total which is not. Do not rely on it for your proofs yet!

### Hints for totality¶

In cases where you believe a program is total, but Idris does not agree, it is
possible to give hints to the checker to give more detail for a termination
argument. The checker works by ensuring that all chains of recursive calls
eventually lead to one of the arguments decreasing towards a base case, but
sometimes this is hard to spot. For example, the following definition cannot be
checked as `total`

because the checker cannot decide that `filter (< x) xs`

will always be smaller than `(x :: xs)`

:

```
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (filter (< x) xs) ++
(x :: qsort (filter (>= x) xs))
```

The function `assert_smaller`

, defined in the prelude, is intended to
address this problem:

```
assert_smaller : a -> a -> a
assert_smaller x y = y
```

It simply evaluates to its second argument, but also asserts to the
totality checker that `y`

is structurally smaller than `x`

. This can
be used to explain the reasoning for totality if the checker cannot work
it out itself. The above example can now be written as:

```
total
qsort : Ord a => List a -> List a
qsort [] = []
qsort (x :: xs)
= qsort (assert_smaller (x :: xs) (filter (< x) xs)) ++
(x :: qsort (assert_smaller (x :: xs) (filter (>= x) xs)))
```

The expression `assert_smaller (x :: xs) (filter (<= x) xs)`

asserts
that the result of the filter will always be smaller than the pattern
`(x :: xs)`

.

In more extreme cases, the function `assert_total`

marks a
subexpression as always being total:

```
assert_total : a -> a
assert_total x = x
```

In general, this function should be avoided, but it can be very useful when reasoning about primitives or externally defined functions (for example from a C library) where totality can be shown by an external argument.

[1] | Timothy G. Griffin. 1989. A formulae-as-type notion of control. In Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ‘90). ACM, New York, NY, USA, 47-58. DOI=10.1145/96709.96714 https://doi.acm.org/10.1145/96709.96714 |