Reverse, Reverse: Theorem Proving with Idris

Constructors are red.
Types are blue.
Your code always works
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.

For more information about Idris and complete tutorials, see Idris and the Idris documentation.

All the quotes in this blog post were taken from the Idris mode for Emacs.