Can I use lemmas for constraining types for initial functions?

[WhiteBlackGoose]

So, assume I have function mergeSort:

let rec mergeSort (l : list int) : list int

In a separate lemma I prove that for the returned list it is true that it is sorted:

let rec sortReturnsSorted (l : list int) : Lemma (ensures sorted (mergeSort l))

Now, can I use this lemma to change the initial function to

let rec mergeSort (l : list int) : (r : list int { sorted r })

?

[TheoWinterhalter]

Yes, you can simply define it to be the other mergeSort and use the lemma to conclude:

assume val _mergeSort (l : list int) : list int

let cmp (x y : int) = x < y

assume val sortReturnsSorted (l : list int) : Lemma (sorted cmp (_mergeSort l))

let mergeSort (l : list int) : (r : list int { sorted cmp r }) =
  sortReturnsSorted l ;
  _mergeSort l

[WhiteBlackGoose]

Oh right, haha! This worked:

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)


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)

let mergeSort (l : list int) : (r : list int { sorted r }) =
    sortReturnsSorted l;
    _mergeSort l

May I ask why you have assume there?

[TheoWinterhalter]

I simply did that to test. assume val means I do not have to provide a definition.

[WhiteBlackGoose]

Ah. Thanks!