I saw a challenge on Twitter from @arntzenius, in response to some discussion about the limits of dependent types.
Hey Agda fans! In the spirit of @Hillelogram's verification challenges: How would you prove that reversing an ascending list produces a descending one?
(Also accepting answers in other languages/systems.)
I thought this looked interesting, and Idris is my dependently typed language of choice, so I set about doing it.
%hide reverse
%default totalThese two list definitions are included because apparently my Idris is old, and has a less clear definition of reverse, but that also gives us a good excuse to see how it's implemented!
||| Reverse a list onto an existing tail.
reverseOnto : List a -> List a -> List a
reverseOnto acc [] = acc
reverseOnto acc (x::xs) = reverseOnto (x::acc) xs
||| Return the elements of a list in reverse order.
reverse : List a -> List a
reverse = reverseOnto []If a list is in increasing order, that's saying that for each pair of elements x and y, we have x < y.
Making it in decreasing order tells you that x > y.
The more general principle at work here is that if some relation R holds (so R x y), then in the reverse, sym R will hold (so (sym R) x y).
Therefore, let's define a type for relations.
We use the encoding a -> a -> Type, so for some type R : Rel a, an element of R x y is a proof that the relation holds for those two elements.
||| A shorthand for binary relations over a type a.
Rel : Type -> Type
Rel a = a -> a -> Type
||| Produces the symmetric relation, R x y <=> (sym R) y x.
sym : Rel a -> Rel a
sym x l r = x r lNext, we want a way to say that some list respects a given relation pairwise.
Here we define a type HasProp that represents a proof of that fact.
Because I want to be cute, I'm using the names (::) and Nil, so these proofs will use the list notation, where each element of the list is a proof that the respective pair obeys the relation.
By the definition here, there's no constructors that let you build one on the empty list.
We could add another constructor for the empty list, but doing it this way allows us to also index the type by the value of the final element in the list, which will be useful later on for letting us append these proofs.
||| Encodes that a non-empty list obeys some relation pairwise.
data HasProp : (r : Rel a) -> List a -> a -> Type where
(::) : r x y -> HasProp r (y::ys) l -> HasProp r (x::y::ys) l
||| A list with one element trivially has the property.
Nil : HasProp r [x] xThese tests demonstrate the proof objects.
I didn't actually have to write out the bodies, simply putting ?test and asking Idris's proof search to fill in the body for me was able to discover the proofs automatically.
test1 : HasProp LT [1, 2, 3, 4] 4
test1 = [LTESucc (LTESucc LTEZero),
LTESucc (LTESucc (LTESucc LTEZero)),
LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))]
test2 : HasProp (=) [2, 1 + 1, 2 - 0] 2
test2 = [Refl, Refl]
test3 : HasProp (sym LT) (reverse [1, 2, 3, 4]) 1
test3 = [LTESucc (LTESucc (LTESucc (LTESucc LTEZero))),
LTESucc (LTESucc (LTESucc LTEZero)),
LTESucc (LTESucc LTEZero)]Now we get into the mechanics of our proofs.
First, we have a lemma that proves that reverseOnto matches the naive implementation of reverse, we use this later to help prove our final goal.
||| Proves that reverseOnto matches the naive implementation of reverse.
reverse_onto_append : (acc, xs : List a) -> reverseOnto acc xs = reverse xs ++ acc
reverse_onto_append acc [] = Refl
reverse_onto_append [] xs =
rewrite appendNilRightNeutral (reverse xs) in
Refl
reverse_onto_append (y :: ys) (x :: xs) =
rewrite reverse_onto_append (x :: y :: ys) xs in
rewrite reverse_onto_append [x] xs in
rewrite appendAssociative (reverse xs) [x] (y :: ys) in
ReflNext, we define a function that allows us to append two HasProp proofs.
The first input makes use of the "final" element, proving that the two lists will happily fit together.
The recursive case matches basically what a normal list append does, and when we get to the empty list, we insert the bridge proof, reflecting the fact that the HasProp contains one proof in between each list element, rather than one for each list element.
||| Appends two HasProp proofs.
appendProp : r l y -> HasProp r xs l -> HasProp r (y :: ys) l' -> HasProp r (xs ++ y :: ys) l'
appendProp p (x :: xs) ys = x :: appendProp p xs ys
appendProp p [] ys = p :: ysAs our culminating proof, we prove that reversing a list will make it obey the symmetric relation.
The key insight here was realizing that we needed 3 cases, an empty base case and a base case that holds one single proof.
In order to handle the appending, we'd like to be able to move over an entire pair at a time.
To do that, we rewrite the reverse to look like reverse (y :: xs) ++ [x, z], and then use appendProp to match the same structure.
This proves the essential property that we were interested in.
||| Proves that a reversing a list that respects a given relation will respect
||| the symmetric relation.
reverse_sym_prop : (x : a) -> (xs : List a)
-> HasProp r (x :: xs) l
-> HasProp (sym r) (reverse (x :: xs)) x
reverse_sym_prop z [] _ = []
reverse_sym_prop {r=r} {l=x} z (x :: []) (p :: []) = [p]
reverse_sym_prop {r=r} {l=l} z (x :: (y :: xs)) (p :: (q :: ps)) =
rewrite reverse_onto_append [x, z] (y :: xs) in
appendProp q (reverse_sym_prop y xs ps) [p]And finally, as an anticlimactic encore, reversing an empty list gives an empty list. I'm satisfied that all our theorems hold vacuously for empty lists, so I'm not going to prove anything else about it.
reverse_empty : reverse [] = []
reverse_empty = ReflOne potential improvement here would be extending HasProp to support empty lists, so that we don't have to view these in empty/nonempty cases.
That would require making the type of appendProp much more complicated, and I'm not interested in doing those final steps at the moment.