Cannot prove merge sort with tree recursion

[WhiteBlackGoose]

Hello! I'm a newbie to F* and I'm trying to prove that my merge sorting function returns an actually sorted list.

Description

Merge

Here is the merge function.

let rec merge (a : list int) (b : list int)
    : c : list int { length c = length a + length b } =
    match a, b with
    | [], o | o, [] -> o
    | h1 :: t1, h2 :: t2 ->
        if h1 <= h2 then
            h1 :: merge t1 b
        else
            h2 :: merge a t2

Then I'm proving that this function returns a sorted list if the inputs are sorted:

let rec mergedCorrectly (l : list int) (r : list int)
    : Lemma (sorted l /\ sorted r ==> sorted (merge l r)) =
    match l, r with
    | [], _ | _, [] -> ()
    | h1 :: t1, h2 :: t2 ->
        mergedCorrectly t1 (h2 :: t2);
        mergedCorrectly (h1 :: t1) t2

Implementation of `length` and `sorted`

let rec length l : nat =
    match l with
    | [] -> 0
    | _ :: t -> 1 + length t

let rec sorted (l : list int) =
    match l with
    | [] | [ _ ] -> true
    | a :: b :: tl -> a <= b && sorted (b :: tl)

Split

So far it works great. Then I'm implementing split:

let rec split #a (s : list a) : x : (list a & list a) { length (fst x) + length (snd x) = length s } =
    match s with
    | [] -> [], []
    | h1 :: [] -> [ h1 ], []
    | h1 :: h2 :: [] -> [ h1 ], [ h2 ]
    | h1 :: h2 :: tl ->
        let (l, r) = split tl in
        h1 :: l, h2 :: r

Then I want to prove that if the input is at least 2 long, then both returned lists are shorter than the input

let splitLemma #a (s : list a)
    : Lemma (requires length s >= 2)
            (ensures length (fst (split s)) < length s /\ length (snd (split s)) < length s)
    = ()

Merge Sort

It works great so far. Now the actual function mergeSort:

let rec mergeSort (l : list int) : Tot (r : list int { length r = length l }) (decreases (length l)) =
    match l with
    | [] -> []
    | [ a ] -> [ a ]
    | [ a; b ] ->
        if a < b then [ a; b ]
        else [ b; a ]
    | other ->
        let (left, right) = split other in
        merge (mergeSort left) (mergeSort right

Finally I want to prove that it returns a sorted list.

let rec sortReturnsSorted (l : list int)
    : Lemma (ensures sorted (mergeSort l)) (decreases length l) =
    match l with
    | [] | [ _ ] | [ _; _ ] -> ()
    | other ->
        let (left, right) = split other in
        assert(length left < length other /\ length right < length other); 
        sortReturnsSorted (mergeSort left);
        sortReturnsSorted (mergeSort right);
        mergedCorrectly (mergeSort left) (mergeSort right);
        sortReturnsSorted (merge (mergeSort left) (mergeSort right))

... but it fails with this:

My logic

So here I'm using recursion over trees. And my idea is the following:

1. Prove the base case (this one works fine)
2. Take arbitrary list. If we split it, we get two strictly shorter lists. Why? Check the lemma we proved for split.
3. Assume they are sorted
4. Now, recall that their merge is sorted too. Why? We proved it in the lemma for merge.
5. We proved the induction step.

What have I done wrong? Here is the whole source file.

Thanks!

[TWal]

Hello!

Your call to sortReturnsSorted is wrong, here is how you should call them:

        sortReturnsSorted left;
        sortReturnsSorted right;

Otherwise in your current proof, what is proved by your recursive call is the fact sorted (sorted (mergeSort left)).

Another remark, which is more style-related: in your mergedCorrectly lemma, it is better to avoid using the implication ==> and use the requires / ensures construct. Like that, you won't be able to call this lemma if you can't prove that the input list aren't sorted!

[WhiteBlackGoose]

Thanks for the info! That's a good catch, I indeed don't need call of mergeSort there!
And after you said that I also realized I don't need

 sortReturnsSorted (merge (mergeSort left) (mergeSort right)

at all!

Thanks, it seems to be working! ^_^
Now I'm looking forward to see the slack link fixed and join your chat.

For completeness, working solution:

let rec sortReturnsSorted (l : list int)
    : Lemma (ensures sorted (mergeSort l)) (decreases length l) =
    match l with
    | [] | [ _ ] | [ _; _ ] -> ()
    | other ->
        let (left, right) = split other in
        assert(length left < length other /\ length right < length other); 
        sortReturnsSorted left;
        sortReturnsSorted right;
        mergedCorrectly (mergeSort left) (mergeSort right