mergesort_list.mlw 9.3 KB
Newer Older
1

2
(** {1 Sorting lists using mergesort}
3 4 5

    Author: Jean-Christophe Filliâtre (CNRS)
*)
6

7
module Elt
8

9
  use export int.Int
10
  use export list.List
11 12 13
  use export list.Length
  use export list.Append
  use export list.Permut
14

15
  type elt
16
  val predicate le elt elt
17
  clone relations.TotalPreOrder
18 19 20
    with type t = elt, predicate rel = le, axiom .
  clone export list.Sorted with
    type t = elt, predicate le  = le, goal Transitive.Trans
21 22 23

end

24 25
(** recursive (and naive) merging of two sorted lists *)

26
module Merge (* : MergeSpec *)
27

28
  clone export Elt with axiom .
29 30 31

  let rec merge (l1 l2: list elt) : list elt
    requires { sorted l1 /\ sorted l2 }
32 33
    ensures  { sorted result }
    ensures  { permut result (l1 ++ l2) }
34 35 36 37 38 39 40 41 42 43
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> l2
    | _, Nil -> l1
    | Cons x1 r1, Cons x2 r2 ->
       if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
    end

end

44
(** tail recursive implementation *)
45

46 47
module EfficientMerge (* : MergeSpec *)

48
  clone export Elt with axiom .
49 50 51
  use list.Mem
  use list.Reverse
  use list.RevAppend
52

53 54 55 56
  lemma sorted_reverse_cons:
    forall acc x1. sorted (reverse acc) ->
    (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))

57 58 59 60
  let rec merge_aux (acc l1 l2: list elt) : list elt
    requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 }
    requires { forall x y: elt. mem x acc -> mem y l1 -> le x y }
    requires { forall x y: elt. mem x acc -> mem y l2 -> le x y }
61 62
    ensures  { sorted result }
    ensures  { permut result (acc ++ l1 ++ l2) }
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append acc l2
    | _, Nil -> rev_append acc l1
    | Cons x1 r1, Cons x2 r2 ->
       if le x1 x2 then merge_aux (Cons x1 acc) r1 l2
                   else merge_aux (Cons x2 acc) l1 r2
    end

  let merge (l1 l2: list elt) : list elt
    requires { sorted l1 /\ sorted l2 }
    ensures  { sorted result /\ permut result (l1 ++ l2) }
  =
    merge_aux Nil l1 l2

end

80 81 82
(** Mergesort.

    This implementation splits the input list in two according to even- and
83 84
    odd-order elements (see function `split` below). Thus it is not stable.
    For a stable implementation, see below module `OCamlMergesort`. *)
85

86 87
module Mergesort

88
  clone Merge (* or EfficientMerge *) with axiom .
89 90

  let split (l0: list 'a) : (list 'a, list 'a)
91
    requires { length l0 >= 2 }
92
    ensures  { let l1, l2 = result in
93
      1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) }
94
  = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a)
95
      requires { length l2 = length l1 \/ length l2 = length l1 + 1 }
96
      ensures  { let r1, r2 = result in
97 98
        (length r2 = length r1 \/ length r2 = length r1 + 1) /\
        permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
99
      variant { length l }
100
    = match l with
101
      | Nil -> l1, l2
102 103 104 105
      | Cons x r -> split_aux l2 (Cons x l1) r
      end
    in
    split_aux Nil Nil l0
106

107
  let rec mergesort (l: list elt) : list elt
108
    ensures { sorted result /\ permut result l }
109
    variant { length l }
110
  = match l with
111 112
      | Nil | Cons _ Nil -> l
      | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
113 114
    end

115
end
116

117 118
(** {2 OCaml's List.sort}

119 120 121 122 123 124 125 126 127
    There are several ideas here:

    - instead of splitting the list in two, sort takes the length of
      the prefix to be sorted; hence there is nothing to do to get the
      first half and the second half is obtained with chop (which does
      not allocate at all)

    - all functions are tail recursive. To avoid the extra cost of
      List.rev, sort is duplicated in two versions that respectively
128 129
      sort in order and in reverse order (`sort` and `sort_rev`) and
      merge is duplicated as well (`rev_merge` and `rev_merge_rev`).
130 131

    Note: this is a stable sort, but stability is not proved here.
132 133
*)

134 135
module OCamlMergesort

136
  clone export Elt with axiom .
137 138 139
  use list.Mem
  use list.Reverse
  use list.RevAppend
140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165

  lemma sorted_reverse_cons:
    forall acc x1. sorted (reverse acc) ->
    (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))

  lemma sorted_rev_append: forall acc l: list elt.
    sorted (reverse acc) ->
    sorted l ->
    (forall x y. mem x acc -> mem y l -> le x y) ->
    sorted (reverse (rev_append l acc))

  let rec rev_merge (l1 l2 accu: list elt) : list elt
    requires { sorted (reverse accu) /\ sorted l1 /\ sorted l2 }
    requires { forall x y: elt. mem x accu -> mem y l1 -> le x y }
    requires { forall x y: elt. mem x accu -> mem y l2 -> le x y }
    ensures  { sorted (reverse result) }
    ensures  { permut result (accu ++ l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append l2 accu
    | _, Nil -> rev_append l1 accu
    | Cons h1 t1, Cons h2 t2 ->
       if le h1 h2 then rev_merge t1 l2 (Cons h1 accu)
                   else rev_merge l1 t2 (Cons h2 accu)
    end

166 167 168
  lemma sorted_reverse_mem:
    forall x l. sorted (reverse (Cons x l)) -> forall y. mem y l -> le y x

169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186
  lemma sorted_reverse_cons2:
    forall x l. sorted (reverse (Cons x l)) -> sorted (reverse l)

  let rec rev_merge_rev (l1 l2 accu: list elt) : list elt
    requires { sorted accu /\ sorted (reverse l1) /\ sorted (reverse l2) }
    requires { forall x y: elt. mem x accu -> mem y l1 -> le y x }
    requires { forall x y: elt. mem x accu -> mem y l2 -> le y x }
    ensures  { sorted result }
    ensures  { permut result (accu ++ l1 ++ l2) }
    variant  { length l1 + length l2 }
  = match l1, l2 with
    | Nil, _ -> rev_append l2 accu
    | _, Nil -> rev_append l1 accu
    | Cons h1 t1, Cons h2 t2 ->
       if not (le h1 h2) then rev_merge_rev t1 l2 (Cons h1 accu)
                         else rev_merge_rev l1 t2 (Cons h2 accu)
    end

187 188 189 190 191 192 193 194
  function prefix int (list 'a) : list 'a

  axiom prefix_def1:
    forall l: list 'a. prefix 0 l = Nil
  axiom prefix_def2:
    forall n: int, x: 'a, l: list 'a. n > 0 ->
    prefix n (Cons x l) = Cons x (prefix (n-1) l)

195 196 197 198 199 200 201 202 203 204 205 206
  let rec lemma prefix_length (n: int) (l: list 'a)
    requires { 0 <= n <= length l } ensures { length (prefix n l) = n }
    variant { n } =
    if n > 0 then match l with Nil -> () | Cons _ r -> prefix_length (n-1) r end

  let rec lemma prefix_append (n: int) (l1 l2: list 'a)
    requires { length l1 <= n <= length l1 + length l2 }
    ensures  { prefix n (l1 ++ l2) =
               prefix (length l1) l1 ++ prefix (n - length l1) l2 }
    variant  { l1 }
  = match l1 with Nil -> () | Cons _ t -> prefix_append (n-1) t l2 end

207 208 209 210 211 212 213 214 215 216 217
  let rec chop (n: int) (l: list 'a) : list 'a
    requires { 0 <= n <= length l }
    ensures  { l = prefix n l ++ result }
    variant  { n }
  =
    if n = 0 then l else
    match l with
      | Cons _ t -> chop (n-1) t
      | Nil -> absurd
    end

218 219
  (** `sort n l` sorts `prefix n l`
      and `rev_sort n l`  sorts `prefix n l` in reverse order. *)
220

221
  use mach.int.Int
222 223

  let rec sort (n: int) (l: list elt) : list elt
224 225 226
    requires { 2 <= n <= length l }
    ensures  { sorted result }
    ensures  { permut result (prefix n l) }
227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284
    variant  { n }
  =
    if n = 2 then match l with
      | Cons x1 (Cons x2 _) ->
          if le x1 x2 then Cons x1 (Cons x2 Nil) else Cons x2 (Cons x1 Nil)
      | _ -> absurd
    end else if n = 3 then match l with
      | Cons x1 (Cons x2 (Cons x3 _)) ->
           if le x1 x2 then
             if le x2 x3 then Cons x1 (Cons x2 (Cons x3 Nil))
             else if le x1 x3 then Cons x1 (Cons x3 (Cons x2 Nil))
             else Cons x3 (Cons x1 (Cons x2 Nil))
           else
             if le x1 x3 then Cons x2 (Cons x1 (Cons x3 Nil))
             else if le x2 x3 then Cons x2 (Cons x3 (Cons x1 Nil))
             else Cons x3 (Cons x2 (Cons x1 Nil))
       | _ -> absurd
    end else begin
      let n1 = n / 2 in
      let n2 = n - n1 in
      let l2 = chop n1 l in
      assert { prefix n1 l ++ prefix n2 l2 = prefix n l };
      let s1 = rev_sort n1 l in
      let s2 = rev_sort n2 l2 in
      rev_merge_rev s1 s2 Nil
   end

  with rev_sort (n: int) (l: list elt) : list elt
    requires { 2 <= n <= length l }
    ensures  { sorted (reverse result) }
    ensures  { permut result (prefix n l) }
    variant  { n }
  =
    if n = 2 then match l with
      | Cons x1 (Cons x2 _) ->
          if not (le x1 x2) then Cons x1 (Cons x2 Nil)
          else Cons x2 (Cons x1 Nil)
      | _ -> absurd
    end else if n = 3 then match l with
      | Cons x1 (Cons x2 (Cons x3 _)) ->
           if not (le x1 x2) then
             if not (le x2 x3) then Cons x1 (Cons x2 (Cons x3 Nil))
             else if not (le x1 x3) then Cons x1 (Cons x3 (Cons x2 Nil))
             else Cons x3 (Cons x1 (Cons x2 Nil))
           else
             if not (le x1 x3) then Cons x2 (Cons x1 (Cons x3 Nil))
             else if not (le x2 x3) then Cons x2 (Cons x3 (Cons x1 Nil))
             else Cons x3 (Cons x2 (Cons x1 Nil))
       | _ -> absurd
    end else begin
      let n1 = n / 2 in
      let n2 = n - n1 in
      let l2 = chop n1 l in
      assert { prefix n1 l ++ prefix n2 l2 = prefix n l };
      let s1 = sort n1 l in
      let s2 = sort n2 l2 in
      rev_merge s1 s2 Nil
    end
285 286 287 288 289 290 291

  lemma permut_prefix: forall l: list elt. permut (prefix (length l) l) l

  let mergesort (l: list elt) : list elt
    ensures { sorted result /\ permut result l }
  =
    let n = length l in
Mário Pereira's avatar
Mário Pereira committed
292 293 294 295
    if n < 2 then begin
      assert { sorted l by match l with
               Nil | Cons _ Nil -> sorted l | _ -> false end }; l end
    else sort n l
296 297

end