Theorem Proving in Idris

Question

I was reading Idris tutorial. And I can't understand the following code.

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

So far, what I figure out is ... Void is the empty type which is used to prove something is impossible.

replace : (x = y) -> P x -> P y replace uses an equality proof to transform a predicate.

My questions are:

1. which one is an equality proof? (Z = S n)?

2. which one is a predicate? the disjointTy function?

3. What's the purpose of disjointTy? Does disjointTy Z = () means Z is in one Type "land" () and (S k) is in another land Void?

4. In what way can an Void output represent contradiction?

Ps. What I know about proving is "all things are no matched then it is false." or "find one thing that is contradictory"...

Answer 1

which one is an equality proof? (Z = S n)?

The p parameter is the equality proof here. p has type Z = S n.

which one is a predicate? the disjointTy function?

Yes, you are right.

What's the purpose of disjointTy?

Let me repeat the definition of disjointTy here:

disjointTy : Nat -> Type
disjointTy Z = ()
disjointTy (S k) = Void

The purpose of disjointTy is to be that predicate replace function needs. This consideration determines the type of disjointTy, viz. [domain] -> Type. Since we have equality between naturals numbers, [domain] is Nat.

To understand how the body has been constructed we need to take a look at replace one more time:

replace : (x = y) -> P x -> P y

Recall that we have p of Z = S n, so x from the above type is Z and y is S n. To call replace we need to construct a term of type P x, i.e. P Z in our case. This means the type P Z returns must be easily constructible, e.g. the unit type is the ideal candidate for this. We have justified disjointTy Z = () clause of the definition of disjointTy. Of course it's not the only option, we could have used any other inhabited (non-empty) type, like Bool or Nat, etc.

The return value in the second clause of disjointTy is obvious now -- we want replace to return a value of Void type, so P (S n) has to be Void.

Next, we use disjointTy like so:

replace   {P = disjointTy}   p    ()
           ^                 ^    ^
           |                 |    |
           |                 |    the value of `()` type
           |                 |
           |                 proof term of Z = S n 
           |
           we are saying "this is the predicate"

As a bonus, here is an alternative proof:

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

I have used False, but could have used True -- it doesn't matter. What matters is our ability to construct a term of type disjointTy Z.

In what way can an Void output represent contradiction?

Void is defined like so:

data Void : Type where

It has no constructors! There is no way to create a term of this type whatsoever (under some conditions: like Idris' implementation is correct and the underlying logic of Idris is sane, etc.). So if some function claims it can return a term of type Void there must be something fishy going on. Our function says: if you give me a proof of Z = S n, I will return a term of the empty type. This means Z = S n cannot be constructed in the first place because it leads to a contradiction.