trjhtr

I'm just starting to learn using both dependent types and proof assistants, and as an exercise I'm trying to write a provably correct merge sort. As a first step, I'm writing a function that merges two non-decreasing lists (this is easy) along with a proof that it produces a non-decreasing list (this is the hard part I'd like to have reviewed, along with the representation of non-decreasing lists).

The code below represents ordering criteria over type a as members of the Order a type. I'm deliberately not using Dec or Decidable.Order (since they seem to make my proof more clumsy), delegating proving the necessary properties of the comparator to the calling code and just requiring Totality instead, which is essentially the assumption that the order is total. Please let me know if this is a really, really bad idea!

I understand this is not sufficient to prove that a merge sort based on this merge function is indeed a sort, since a merge that, say, always returns an empty list or the first list, would still be provably mergeIsIncreasing, so another piece of the puzzle is proving that merge f xs ys is a permutation of xs ++ ys, but let's deal with non-decreasing part first.

I also understand that Increasing is not equal to NonDecreasing, but typing and abbreviating the latter is a pain in the fingers.

Other than that, stylistic comments, proof idea comments, whatever else comments are welcome!

import Data.So

%hide merge
%default total

Order : Type -> Type
Order a = a -> a -> Bool

Totality : Order a -> Type
Totality a f = x, y : a -> So (not (x `f` y)) -> So (y `f` x)

data Increasing : (f : Order a) -> (xs : List a) -> Type where
 EmptyInc : Increasing f 
 SingleInc : (x : a) -> Increasing f [x]
 RecInc : (f : Order a) -> (x0 : a) -> auto prf : So (x0 `f` x1) -> (rest : Increasing f (x1 :: xs)) -> Increasing f (x0 :: x1 :: xs)

%name Increasing xsinc, ysinc, zsinc


merge : (f : Order a) -> (xs : List a) -> (ys : List a) -> List a
merge f xs = xs
merge f ys = ys
merge f (x :: xs) (y :: ys) = case choose $ x `f` y of
 Left _ => x :: merge f xs (y :: ys)
 Right _ => y :: merge f (x :: xs) ys

mergeLeftEmptyId : (f : Order a) -> (ys : List a) -> merge f ys = ys
mergeLeftEmptyId f = Refl
mergeLeftEmptyId f (x :: xs) = Refl

mutual
 mergeIsIncreasing_single_x : (ftotal : Totality f) -> (x : a) -> (f_y_x : So (f y x)) -> (ysinc : Increasing f (y :: ys)) -> Increasing f (y :: (merge f [x] ys))
 mergeIsIncreasing_single_x f _ x f_y_x (SingleInc y) = RecInc f y (SingleInc x)
 mergeIsIncreasing_single_x f ys = y1 :: ys ftotal x f_y_x (RecInc f y0 yrest) with (mergeIsIncreasing ftotal (SingleInc x) yrest)
 | rest with (choose $ x `f` y1)
 | Left _ = RecInc f y0 rest
 | Right _ = RecInc f y0 rest

 mergeIsIncreasing_x0_leq_y : (x0_f_y : So (x0 `f` y)) -> (x0_f_x1 : So (x0 `f` x1)) -> (ftotal : Totality f) ->
 (xrest : Increasing f (x1 :: xs)) -> (ysinc : Increasing f (y :: ys)) -> Increasing f (x0 :: merge f (x1 :: xs) (y :: ys))
 mergeIsIncreasing_x0_leq_y f x1 y x0 x0_f_y x0_f_x1 ftotal xrest ysinc with (mergeIsIncreasing ftotal xrest ysinc)
 | rest with (choose $ x1 `f` y)
 | Left _ = RecInc f x0 rest
 | Right _ = RecInc f x0 rest

 mergeIsIncreasing_x0_geq_y : (y_f_x0 : So (y0 `f` x0)) -> (ftotal : Totality f) ->
 (xsinc : Increasing f (x0 :: xs)) -> (ysinc : Increasing f (y0 :: ys)) -> Increasing f (y0 :: merge f (x0 :: xs) ys)
 mergeIsIncreasing_x0_geq_y f y_f_x0 ftotal xsinc (SingleInc y0) = RecInc f y0 xsinc
 mergeIsIncreasing_x0_geq_y y_f_x0 x0 ftotal xsinc (RecInc prf x1 f y0 yrest) with (mergeIsIncreasing ftotal xsinc yrest)
 | rest with (choose $ x0 `f` x1)
 | Left _ = RecInc f y0 rest
 | Right _ = RecInc f y0 rest

 mergeIsIncreasing : ftotal : Totality f ->
 (xsinc : Increasing f xs) ->
 (ysinc : Increasing f ys) ->
 Increasing f (merge f xs ys)
 mergeIsIncreasing f xs = ys xsinc ysinc = rewrite mergeLeftEmptyId f ys in ysinc
 mergeIsIncreasing f xs ys = xsinc ysinc = xsinc

 mergeIsIncreasing f xs = [x] ys = y :: ys ftotal (SingleInc x) ysinc with (choose $ x `f` y)
 | Left _ = RecInc f x ysinc
 | Right not_f_x_y = mergeIsIncreasing_single_x ftotal x (ftotal not_f_x_y) ysinc

 mergeIsIncreasing f xs = x0 :: x1 :: xs ys = y :: ys ftotal (RecInc prf f x0 xrest) ysinc with (choose $ x0 `f` y)
 | Left x0_f_y = mergeIsIncreasing_x0_leq_y x0_f_y prf ftotal xrest ysinc
 | Right not_x0_f_y = mergeIsIncreasing_x0_geq_y (ftotal not_x0_f_y) ftotal (RecInc f x0 xrest) ysinc

and welcome to Code Review.

I'll be perfectly upfront here: your post 8 days ago was the first I had ever heard of idris. I was hoping that someone who knew it, or even knew a bit more Haskell, might be able to help, but as yet that hasn't happened. Anyway, I've had a few days to do my homework, but please don't take anything I say here without question.

The first thing I would point out is that the proof here is considerably longer than and harder to reason about than the merge function itself. That means that standard best practices to help readability apply double to the proof. Perhaps this is because I have a harder time than usual reading the language, but I think a few comments would be worth their weight in gold. Note down what base cases are; note where you're encoding the inductive hypothesis; perhaps expressly disambiguate between total functions (in %default total) and a total order (in Totality : Order a -> Type).

Another significant issue with code clarity is consistency. For example, sometimes you use infix notation for your comparison function f and sometimes you write it as (f y x). If those mean the same things, I don't especially care how you write them. Normal function order is more conventional, infix notation is more conventional for comparison operators specifically, there isn't much in it. But pick one.

Again on consistency, let's consider this block of code.

mergeLeftEmptyId : (f : Order a) -> (ys : List a) -> merge f ys = ys
mergeLeftEmptyId f = Refl
mergeLeftEmptyId f (x :: xs) = Refl

The first two lines are fine. The third one changes the variable name from ys to xs (or properly x :: xs). Such things are confusing, and made worse by the fact that xs is the name assigned to the other, empty list, parameter of merge.

(Incidentally, it bothers me that you have mergeLeftEmptyId and do not provide mergeRightEmptyId. Given that merge itself is so inherently symmetrical, I'd expect the proof to be likewise. Perhaps this is another point where a comment would be helpful to explain why the imbalance is needed.)

I'm not entirely comfortable by your definition of Totality. If I'm reading that right, you're requiring $ neg f(a,b) implies f(b,a) $, implicitly getting $ neg f(b,a) implies f(a,b) $ because variable names can be swapped around, and using that to define Comparability: that $ f(a,b) lor f(b,a) $. Don't get me wrong, that is a pretty neat trick. However, it took some serious figuring what you were going for. As above, clarity is king here. For comparison, it looks like idris itself used Either for the same effect in Decideable.Order.

In trying to learn from the idris source code (frustratingly I couldn't find evidence of this in the docs) about Decideable.Order I discovered that the Comparability property is required for anything to be Ordered, but it also depends on the properties of being a Poset which depends on Preorder. That is where it gets the other three properties needed for something to actually be a total order. As far as I can see, you don't define those properties, which is somewhat alarming for your argument.

For comparison the $ leq $ operation in Rock Paper Scissors has Comparability but it lacks Transitivity among other things. That's why you couldn't sort anything into rock paper scissors ordering.

As for the decision to not actually require your ordering properties in merge; that does seem a little weird. My understanding of the whole dependent types approach is that you encode your preconditions into the type system, essentially so that if your program could fail at run time then it won't even build.

Essentially what you have is a little better than conventional unit testing. After all, who writes unit tests that prove correctness for all valid inputs? And what testing library stops you at compile time if valid inputs give the wrong answer? Even so, this doesn't exploit the full power of this type system.

Your proof here may demonstrate that merge works as intended so long as your assumptions are met (sorted lists, total order comparison function) but doesn't actually enforce those assumptions. Nor does it seem to guarantee the post conditions: if you had say a binary search function that only operates on sorted lists, I expect the type system wouldn't know to let it build against the output of merge.

The proof itself has roughly the shape I would expect, excepting the special asymmetrically provided special cases for the left hand side. It covers both base cases with empty sets, and handles the inductive cases. I'm afraid I don't have the knowledge of the language particulars to provide a more detailed inspection.