## Sunday, May 21, 2017

### Proving fib equivalence

Summary: Using Idris I proved the exponential and linear time `fib` functions are equivalent.

The Haskell wiki proclaims that Implementing the Fibonacci sequence is considered the "Hello, world!" of Haskell programming. It also provides multiple versions of `fib` - an exponential version and a linear version. We can translate these into Idris fairly easily:

``````fibExp : Nat -> Nat
fibExp Z = 0
fibExp (S Z) = 1
fibExp (S (S n)) = fibExp (S n) + fibExp n

fibLin' : Nat -> Nat -> Nat -> Nat
fibLin' Z a b = b
fibLin' (S n) a b = fibLin' n (a + b) a

fibLin : Nat -> Nat
fibLin n = fibLin' n 1 0
``````

We've made the intermediate `go` function in `fibLin` top-level, named it `fibLib'` and untupled the accumulator - but it's still fundamentally the same. Now we've got the power of Idris, it would be nice to prove that `fibExp` and `fibLin` are equivalent. To do that, it's first useful to think about why `fibLib'` works at all. In essence we're decrementing the first argument, and making the next two arguments be `fib` of increasingly large values. If we think more carefully we can come up with the invariant:

``````fibLinInvariant : (d : Nat) -> (u : Nat) ->
fibLin' d (fibExp (1+u)) (fibExp u) = fibExp (d+u)
``````

Namely that at all recursive calls we must have the `fib` of two successive values (`u` and `u+1`), and after `d` additional loops we end up with `fib (d+u)`. Actually proving this invariant isn't too hard:

``````fibLinInvariant Z u = Refl
fibLinInvariant (S d) u =
rewrite fibLinInvariant d (S u) in
rewrite plusSuccRightSucc d u in
Refl
``````

Idris simplifies the base case away for us. For the recursive case we apply the induction hypothesis to leave us with:

``````fibExp (plus d (S u)) = fibExp (S (plus d u))
``````

Ignoring the `fibExp` we just need to prove `d+(u+1) = (d+u)+1`. That statement is obviously true because `+` is associative, but in our particular case, we use `plusSuccRightSucc` which is the associative lemma where `+1` is the special `S` constructor. After that, everything has been proven.

Armed with the fundamental correctness invariant for `fibLib`, we can prove the complete equivalence.

``````fibEq : (n : Nat) -> fibLin n = fibExp n
fibEq n =
rewrite fibLinInvariant n 0 in
rewrite plusZeroRightNeutral n in
Refl
``````

We appeal to the invariant linking `fibLin'` and `finExp`, do some minor arithmetic manipulation (`x+0 = x`), and are done. Note that depending on exactly how you define the `fibLinInvariant` you require different arithmetic lemmas, e.g. if you write `d+u` or `u+d`. Idris is equipped with everything required.

I was rather impressed that proving `fib` equivalence wasn't all that complicated, and really just requires figuring out what fundamental property makes `fibLin` actually work. In many ways the proof makes things clearer.

## Tuesday, May 16, 2017

### Idris reverse proofs

Summary: I proved O(n) reverse is equivalent to O(n^2) reverse.

Following on from my previous post I left the goal of given two `reverse` implementations:

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

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []
``````

Proving the following laws hold:

``````proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
``````

The complete proofs are available in my Idris github repo, and if you want to get the most out of the code, it's probably best to step through the types in Idris. In this post I'll talk through a few of the details.

Directly proving the `reverse1 (reverse1 x) = x` by induction is hard, since the function doesn't really follow so directly. Instead we need to define a helper lemma.

``````proof_reverse1_append : (xs : List a) -> (ys : List a) ->
reverse1 (xs ++ ys) = reverse1 ys ++ reverse1 xs
``````

Coming up with these helper lemmas is the magic of writing proofs - and is part intuition, part thinking about what might be useful and part thinking about what invariants are obeyed. With that lemma, you can prove by induction on the first argument (which is the obvious one to chose since `++` evaluates the first argument first). Proving the base case is trivial:

``````proof_reverse1_append [] ys =
rewrite appendNilRightNeutral (reverse1 ys) in
Refl
``````

The proof immediately reduces to `reverse1 ys == reverse1 ys ++ []` and we can invoke the standard proof that if `++` has `[]` on the right we can ignore it. After applying that rewrite, we're straight back to `Refl`.

The `::` is not really any harder, we immediately get to `reverse1 ys ++ (reverse1 xs ++ [x])`, but bracketed the wrong way round, so have to apply `appendAssociative` to rebracket so it fits the inductive lemma. The proof looks like:

``````proof_reverse1_append (x :: xs) ys =
rewrite appendAssociative (reverse1 ys) (reverse1 xs) [x] in
rewrite proof_reverse1_append xs ys in Refl
``````

Once we have the proof of how to move `reverse1` over `++` we use it inductively to prove the original lemma:

``````proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse1_reverse1 [] = Refl
proof_reverse1_reverse1 (x :: xs) =
rewrite proof_reverse1_append (reverse1 xs) [x] in
rewrite proof_reverse1_reverse1 xs in
Refl
``````

For the remaining two proofs, I first decided to prove `reverse1 x = reverse2 x` and then prove the `reverse2 (reverse2 x) = x` in terms of that. To prove equivalence of the two functions I first needed information about the fundamental property that `rev2` obeys:

``````proof_rev : (xs : List a) -> (ys : List a) ->
rev2 xs ys = reverse2 ys ++ xs
``````

Namely that the accumulator can be tacked on the end. The proof itself isn't very complicated, although it does require two calls to the inductive hypothesis (you basically expand out `rev2` on both sides and show they are equivalent):

``````proof_rev xs [] = Refl
proof_rev xs (y :: ys) =
rewrite proof_rev [y] ys in
rewrite sym \$ appendAssociative (rev2 [] ys) [y] xs in
rewrite proof_rev (y :: xs) ys in
Refl
``````

The only slight complexity is that I needed to apply `sym` to switch the way the `appendAssocative` proof is applied. With that proof available, proving equivalence isn't that hard:

``````proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
proof_reverse1_reverse2 [] = Refl
proof_reverse1_reverse2 (x :: xs) =
rewrite proof_rev [x] xs in
rewrite proof_reverse1_reverse2 xs in
Refl
``````

In essence the `proof_rev` term shows that `rev` behaves like the O(n^2) reverse.

Finally, actually proving that `reverse2 (reverse2 x)` is true just involves replacing all the occurrences of `reverse2` with `reverse1`, then applying the proof that the property holds for `reverse1`. Nothing complicated at all:

``````proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse2_reverse2 xs =
rewrite sym \$ proof_reverse1_reverse2 xs in
rewrite sym \$ proof_reverse1_reverse2 (reverse1 xs) in
rewrite proof_reverse1_reverse1 xs in
Refl
``````

If you've got this far and are still hungry for more proof exercises I recommend Exercises on Generalizing the Induction Hypothesis which I have now worked through (solutions if you want to cheat).

## Sunday, May 07, 2017

### Proving stuff with Idris

Summary: I've been learning Idris to play around with writing simple proofs. It seems pretty cool.

The Idris programming language is a lot like Haskell, but with quite a few cleanups (better export syntax, more though out type classes), and also dependent types. I'm not a massive fan of dependent types as commonly presented - I want to write my code so it's easy to prove, not intertwine my beautiful code with lots of invariants. To try out Idris I've been proving some lemmas about list functions. I'm very much an Idris beginner, but thought I would share what I've done so far, partly to teach, partly to remember, and party to get feedback/criticism about all the beginner mistakes I've made.

Before proving stuff, you need to write some definitions. Idris comes with an append function (named `++` as you might expect), but to keep everything simple and out in the open I've defined:

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

Coming from Haskell the only real difference is that cons is `::` and types are `:`. Given how Haskell code now looks, that's probably the right way around anyway. We can load that code in the Idris interactive environment and run it:

``````\$ idris Main.idr
Main> append [1,2] 
[1,2,3] : List Integer
``````

What we can also do, but can't easily do in Haskell, is start proving lemmas about it. We'd like to prove that `append xs [] = xs`, so we write a proof:

``````proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil xs = ?todo
``````

We name the proof `proof_append_nil` and then say that given `xs` (of type `List a`) we can prove that `append xs [] = xs`. That's pretty direct and simple. Now we have to write the proof - we first write out the definition leaving `?todo` where we want the proof to go. Now we can load the proof in Idris and type `:t todo` to get the bit of the proof that is required, and Idris says:

``````todo : append xs [] = xs
``````

That's fair - we haven't proven anything yet. Since we know the proof will proceed by splitting apart the `xs` we can rewrite as:

``````proof_append_nil [] = ?todo_nil
proof_append_nil (x :: xs) = ?todo_cons
``````

We can now ask for the types of the two remaining `todo` bits:

``````todo_nil : [] = []
todo_cons : x :: append xs [] = x :: xs
``````

The first `todo_nil` is obviously true since the things on either side of the equality match, so we can replace it with `Refl`. The second statement looks like the inductive case, so we want to apply `proof_append_nil` to it. We can do that with `rewrite proof_append_nil xs`, which expands to `append xs [] = xs`, and rewrites the left-hand-side of the proof to be more like the right. Refined, we end up with:

``````proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in ?todo_cons
``````

Reloading again and asking for the type of `todo_cons` we get:

``````todo_cons : x :: xs = x :: xs
``````

These things are equal, so we replace `todo_cons` with `Refl` to get a complete proof of:

``````proof_append_nil : (xs : List a) -> append xs [] = xs
proof_append_nil [] = Refl
proof_append_nil (x :: xs) = rewrite proof_append_nil xs in Refl
``````

Totality Checking

Proofs are only proofs if you have code that terminates. In Idris, seemingly sprinkling the statement:

``````%default total
``````

At the top of the file turns on the totality checker, which ensures the proof is really true. With the statement turned on I don't get any warnings about totality issues, so we have proved `append` really does have `[]` as a right-identity.

Avoiding rewrite

The `rewrite` keyword seems like a very big hammer, and in our case we know exactly where we want to apply the rewrite. Namely at the end. In this case we could have equally written:

``````cong (proof_append_nil xs)
``````

Not sure which would be generally preferred style in the Idris world, but as the proofs get more complex using `rewrite` certainly seems easier.

Coming from a Haskell background, and sticking to simple things, the main differences in Idris were that modules don't have export lists (yay), lists are `::` and types are `:` (yay), functions can only use functions defined before them (sad, but I guess a restriction to make dependent types work) and case/lambda both use `=>` instead of `->` (meh).

Next steps

For my first task in Idris I also defined two `reverse` functions:

``````reverse1 : List a -> List a
reverse1 [] = []
reverse1 (x :: xs) = reverse1 xs `append` [x]

rev2 : List a -> List a -> List a
rev2 acc [] = acc
rev2 acc (x :: xs) = rev2 (x :: acc) xs

reverse2 : List a -> List a
reverse2 = rev2 []
``````

The first `reverse1` function is `reverse` in O(n^2), the second is `reverse` in `O(n)`. I then tried to prove the three lemmas:

``````proof_reverse1_reverse1 : (xs : List a) -> xs = reverse1 (reverse1 xs)
proof_reverse2_reverse2 : (xs : List a) -> xs = reverse2 (reverse2 xs)
proof_reverse1_reverse2 : (xs : List a) -> reverse1 xs = reverse2 xs
``````

Namely that both `reverse1` and `reverse2` are self inverses, and then that they are equivalent. To prove these functions required a few helper lemmas, but only one additional Idris function/feature, namely:

``````sym : (left = right) -> right = left
``````

A function which transforms a proof of equality from one way around to the other way around. I also required a bunch of helper lemmas, including:

``````proof_append_assoc : (xs : List a) -> (ys : List a) -> (zs : List a) -> append xs (append ys zs) = append (append xs ys) zs
``````

Developing these proofs in Idris took me about ~2 hours, so were a nice introductory exercise (with the caveat that I've proven these lemmas before, although not in 4+ years). I'd invite anyone interested in learning this aspect of Idris to have a go, and I'll post my proofs sometime in the coming week.

Update: additional notes on this material can be found here from Reddit user chshersh.