\section{Provisional Definitions}

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 \texttt{parity} function:

\begin{SaveVerbatim}{pardecl}

data Parity : Nat -> Type where
   even : Parity (n + n)
   odd  : Parity (S (n + n))

parity : (n:Nat) -> Parity n

\end{SaveVerbatim}
\useverb{pardecl}

\noindent
We'd like to implement this as follows:

\begin{SaveVerbatim}{parfail}

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}

\end{SaveVerbatim}
\useverb{parfail}

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

\begin{SaveVerbatim}{parerror}

views.idr:12:Can't unify Parity (plus (S j) (S j)) with 
Parity (S (S (plus j j)))

\end{SaveVerbatim}
\useverb{parerror}

\noindent
The type checker
is telling us that \texttt{(j+1)+(j+1)} and \texttt{2+j+j}
do not normalise to the same value.
This is because \texttt{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?

\subsection{Provisional definitions}

\emph{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.

\begin{itemize}
\item When \emph{prototyping}, it is useful to be able to test programs before
finishing all the details of proofs.  
\item When \emph{reading} a program, it is often much clearer to defer the proof
details so that they do not distract the reader from the underlying algorithm.
\end{itemize}

\noindent
Provisional definitions are written in the same way as ordinary definitions,
except that they introduce the right hand side with a \texttt{?=} rathar than
\texttt{=}. We define
\texttt{parity} as follows:

\begin{SaveVerbatim}{paritypro}

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}

\end{SaveVerbatim}
\useverb{paritypro}

\noindent
When written in this form, instead of reporting a type error, \Idris{} will insert
a metavariable standing for a theorem which will correct the type error. \Idris{} 
tells us we have two proof obligations, with names generated from the module and
function names:

\begin{SaveVerbatim}{prometas}

*views> :m 
Global metavariables:
        [views.parity_lemma_2,views.parity_lemma_1]

\end{SaveVerbatim}
\useverb{prometas}

\noindent
The first of these has the following type:

\begin{SaveVerbatim}{prolem1}

*views> :p views.parity_lemma_1 

---------------------------------- (views.parity_lemma_1) --------
{hole0} : (j : Nat) -> (Parity (plus (S j) (S j))) -> Parity (S (S (plus j j)))

-views.parity_lemma_1>  

\end{SaveVerbatim}
\useverb{prolem1}

\noindent
The two arguments are \texttt{j}, the variable in scope from the pattern match,
and \texttt{value}, which is the value we gave in the right hand side of the
provisional definition. Our goal is to rewrite the type so that we can use
this value.
We can achieve this using the following theorem from
the prelude:

\begin{SaveVerbatim}{plusnsm}

plusSuccRightSucc : (left : Nat) -> (right : Nat) ->
  S (plus left right) = plus left (S right)


\end{SaveVerbatim}
\useverb{plusnsm}

\noindent
After applying \texttt{intro} twice, we have:

\begin{SaveVerbatim}{prolemii}

-views.parity_lemma_1> intro 

  j : Nat
  value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole2} : Parity (S (S (plus j j)))

\end{SaveVerbatim}
\useverb{prolemii}

\noindent
Then we apply the \texttt{plusSuccRightSucc} rewrite rule, symmetrically,
to \texttt{j} and \texttt{j}, giving:

\begin{SaveVerbatim}{prolemr}

-views.parity_lemma_1> rewrite sym (plusSuccRightSucc j j) 
 
  j : Nat
  value : Parity (S (plus j (S j)))
---------------------------------- (views.parity_lemma_1) --------
{hole3} : Parity (S (plus j (S j)))

\end{SaveVerbatim}
\useverb{prolemr}

\noindent
\texttt{sym} is a function, defined in the library, which reverses the order of the rewrite:

\begin{SaveVerbatim}{sym}

sym : l = r -> r = l
sym refl = refl

\end{SaveVerbatim}
\useverb{sym} 

\noindent
We can complete this proof using the \texttt{trivial} tactic, which finds 
\texttt{value} in the premisses. The proof of the second lemma proceeds in
exactly the same way.

\subsection{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!

Therefore, \Idris{} provides a built-in coercion function, which allows you to use
a value of the incorrect types:

\begin{SaveVerbatim}{believe}

believe_me : a -> b 

\end{SaveVerbatim}
\useverb{believe}

\noindent
Obviously, this should be used with extreme caution. It is useful when prototyping, and
can also be appropriate when asserting properties of external code (perhaps in an
external C library). The ``proof'' of \texttt{views.parity\_lemma\_1} using this is:

\begin{SaveVerbatim}{pladodgy}

views.parity_lemma_2 = proof {
    intro;
    intro;
    exact believe_me value;
}

\end{SaveVerbatim}
\useverb{pladodgy}

\noindent
The \texttt{exact} tactic allows us to provide an exact value for the proof. In this case,
we assert that the value we gave was correct.

\subsection{Example: Binary numbers}

Previously, we implemented conversion to binary numbers using the \texttt{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 \texttt{Nat} equivalent. This is a common
pattern, linking a representation (in this case \texttt{Binary}) with a meaning (in this
case \texttt{Nat}):

\begin{SaveVerbatim}{bindef}

data Binary : Nat -> Type where
   bEnd : Binary Z
   bO : Binary n -> Binary (n + n)
   bI : Binary n -> Binary (S (n + n))

\end{SaveVerbatim}
\useverb{bindef}

\noindent
\texttt{bO} and \texttt{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,
\texttt{n + n} or \texttt{S (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:

\begin{SaveVerbatim}{ntbty}

natToBin : (n:Nat) -> Binary n

\end{SaveVerbatim}
\useverb{ntbty}

\noindent
The \texttt{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:

\begin{SaveVerbatim}{ntbdef}

natToBin : (n:Nat) -> Binary n
natToBin Z = bEnd
natToBin (S k) with (parity k)
   natToBin (S (j + j))     | even  = bI (natToBin j)
   natToBin (S (S (j + j))) | odd  ?= bO (natToBin (S j))

\end{SaveVerbatim}
\useverb{ntbdef}

\noindent
The problem with the odd case is the same as in the definition of \texttt{parity}, and
the proof proceeds in the same way:

\begin{SaveVerbatim}{ntboddprf}

natToBin_lemma_1 = proof {
    intro;
    intro;
    rewrite sym (plusSuccRightSucc j j);
    trivial;
}

\end{SaveVerbatim}
\useverb{ntboddprf}

\noindent
To finish, we'll implement a main program which reads an integer from the user and
outputs it in binary. 

\begin{SaveVerbatim}{binmain}

main : IO ()
main = do putStr "Enter a number: "
          x <- getLine
          print (natToBin (fromInteger (cast x)))

\end{SaveVerbatim}
\useverb{binmain}

\noindent
For this to work, of course, we need a \texttt{Show} instance for \texttt{Binary n}:

\begin{SaveVerbatim}{showbin}

instance Show (Binary n) where
    show (bO x) = show x ++ "0"
    show (bI x) = show x ++ "1"
    show bEnd = ""

\end{SaveVerbatim}
\useverb{showbin}