# Reverse, Reverse: Theorem Proving with Idris

Constructors are red.
Types are blue.
Because Idris loves you.

In How Functional Programming Mattered, Zhenjiang Hu, John Hughes, and Meng Wang argue that (pure) functional programming has changed the way we think about programs. An important part of the reason why is equational reasoning and referential transparency.

As an example, Hu, Hughes, and Wang use a function to reverse a list to show how functional languages such as Haskell allow us to write properties of programs as programs, and to prove such properties by hand, just like in mathematics. But functional languages such as Agda and Idris go a step further. They have dependent types, which means we can write proofs of properties of programs as programs.

In this blog post, we’ll use Haskell (GHC 7.10.2 and QuickCheck 2.8.1) to test that a function to reverse a list satisfies the property that such a function is its own inverse, and Idris (0.9.19) to prove that it does.

Let’s begin by creating a file `reverse-reverse.hs` for the Haskell code. We’re not going to use the standard `++` and `reverse` functions, so let’s hide them:

``import Prelude hiding ((++), reverse)``

We can now add the definition of the `++` function to append lists. This is not necessary because it corresponds to the standard `++` function, but it can be useful to include it for reference:

``````infixr 5 ++

(++) :: [a] -> [a] -> [a]
[]     ++ ys = ys
(x:xs) ++ ys = x : xs ++ ys``````

Now, let’s define a `reverse` function to reverse lists:

``````reverse :: [a] -> [a]
reverse []     = []
reverse (x:xs) = reverse xs ++ [x]``````

Given a definition like the one above, we can express as a function the property that `reverse` should be its own inverse:

``````reverseReverse :: [Integer] -> Bool
reverseReverse xs = reverse (reverse xs) == xs``````

This function returns `True` if applying `reverse` twice to a list yields the same list, and `False` otherwise:

``````ghci> reverseReverse [1,2,3,4,5]
True``````

We can test this property using QuickCheck, which will generate 100 lists of integers and check that the property holds for all of them:

``````ghci> import Test.QuickCheck
ghci> quickCheck reverseReverse
+++ OK, passed 100 tests.``````

We’ve just tested that our definition of `reverse` satisfies the `reverseReverse` property. Equational reasoning, however, gives us the power to reason about definitions. Thus, we can actually prove that the property holds for all finite lists. We can do it by induction on the given list, as follows:

• In the case of an empty list:

`reverse (reverse [])`
`==` (by definition of `reverse`)
`reverse []`
`==` (by definition of `reverse`)
`[]`

• And, in the case of a list `x:xs`:

`reverse (reverse (x:xs))`
`==` (by definition of `reverse`)
`reverse (reverse xs ++ [x])`
`==` (see below)
`reverse [x] ++ reverse (reverse xs)`
`==` (by inductive hypothesis)
`reverse [x] ++ xs`
`==` (by definition of `reverse`)
`(reverse [] ++ [x]) ++ xs`
`==` (by definitions of `reverse` and `++`)
`x:xs`

In order to prove that `reverse` is its own inverse, we need to prove that `reverse` and `++` commute for all finite lists:

``reverse (xs ++ ys) == reverse ys ++ reverse xs``

We won’t prove this property here. Instead, we’ll assume that it holds (and it does, we could prove it by induction too).

The above proof is one of the most basic examples of correctness proofs, but we did it by hand. Functional languages with dependent types make it possible to write such proofs as programs, which is even more impressive.

Let’s create a file `reverse-reverse.idr` for the Idris code. We’re not going to use the standard `reverse` function, so let’s hide it:

``%hide reverse``

Next, we can write the type of the `reverse` function:

``reverse : List a -> List a``

Functional languages like Idris are great for type-driven and incremental development, and the Idris mode for editors such as Emacs and Vim take full advantage of that.

If we place the cursor on top of `reverse` (the name of the function), we can make a new definition with `C-c C-s` for Emacs (or `\d` for Vim):

``````reverse : List a -> List a
reverse xs = ?reverse_rhs``````

This adds a line for the definition of `reverse` and a hole (`?reverse_rsh`) to fill with the actual definition. We can place the cursor on `xs` and split cases with `C-c C-c` (or `\c`):

``````reverse : List a -> List a
reverse [] = ?reverse_rhs_1
reverse (x :: xs) = ?reverse_rhs_2``````

We now have two equations for the definition of `reverse` and two holes to fill with appropriate definitions. After loading the file with `C-c C-l` (or `\r`), we can place the cursor on the `?reverse_rhs_1` hole and ask for its type with `C-c C-t` (or `\t`):

``````  a : Type
--------------------------------------
Main.reverse_rhs_1 : List a``````

The only thing we know is that `a` is a `Type` and we need to provide a value of type `List a`. The only option we have is to fill the hole with an empty list:

``````reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = ?reverse_rhs_2``````

We can now put the cursor over the `?reverse_rhs_2` hole and ask for its type:

``````  a : Type
x : a
xs : List a
--------------------------------------
Main.reverse_rhs_2 : List a``````

In this case, we have that `a` is a `Type`, `x` is a value of type `a`, `xs` is a list of elements of type `a`, and we need to provide a value of type `List a`. There’s more than one way to build such a list, but we already know the answer for reversing a list:

``````reverse : List a -> List a
reverse [] = []
reverse (x :: xs) = reverse xs ++ [x]``````

Since we have dependent types, we can define a new function for the proof that `reverse` is its own inverse:

``reverseReverse : (xs : List a) -> reverse (reverse xs) = xs``

Given a value `xs` of type `List a`, `reverseReverse xs` is a proof of the property that `reverse (reverse xs) = xs`. This is similar to what we did with Haskell, but at the type level – the `=` here is an actual data type representing equality.

Let’s make a new definition for `reverseReverse`:

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse xs = ?reverseReverse_rhs``````

And split cases for `xs`:

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = ?reverseReverse_rhs_1
reverseReverse (x :: xs) = ?reverseReverse_rhs_2``````

In the case of an empty list, this is the type of the hole:

``````  a : Type
--------------------------------------
Main.reverseReverse_rhs_1 : [] = []``````

We can prove that `[] = []` by reflexivity. Actually, we can place the cursor on the hole and tell Idris to search for a proof with `C-c C-a` (or `\o`). Idris will fill the hole with a `Refl`, which is the only constructor for the `=` type:

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) = ?reverseReverse_rhs_2``````

Let’s check the type of the second hole:

``````  a : Type
x : xs
xs : List a
--------------------------------------
Main.reverseReverse_rhs_2 : reverse (reverse xs ++ [x]) = x :: xs``````

We know that we need a proof of the property that `reverse` and `++` commute. This time, we can’t simply assume that it holds – we have to either prove it or postulate it if we want to use it. We should prove it, but let’s postulate it and focus on `reverseReverse`:

``````postulate
reverseAppend : (xs : List a) -> (ys : List a) ->
reverse (xs ++ ys) = reverse ys ++ reverse xs``````

We can `rewrite` the left-hand side of the goal using the `reverseAppend` property for `reverse xs` and `[x]`:

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in ?reverseReverse_rhs_2``````

Let’s ask for the type of the new hole:

``````  a : Type
x : xs
xs : List a
_rewrite_rule : x :: reverse (reverse xs) = reverse (reverse xs ++ [x])
--------------------------------------
Main.reverseReverse_rhs_2 : x :: reverse (reverse xs) = x :: xs``````

The type now includes a rewrite rule that explicitly tells us what was replaced in the previous step. The left-hand side of the new goal can be rewritten using the inductive hypothesis (that is, `reverseReverse xs`):

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in
rewrite reverseReverse xs in ?reverseReverse_rhs_2``````

Let’s ask for the type of the new hole:

``````  a : Type
x : xs
xs : List a
_rewrite_rule : x :: reverse (reverse xs) = reverse (reverse xs ++ [x])
_rewrite_rule1 : xs = reverse (reverse xs)
--------------------------------------
Main.reverseReverse_rhs_2 : x :: xs = x :: xs``````

The only thing remaining is to prove that `x :: xs = x :: xs`, which is true by reflexivity:

``````reverseReverse : (xs : List a) -> reverse (reverse xs) = xs
reverseReverse [] = Refl
reverseReverse (x :: xs) =
rewrite reverseAppend (reverse xs) [x] in
rewrite reverseReverse xs in Refl``````

“It type checks! Ship it!”

Many thanks to Eric Jones for the idea for this blog post.