examples/mergesort_list.mlw

   1
   2 (** {1 Sorting lists using mergesort}
   3
   4     Author: Jean-Christophe Filliâtre (CNRS)
   5 *)
   6
   7 module Elt
   8
   9   use export int.Int
  10   use export list.List
  11   use export list.Length
  12   use export list.Append
  13   use export list.Permut
  14
  15   type elt
  16   val predicate le elt elt
  17   clone relations.TotalPreOrder
  18     with type t = elt, predicate rel = le, axiom .
  19   clone export list.Sorted with
  20     type t = elt, predicate le  = le, goal Transitive.Trans
  21
  22 end
  23
  24 (** recursive (and naive) merging of two sorted lists *)
  25
  26 module Merge (* : MergeSpec *)
  27
  28   clone export Elt with axiom .
  29
  30   let rec merge (l1 l2: list elt) : list elt
  31     requires { sorted l1 /\ sorted l2 }
  32     ensures  { sorted result }
  33     ensures  { permut result (l1 ++ l2) }
  34     variant  { length l1 + length l2 }
  35   = match l1, l2 with
  36     | Nil, _ -> l2
  37     | _, Nil -> l1
  38     | Cons x1 r1, Cons x2 r2 ->
  39        if le x1 x2 then Cons x1 (merge r1 l2) else Cons x2 (merge l1 r2)
  40     end
  41
  42 end
  43
  44 (** tail recursive implementation *)
  45
  46 module EfficientMerge (* : MergeSpec *)
  47
  48   clone export Elt with axiom .
  49   use list.Mem
  50   use list.Reverse
  51   use list.RevAppend
  52
  53   lemma sorted_reverse_cons:
  54     forall acc x1. sorted (reverse acc) ->
  55     (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))
  56
  57   let rec merge_aux (acc l1 l2: list elt) : list elt
  58     requires { sorted (reverse acc) /\ sorted l1 /\ sorted l2 }
  59     requires { forall x y: elt. mem x acc -> mem y l1 -> le x y }
  60     requires { forall x y: elt. mem x acc -> mem y l2 -> le x y }
  61     ensures  { sorted result }
  62     ensures  { permut result (acc ++ l1 ++ l2) }
  63     variant  { length l1 + length l2 }
  64   = match l1, l2 with
  65     | Nil, _ -> rev_append acc l2
  66     | _, Nil -> rev_append acc l1
  67     | Cons x1 r1, Cons x2 r2 ->
  68        if le x1 x2 then merge_aux (Cons x1 acc) r1 l2
  69                    else merge_aux (Cons x2 acc) l1 r2
  70     end
  71
  72   let merge (l1 l2: list elt) : list elt
  73     requires { sorted l1 /\ sorted l2 }
  74     ensures  { sorted result /\ permut result (l1 ++ l2) }
  75   =
  76     merge_aux Nil l1 l2
  77
  78 end
  79
  80 (** Mergesort.
  81
  82     This implementation splits the input list in two according to even- and
  83     odd-order elements (see function `split` below). Thus it is not stable.
  84     For a stable implementation, see below module `OCamlMergesort`. *)
  85
  86 module Mergesort
  87
  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         (length r2 = length r1 \/ length r2 = length r1 + 1) /\
  98         permut (r1 ++ r2) (l1 ++ (l2 ++ l)) }
  99       variant { length l }
 100     = match l with
 101       | Nil -> l1, l2
 102       | Cons x r -> split_aux l2 (Cons x l1) r
 103       end
 104     in
 105     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       | Nil | Cons _ Nil -> l
 112       | _ -> let l1, l2 = split l in merge (mergesort l1) (mergesort l2)
 113     end
 114
 115 end
 116
 117 (** {2 OCaml's List.sort}
 118
 119     There are several ideas here:
 120
 121     - instead of splitting the list in two, sort takes the length of
 122       the prefix to be sorted; hence there is nothing to do to get the
 123       first half and the second half is obtained with chop (which does
 124       not allocate at all)
 125
 126     - all functions are tail recursive. To avoid the extra cost of
 127       List.rev, sort is duplicated in two versions that respectively
 128       sort in order and in reverse order (`sort` and `sort_rev`) and
 129       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 module OCamlMergesort
 135
 136   clone export Elt with axiom .
 137   use list.Mem
 138   use list.Reverse
 139   use list.RevAppend
 140
 141   lemma sorted_reverse_cons:
 142     forall acc x1. sorted (reverse acc) ->
 143     (forall x. mem x acc -> le x x1) -> sorted (reverse (Cons x1 acc))
 144
 145   lemma sorted_rev_append: forall acc l: list elt.
 146     sorted (reverse acc) ->
 147     sorted l ->
 148     (forall x y. mem x acc -> mem y l -> le x y) ->
 149     sorted (reverse (rev_append l acc))
 150
 151   let rec rev_merge (l1 l2 accu: list elt) : list elt
 152     requires { sorted (reverse accu) /\ sorted l1 /\ sorted l2 }
 153     requires { forall x y: elt. mem x accu -> mem y l1 -> le x y }
 154     requires { forall x y: elt. mem x accu -> mem y l2 -> le x y }
 155     ensures  { sorted (reverse result) }
 156     ensures  { permut result (accu ++ l1 ++ l2) }
 157     variant  { length l1 + length l2 }
 158   = match l1, l2 with
 159     | Nil, _ -> rev_append l2 accu
 160     | _, Nil -> rev_append l1 accu
 161     | Cons h1 t1, Cons h2 t2 ->
 162        if le h1 h2 then rev_merge t1 l2 (Cons h1 accu)
 163                    else rev_merge l1 t2 (Cons h2 accu)
 164     end
 165
 166   lemma sorted_reverse_mem:
 167     forall x l. sorted (reverse (Cons x l)) -> forall y. mem y l -> le y x
 168
 169   lemma sorted_reverse_cons2:
 170     forall x l. sorted (reverse (Cons x l)) -> sorted (reverse l)
 171
 172   let rec rev_merge_rev (l1 l2 accu: list elt) : list elt
 173     requires { sorted accu /\ sorted (reverse l1) /\ sorted (reverse l2) }
 174     requires { forall x y: elt. mem x accu -> mem y l1 -> le y x }
 175     requires { forall x y: elt. mem x accu -> mem y l2 -> le y x }
 176     ensures  { sorted result }
 177     ensures  { permut result (accu ++ l1 ++ l2) }
 178     variant  { length l1 + length l2 }
 179   = match l1, l2 with
 180     | Nil, _ -> rev_append l2 accu
 181     | _, Nil -> rev_append l1 accu
 182     | Cons h1 t1, Cons h2 t2 ->
 183        if not (le h1 h2) then rev_merge_rev t1 l2 (Cons h1 accu)
 184                          else rev_merge_rev l1 t2 (Cons h2 accu)
 185     end
 186
 187   function prefix int (list 'a) : list 'a
 188
 189   axiom prefix_def1:
 190     forall l: list 'a. prefix 0 l = Nil
 191   axiom prefix_def2:
 192     forall n: int, x: 'a, l: list 'a. n > 0 ->
 193     prefix n (Cons x l) = Cons x (prefix (n-1) l)
 194
 195   let rec lemma prefix_length (n: int) (l: list 'a)
 196     requires { 0 <= n <= length l } ensures { length (prefix n l) = n }
 197     variant { n } =
 198     if n > 0 then match l with Nil -> () | Cons _ r -> prefix_length (n-1) r end
 199
 200   let rec lemma prefix_append (n: int) (l1 l2: list 'a)
 201     requires { length l1 <= n <= length l1 + length l2 }
 202     ensures  { prefix n (l1 ++ l2) =
 203                prefix (length l1) l1 ++ prefix (n - length l1) l2 }
 204     variant  { l1 }
 205   = match l1 with Nil -> () | Cons _ t -> prefix_append (n-1) t l2 end
 206
 207   let rec chop (n: int) (l: list 'a) : list 'a
 208     requires { 0 <= n <= length l }
 209     ensures  { l = prefix n l ++ result }
 210     variant  { n }
 211   =
 212     if n = 0 then l else
 213     match l with
 214       | Cons _ t -> chop (n-1) t
 215       | Nil -> absurd
 216     end
 217
 218   (** `sort n l` sorts `prefix n l`
 219       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     requires { 2 <= n <= length l }
 225     ensures  { sorted result }
 226     ensures  { permut result (prefix n l) }
 227     variant  { n }
 228   =
 229     if n = 2 then match l with
 230       | Cons x1 (Cons x2 _) ->
 231           if le x1 x2 then Cons x1 (Cons x2 Nil) else Cons x2 (Cons x1 Nil)
 232       | _ -> absurd
 233     end else if n = 3 then match l with
 234       | Cons x1 (Cons x2 (Cons x3 _)) ->
 235            if le x1 x2 then
 236              if le x2 x3 then Cons x1 (Cons x2 (Cons x3 Nil))
 237              else if le x1 x3 then Cons x1 (Cons x3 (Cons x2 Nil))
 238              else Cons x3 (Cons x1 (Cons x2 Nil))
 239            else
 240              if le x1 x3 then Cons x2 (Cons x1 (Cons x3 Nil))
 241              else if le x2 x3 then Cons x2 (Cons x3 (Cons x1 Nil))
 242              else Cons x3 (Cons x2 (Cons x1 Nil))
 243        | _ -> absurd
 244     end else begin
 245       let n1 = n / 2 in
 246       let n2 = n - n1 in
 247       let l2 = chop n1 l in
 248       assert { prefix n1 l ++ prefix n2 l2 = prefix n l };
 249       let s1 = rev_sort n1 l in
 250       let s2 = rev_sort n2 l2 in
 251       rev_merge_rev s1 s2 Nil
 252    end
 253
 254   with rev_sort (n: int) (l: list elt) : list elt
 255     requires { 2 <= n <= length l }
 256     ensures  { sorted (reverse result) }
 257     ensures  { permut result (prefix n l) }
 258     variant  { n }
 259   =
 260     if n = 2 then match l with
 261       | Cons x1 (Cons x2 _) ->
 262           if not (le x1 x2) then Cons x1 (Cons x2 Nil)
 263           else Cons x2 (Cons x1 Nil)
 264       | _ -> absurd
 265     end else if n = 3 then match l with
 266       | Cons x1 (Cons x2 (Cons x3 _)) ->
 267            if not (le x1 x2) then
 268              if not (le x2 x3) then Cons x1 (Cons x2 (Cons x3 Nil))
 269              else if not (le x1 x3) then Cons x1 (Cons x3 (Cons x2 Nil))
 270              else Cons x3 (Cons x1 (Cons x2 Nil))
 271            else
 272              if not (le x1 x3) then Cons x2 (Cons x1 (Cons x3 Nil))
 273              else if not (le x2 x3) then Cons x2 (Cons x3 (Cons x1 Nil))
 274              else Cons x3 (Cons x2 (Cons x1 Nil))
 275        | _ -> absurd
 276     end else begin
 277       let n1 = n / 2 in
 278       let n2 = n - n1 in
 279       let l2 = chop n1 l in
 280       assert { prefix n1 l ++ prefix n2 l2 = prefix n l };
 281       let s1 = sort n1 l in
 282       let s2 = sort n2 l2 in
 283       rev_merge s1 s2 Nil
 284     end
 285
 286   lemma permut_prefix: forall l: list elt. permut (prefix (length l) l) l
 287
 288   let mergesort (l: list elt) : list elt
 289     ensures { sorted result /\ permut result l }
 290   =
 291     let n = length l in
 292     if n < 2 then begin
 293       assert { sorted l by match l with
 294                Nil | Cons _ Nil -> sorted l | _ -> false end }; l end
 295     else sort n l
 296
 297 end