mergesort_list.mlw 9.13 KB
 Jean-Christophe Filliatre committed Apr 03, 2011 1 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 2 ``````(** {1 Sorting lists using mergesort} `````` Jean-Christophe Filliatre committed Mar 29, 2014 3 4 5 `````` Author: Jean-Christophe Filliâtre (CNRS) *) `````` Jean-Christophe Filliatre committed Apr 03, 2011 6 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 7 ``````module Elt `````` 8 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 9 10 11 12 `````` use export int.Int use export list.Length use export list.Append use export list.Permut `````` 13 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 14 15 16 17 18 19 20 `````` type elt predicate le elt elt clone relations.TotalPreOrder with type t = elt, predicate rel = le clone export list.Sorted with type t = elt, predicate le = le end `````` Jean-Christophe Filliatre committed Apr 01, 2014 21 22 ``````(** recursive (and naive) merging of two sorted lists *) `````` Jean-Christophe Filliatre committed Mar 29, 2014 23 ``````module Merge (* : MergeSpec *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 24 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2014 25 `````` clone export Elt `````` Jean-Christophe Filliatre committed Mar 28, 2014 26 27 28 `````` let rec merge (l1 l2: list elt) : list elt requires { sorted l1 /\ sorted l2 } `````` Jean-Christophe Filliatre committed Mar 29, 2014 29 30 `````` ensures { sorted result } ensures { permut result (l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 31 32 33 34 35 36 37 38 39 40 `````` 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 `````` Jean-Christophe Filliatre committed Mar 29, 2014 41 ``````(** tail recursive implementation *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 42 `````` `````` Jean-Christophe Filliatre committed Mar 29, 2014 43 44 45 ``````module EfficientMerge (* : MergeSpec *) clone export Elt `````` Jean-Christophe Filliatre committed Mar 28, 2014 46 47 48 49 `````` use import list.Mem use import list.Reverse use import list.RevAppend `````` Jean-Christophe Filliatre committed Mar 29, 2014 50 51 52 53 `````` lemma sorted_reverse_cons: forall acc x1. sorted (reverse acc) -> (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc)) `````` Jean-Christophe Filliatre committed Mar 28, 2014 54 55 56 57 `````` 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 } `````` Jean-Christophe Filliatre committed Mar 29, 2014 58 59 `````` ensures { sorted result } ensures { permut result (acc ++ l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 `````` 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 77 78 79 80 81 82 ``````(** Mergesort. This implementation splits the input list in two according to even- and odd-order elements (see function [split] below). Thus it is not stable. For a stable implementation, see below module [OCamlMergesort]. *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 83 84 ``````module Mergesort `````` Jean-Christophe Filliatre committed Apr 01, 2014 85 `````` clone import Merge (* or EfficientMerge *) `````` Jean-Christophe Filliatre committed Mar 28, 2014 86 87 `````` let split (l0: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 88 `````` requires { length l0 >= 2 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 89 `````` ensures { let (l1, l2) = result in `````` Andrei Paskevich committed Oct 13, 2012 90 `````` 1 <= length l1 /\ 1 <= length l2 /\ permut l0 (l1 ++ l2) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 91 `````` = let rec split_aux (l1 l2 l: list 'a) : (list 'a, list 'a) `````` Andrei Paskevich committed Oct 13, 2012 92 `````` requires { length l2 = length l1 \/ length l2 = length l1 + 1 } `````` Jean-Christophe Filliatre committed Mar 28, 2014 93 `````` ensures { let r1, r2 = result in `````` Andrei Paskevich committed Oct 13, 2012 94 95 `````` (length r2 = length r1 \/ length r2 = length r1 + 1) /\ permut (r1 ++ r2) (l1 ++ (l2 ++ l)) } `````` Jean-Christophe Filliatre committed Mar 28, 2014 96 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 97 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 98 99 100 101 102 `````` | Nil -> (l1, l2) | Cons x r -> split_aux l2 (Cons x l1) r end in split_aux Nil Nil l0 `````` Jean-Christophe Filliatre committed May 20, 2011 103 `````` `````` Jean-Christophe Filliatre committed Mar 28, 2014 104 `````` let rec mergesort (l: list elt) : list elt `````` Andrei Paskevich committed Oct 13, 2012 105 `````` ensures { sorted result /\ permut result l } `````` Jean-Christophe Filliatre committed Mar 28, 2014 106 `````` variant { length l } `````` Andrei Paskevich committed Oct 13, 2012 107 `````` = match l with `````` Jean-Christophe Filliatre committed Apr 03, 2011 108 109 `````` | Nil | Cons _ Nil -> l | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2) `````` 110 111 `````` end `````` Jean-Christophe Filliatre committed Dec 29, 2010 112 ``````end `````` Jean-Christophe Filliatre committed Mar 31, 2014 113 `````` `````` Jean-Christophe Filliatre committed Apr 01, 2014 114 115 ``````(** {2 OCaml's List.sort} `````` Jean-Christophe Filliatre committed Apr 01, 2014 116 117 118 119 120 121 122 123 124 125 126 127 128 `````` 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 sort in order and in reverse order ([sort] and [sort_rev]) and merge is duplicated as well ([rev_merge] and [rev_merge_rev]). Note: this is a stable sort, but stability is not proved here. `````` Jean-Christophe Filliatre committed Apr 01, 2014 129 130 ``````*) `````` Jean-Christophe Filliatre committed Mar 31, 2014 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 ``````module OCamlMergesort clone export Elt use import list.Mem use import list.Reverse use import list.RevAppend 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 163 164 165 `````` lemma sorted_reverse_mem: forall x l. sorted (reverse (Cons x l)) -> forall y. mem y l -> le y x `````` Jean-Christophe Filliatre committed Mar 31, 2014 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 `````` 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 184 185 186 187 188 189 190 191 `````` 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) `````` Jean-Christophe Filliatre committed Apr 01, 2014 192 193 194 195 196 197 198 199 200 201 202 203 `````` 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 204 205 206 207 208 209 210 211 212 213 214 `````` 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 `````` Jean-Christophe Filliatre committed Apr 01, 2014 215 216 217 218 219 220 `````` (** [sort n l] sorts [prefix n l] and [rev_sort n l] sorts [prefix n l] in reverse order. *) use import mach.int.Int let rec sort (n: int) (l: list elt) : list elt `````` Jean-Christophe Filliatre committed Mar 31, 2014 221 222 223 `````` requires { 2 <= n <= length l } ensures { sorted result } ensures { permut result (prefix n l) } `````` Jean-Christophe Filliatre committed Apr 01, 2014 224 225 226 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 `````` 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 `````` Jean-Christophe Filliatre committed Mar 31, 2014 282 283 284 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 if n < 2 then l else sort n l end``````