permutations (bubble sort in agda, pt 2)

(following from part 1)

I implemented bubblesort in Agda, and it looks bug-free. But I want to prove that it is correct. First I want to prove that the output is a permutation of the input. I'm not going to try proving anything about the ordering yet, but I want to know that at least I'm getting back the same list, rearranged.

This is where Agda starts getting really hard for me, and becomes more like stuff I did in my maths degree courses than stuff I've done with hobby computer hacking. Except you can't write "clearly, .... is true" in your Agda programs like you could in your maths homework, so you don't get to bluff your way through proofs quite so easily.

The previous post showed how you could augment the datatypes of the functions in your program to carry more information about how those functions behave. That's one way of using dependent types. In this post, I'm going to use a different style to prove that the output of bubblesort is a permutation.

The Curry-Howard isomorphism which (for the purposes of this post) says (for the purposes of this post) that you can regard propositions as types, and proofs of those propositions as values in those types.

So you define a type to represent whatever proposition it is you want to prove, and then you write a function that creates a value of that type - that value is then a proof of the proposition. When you use values normally, you care what that value is. When you use proofs though, you don't care so much what the proof is. You just care that the proof exists.

First I need to make a definition of what I mean by permutation. There are a few different ways I could have done this. I ended up settling on this one:

data SwapBasedPermutation {A : Set} : {n : ℕ} -> (Vec A n) -> (Vec A n) -> Set where

    reflexivity : {n : ℕ} -> (i : Vec A n) -> SwapBasedPermutation i i

    transitivity : {n : ℕ} -> {a : Vec A n} -> {b : Vec A n} -> {c : Vec A n} -> (SwapBasedPermutation a b) -> (SwapBasedPermutation b c) -> SwapBasedPermutation a c

    prepend : {pn : ℕ} -> {l r : Vec A pn } -> (e : A) -> (SwapBasedPermutation l r) -> SwapBasedPermutation (e :: l) (e :: r)

    swapheads : {pn : ℕ} -> {first second : A} -> {rest : Vec A pn} -> SwapBasedPermutation ( first :: second :: rest ) ( second :: first :: rest)

My permutations are swap-based. Given a list, you can swap the first two elements (using the swapheads constructor, and you get a proof that the first list (but only the first two elements, not some arbitrary pair of elements) is a permutation of the second; and given two lists that are permutations of each other, you can add the same element onto the front of both, and you get a proof that those two new lists will be permutations of each other (using the prepend constructor).

I also declare that permutations are reflexive and transitivitive by definition (although I think I could build those up from more fundamental parts, but I'm more interested in looking at the higher level behaviour of bubblesort).

Those are proofs-by-definition and so they are trivially true (at least as far as the type-checker is concerned).

Now given this SwapBasedPermutation type, I can write a theorem that the top level sortlist function (defined in my previous post) outputs a permutation of its input.

The theorem is a type signature for a function, and body of the function needs to generate a proof of that theorem:

The type signature for my theorem looks like this:

sortlist-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (sortlist l)

It says: for all ℕumbers n: for all Vectors l of length n: l is a permutation of sortlist l.

If we can write a definition for this function that typechecks correctly, then this theorem holds. We never actually need to invoke the function at runtime - it is enough to know that we could. (That's another thing thats a bit weird in Agda- you're writing functions that will never be called at runtime but they're still useful. I guess its like writing javadocs...)

Here its important that Agda functions are total - we need to know that our proof generating function really will return a value and not loop forever or error out. Otherwise, our theorem could typecheck but not really be proved.

Now that we've stated the theorem (as a type), we need to build the body (the proof).

To get there, we can define lemmas, in the same way that you can define helper functions to help implement your main function.

First, invoking onepass on a list permutes that list. onepass is the code in my implementation that actually re-orders the list, so the proof of this lemma makes use of the swaphead definition. It also recursively calls itself on a smaller list - that means we're using proof by induction. This definition roughly follows the shape of the definition of onepass itself.

lemma-onepass-permutes : {n : ℕ} -> (l : Vec ℕ n) -> SwapBasedPermutation l (onepass l)
  lemma-onepass-permutes [] = reflexivity []
  lemma-onepass-permutes (e :: []) = reflexivity (e :: [])
  lemma-onepass-permutes (y :: y' :: rest) with  y ≤? y'
  ... | yes _ = prepend y (lemma-onepass-permutes (y' :: rest))
  ... | no _ = let                      
       p1 = lemma-onepass-permutes (y :: rest)                              
       p2 = prepend y' p1
       p3 = swapheads -- magically the list that we're swapping the             
                      -- heads for is inferred (from use in p4)                 
       p4 = transitivity p3 p2
    in p4

Another lemma, this time about the behaviour of innersort:

lemma-innersort-permutes : {vn : ℕ } -> (sn : ℕ) -> (l : Vec ℕ vn) -> SwapBasedPermutation l (innersort sn l)
  lemma-innersort-permutes zero l = reflexivity l
  lemma-innersort-permutes (suc sm) l = let
             a = lemma-onepass-permutes l
                  -- this shows l is a permutation of onepass l                                  
             b = lemma-innersort-permutes sm (onepass l)
                  -- this shows that (onepass l) is a permutation of (innersort sm (onepass l))               
          in transitivity a b

and finally we can give our definition for our theorem, sortlist-permutes, using these lemmas:

sortlist-permutes {n} l = lemma-innersort-permutes  n l

And now, because sortlist-permutes typechecks correctly at compile time, I know that I can generate a proof that sortlist really does permute a list, no matter what list I give it.

Tada!

Except this doesn't actually typecheck in Agda due to a problem with my definition of onepass... see the next post.