Previous | Contents | Next

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

Provisional Definitions

Edwin Brady

Parity | Provisional definitions | Example: Binary numbers

Parity

Sometimes when programming with dependent types, the type required by the type checker and the type of the program we have written will be different (in that they do not have the same normal form), but nevertheless provably equal. For example, recall the parity function:

data Parity : Nat -> Set where
   even : Parity (plus n n)
 | odd  : Parity (S (plus n n));

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

We'd like to implement this as follows:

parity O = even {n=O};
parity (S O) = odd {n=O};
parity (S (S k)) with parity k {
  parity (S (S (plus j j)))     | even = even {n=S j};
  parity (S (S (S (plus j j)))) | odd  = odd {n=S j};
}

This simply states that zero is even, one is odd, and recursively, the parity of k+2 is the same as the parity of k. Explicitly marking the value of n in even and odd is necessary to help type inference. Unfortunately, the type checker rejects this:

provisional.idr:23:Can't unify Parity (S (S (plus j j))) and Parity (plus (S j) (S j))

It's telling us that 2+j+j and (j+1)+(j+1) do not normalise to the same value. This is because plus is defined by recursion on its first argument, and in the second value, there is a successor symbol on the second argument, so this will not help with reduction. These values are obviously equal - how can we rewrite the program to fix this problem?

Provisional definitions

Provisional definitions help with this problem by allowing us to defer the proof details until a later point. There are two main reasons why they are useful.

They are written in pattern matching form with a ?= instead of = before the right hand side, and a name of a theorem to generate. We write parity as follows:

parity O = even {n=O};
parity (S O) = odd {n=O};
parity (S (S k)) with parity k {
  parity (S (S (plus j j)))     | even ?= even {n=S j};  [paritySSe]
  parity (S (S (S (plus j j)))) | odd  ?= odd {n=S j};   [paritySSo]
}

When written in this form, instead of reporting a type error, Idris will insert a hole for a theorem which will correct the type error. Idris tells us we have two proof obligations:

Idris> :m
Proof obligations:
        [paritySSe,paritySSo]

The first of these, paritySSe has the following type.

Idris> :p paritySSe

--------------------------------
H0 ? (j : Nat) -> (value : Parity (S (plus j (S j)))) -> Parity (S (S (plus j j)))

There are two arguments; j is the variable in scope from the pattern on the left hand side, and value is the value we tried to use in the definition. To prove this, first we introduce the arguments:

paritySSeintro

j : Nat
value : Parity (S (plus j (S j)))

--------------------------------
H0 ? Parity (S (S (plus j j)))

Next, we declare that we would like to use the value to solve the goal. If there is a goal of the form P x, and a premiss p of type P y, then use p will solve the goal, introducing a subgoal x=y:

paritySSeuse value

j : Nat
value : Parity (S (plus j (S j)))

--------------------------------
equality ? S (S (plus j j))=S (plus j (S j))

We can solve this goal by applying a theorem from the library plus_nSm:

paritySSerewrite plus_nSm {n=j} {m=j}

j : Nat
value : Parity (S (plus j (S j)))

--------------------------------
H2 ? S (plus j (S j))=S (plus j (S j))

We finish the proof with refl then qed. This results in a proof script which can be pasted in to the source file (perhaps as a kind of 'appendix' to the program):

paritySSe proof {
        %intro;
        %use value;
        %rewrite plus_nSm j j;
        %refl;
        %qed;
};

The proof of paritySSo proceeds in a similar fashion. Developing programs and their associated proofs in this way allows us to present an algorithm to the reader while deferring the precise details of the explanation, required only by the machine, until a separate point in the source file.

Suspension of disbelief

Idris requires that proofs be complete before compiling programs (although evaluation at the prompt is possible without proof details). Sometimes, especially when prototyping, it is easier not to have to do this. It might even be beneficial to test programs before attempting to prove things about them - if testing finds an error, you know you had better not waste your time proving something!

For this situation, there is a variant of the use tactic, called believe, which uses a library function __Suspend_Disbelief to fill in the equality proof:

__Suspend_Disbelief : (m:A) -> (n:A) -> (m = n);

Obviously, there is no proof of this, so any program with uses it should not be trusted. Nevertheless, it can be useful when prototyping. The 'proof' of paritySSe would be written as:

paritySSe proof {
        %intro;
        %believe value;
        %qed;
};

Example: Binary numbers

Previously, we implemented conversion to binary numbers using the Parity view. Here, we show how to use the same view to implement a verified conversion to binary.

We begin by indexing binary numbers over their Nat equivalent. This is a common pattern, linking a representation (in this case Binary) with a meaning (in this case Nat):

data Binary : Nat -> Set where
   bEnd : Binary O
 | bO : Binary n -> Binary (plus n n)
 | bI : Binary n -> Binary (S (plus n n));

bO and bI take a binary number as an argument and effectively shift it one bit left, adding either a zero or one as the new least significant bit. The index, plus n n or S (plus n n) states the result that this left shift then add will have to the meaning of the number. This will result in a representation with the least significant bit at the front.

Now a function which converts a Nat to binary will state, in the type, that the resulting binary number is a faithful representation of the original Nat:

natToBin : (n:Nat) -> Binary n;

The Parity view makes the definition fairly simple - halving the number is effectively a right shift after all - although we need to use a provisional definition in the odd case:

natToBin O = bEnd;
natToBin (S kwith parity k {
   natToBin (S (plus j j))     | even  = bI (natToBin j);
   natToBin (S (S (plus j j))) | odd  ?= bO (natToBin (S j)); [ntbOdd]
}

The problem with the odd case is the same as in the definition of parity, and the proof proceeds in the same way:

ntbOdd proof {
        %intro;
        %use value;
        %rewrite plus_nSm j j;
        %refl;
        %qed;
};

If we were to take an extreme viewpoint, we could say we don't need to test natToBin, because we've proved it works because of its type. But let's check anyway...

IdrisnatToBin (intToNat 42)
bO (bI (bO (bI (bO (bI bEnd))))) 


Source for this chapter

Previous | Contents | Next