mergesort_array: completed proofs

examples/in_progress/mergesort_array.mlw → examples/mergesort_array.mlw

 
-(** Sorting arrays using mergesort
+(** {1 Sorting arrays using mergesort}
 
     Author: Jean-Christophe Filliâtre (CNRS)
 *)
 
+(** {2 Parameters} *)
+
 module Elt
 
   use export int.Int
@@ -19,9 +21,16 @@ module Elt
 
 end
 
+(** {2 Merging}
+
+    It is well-known than merging sub-arrays in-place is extremely difficult
+    (we don't even know how to do it in linear time).
+    So we use some extra storage i.e. we merge two segments of a first array
+    into a second array. *)
+
 module Merge
 
-  use export Elt
+  clone export Elt
   use export ref.Refint
   use export array.Array
   use import map.Occ
@@ -80,9 +89,13 @@ module Merge
 
 end
 
+(** {2 Top-down, recursive mergesort}
+
+    Split in equal halves, recursively sort the two, and then merge. *)
+
 module TopDownMergesort
 
-  use import Merge
+  clone import Merge
   use import mach.int.Int
 
   let rec mergesort_rec (a tmp: array elt) (l r: int) : unit
@@ -111,38 +124,94 @@ module TopDownMergesort
 
 end
 
+(** {2 Bottom-up, iterative mergesort}
+
+    First sort segments of length 1, then of length 2, then of length 4, etc.
+    until the array is sorted.
+
+    Surprisingly, the proof is much more complex than for natural mergesort
+    (see below). *)
+
 module BottomUpMergesort
 
-  use import Merge
+  clone import Merge
   use import mach.int.Int
   use import int.MinMax
 
   let bottom_up_mergesort (a: array elt) : unit
-
-  =
+    ensures { sorted a }
+    ensures { permut_all (old a) a }
+  = 'I:
     let n = length a in
     let tmp = Array.copy a in
     let len = ref 1 in
     while !len < n do
       invariant { 1 <= !len }
+      invariant { permut_all (at a 'I) a }
+      invariant { forall k: int. let l = k * !len in
+                  0 <= l < n -> sorted_sub a l (min n (l + !len)) }
       variant   { 2 * n - !len }
+      'L:
       let lo = ref 0 in
+      let ghost i = ref 0 in
       while !lo < n - !len do
-        invariant { 0 <= !lo <= n }
+        invariant { 0 <= !lo /\ !lo = 2 * !i * !len }
+        invariant { permut_all (at a 'L) a }
+        invariant { forall k: int. let l = k * !len in
+                    !lo <= l < n -> sorted_sub a l (min n (l + !len)) }
+        invariant { forall k: int. let l = k * (2 * !len) in
+                    0 <= l < !lo -> sorted_sub a l (min n (l + 2 * !len)) }
         variant   { n + !len - !lo }
         let mid = !lo + !len in
+        assert { mid = (2 * !i + 1) * !len };
+        assert { sorted_sub a !lo (min n (!lo + !len)) };
         let hi = min n (mid + !len) in
+        assert { sorted_sub a mid (min n (mid + !len)) };
+        'M:
         merge_using tmp a !lo mid hi;
-        lo := hi
+        assert { permut_sub (at a 'M) a !lo hi };
+        assert { permut_all (at a 'M) a };
+        assert { hi = min n (!lo + 2 * !len) };
+        assert { sorted_sub a !lo (min n (!lo + 2 * !len)) };
+        assert { forall k: int. let l = k * !len in mid + !len <= l < n ->
+                   sorted_sub (at a 'M) l (min n (l + !len)) &&
+                   sorted_sub a         l (min n (l + !len)) };
+        assert { forall k: int. let l = k * (2 * !len) in 0 <= l < mid + !len ->
+                   k <= !i &&
+                   (k < !i ->
+                     min n (l + 2 * !len) <= !lo &&
+                     sorted_sub (at a 'M) l (min n (l + 2 * !len)) &&
+                     sorted_sub a         l (min n (l + 2 * !len)) )
+                   &&
+                   (k = !i ->
+                     l = !lo /\ sorted_sub a         l (min n (l + 2 * !len)))
+               };
+        lo := mid + !len;
+        ghost incr i
       done;
-      len := 2 * !len
-    done
+      assert { forall k: int. let l = k * (2 * !len) in 0 <= l < n ->
+               l = (k * 2) * !len &&
+               (l < !lo ->
+                 sorted_sub a l (min n (l + 2 * !len))) &&
+               (l >= !lo ->
+                 sorted_sub a l (min n (l + !len)) &&
+                 min n (l + 2 * !len) = min n (l + !len) = n &&
+                 sorted_sub a l (min n (l + 2 * !len))) };
+      len := 2 * !len;
+    done;
+    assert { sorted_sub a (0 * !len) (min n (0 + !len)) }
 
 end
 
+(** {2 Natural mergesort}
+
+    This is a mere variant of bottom-up mergesort above, where
+    we start with ascending runs (i.e. segments that are already sorted)
+    instead of starting with single elements. *)
+
 module NaturalMergesort
 
-  use import Merge
+  clone import Merge
   use import mach.int.Int
   use import int.MinMax
 
@@ -166,25 +235,35 @@ module NaturalMergesort
   exception Return
 
   let natural_mergesort (a: array elt) : unit
-
-  =
+    ensures { sorted a }
+    ensures { permut_all (old a) a }
+  = 'I:
     let n = length a in
+    if n >= 2 then
     let tmp = Array.copy a in
     let ghost first_run = ref 0 in
     try
     while true do
-      (* invariant { 0 <= !first_run && sorted_sub a 0 !first_run } *)
+      invariant { 0 <= !first_run <= n && sorted_sub a 0 !first_run }
+      invariant { permut_all (at a 'I) a }
       variant   { n - !first_run }
+      'L:
       let lo = ref 0 in
       try
       while !lo < n - 1 do
         invariant { 0 <= !lo <= n }
-        (* invariant { 0 <= !first_run && sorted_sub a 0 !first_run } *)
+        invariant { at !first_run 'L <= !first_run <= n }
+        invariant { sorted_sub a 0 !first_run }
+        invariant { !lo = 0 \/ !lo >= !first_run > at !first_run 'L }
+        invariant { permut_all (at a 'L) a }
         variant   { n - !lo }
         let mid = find_run a !lo in
         if mid = n then begin if !lo = 0 then raise Return; raise Break end;
         let hi = find_run a mid in
+        'M:
         merge_using tmp a !lo mid hi;
+        assert { permut_sub (at a 'M) a !lo hi };
+        assert { permut_all (at a 'M) a };
         ghost if !lo = 0 then first_run := hi;
         lo := hi;
       done

examples/mergesort_array/mergesort_array_BottomUpMergesort_WP_parameter_bottom_up_mergesort_1.v

+(* This file is generated by Why3's Coq driver *)
+(* Beware! Only edit allowed sections below    *)
+Require Import BuiltIn.
+Require BuiltIn.
+Require int.Int.
+Require int.Abs.
+Require int.MinMax.
+Require int.ComputerDivision.
+Require map.Map.
+Require map.Occ.
+Require map.MapPermut.
+
+(* Why3 assumption *)
+Definition unit := unit.
+
+Axiom qtmark : Type.
+Parameter qtmark_WhyType : WhyType qtmark.
+Existing Instance qtmark_WhyType.
+
+(* Why3 assumption *)
+Inductive array (a:Type) :=
+  | mk_array : Z -> (map.Map.map Z a) -> array a.
+Axiom array_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (array a).
+Existing Instance array_WhyType.
+Implicit Arguments mk_array [[a]].
+
+(* Why3 assumption *)
+Definition elts {a:Type} {a_WT:WhyType a} (v:(array a)): (map.Map.map Z a) :=
+  match v with
+  | (mk_array x x1) => x1
+  end.
+
+(* Why3 assumption *)
+Definition length {a:Type} {a_WT:WhyType a} (v:(array a)): Z :=
+  match v with
+  | (mk_array x x1) => x
+  end.
+
+(* Why3 assumption *)
+Definition get {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z): a :=
+  (map.Map.get (elts a1) i).
+
+(* Why3 assumption *)
+Definition set {a:Type} {a_WT:WhyType a} (a1:(array a)) (i:Z) (v:a): (array
+  a) := (mk_array (length a1) (map.Map.set (elts a1) i v)).
+
+(* Why3 assumption *)
+Definition make {a:Type} {a_WT:WhyType a} (n:Z) (v:a): (array a) :=
+  (mk_array n (map.Map.const v: (map.Map.map Z a))).
+
+Axiom elt : Type.
+Parameter elt_WhyType : WhyType elt.
+Existing Instance elt_WhyType.
+
+Parameter le: elt -> elt -> Prop.
+
+Axiom Refl : forall (x:elt), (le x x).
+
+Axiom Trans : forall (x:elt) (y:elt) (z:elt), (le x y) -> ((le y z) -> (le x
+  z)).
+
+Axiom Total : forall (x:elt) (y:elt), (le x y) \/ (le y x).
+
+(* Why3 assumption *)
+Definition sorted_sub (a:(array elt)) (l:Z) (u:Z): Prop := forall (i1:Z)
+  (i2:Z), ((l <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < u)%Z)) -> (le (get a i1)
+  (get a i2)).
+
+(* Why3 assumption *)
+Definition sorted (a:(array elt)): Prop := forall (i1:Z) (i2:Z),
+  ((0%Z <= i1)%Z /\ ((i1 <= i2)%Z /\ (i2 < (length a))%Z)) -> (le (get a i1)
+  (get a i2)).
+
+(* Why3 assumption *)
+Inductive ref (a:Type) :=
+  | mk_ref : a -> ref a.
+Axiom ref_WhyType : forall (a:Type) {a_WT:WhyType a}, WhyType (ref a).
+Existing Instance ref_WhyType.
+Implicit Arguments mk_ref [[a]].
+
+(* Why3 assumption *)
+Definition contents {a:Type} {a_WT:WhyType a} (v:(ref a)): a :=
+  match v with
+  | (mk_ref x) => x
+  end.
+
+(* Why3 assumption *)
+Definition map_eq_sub {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
+  (a2:(map.Map.map Z a)) (l:Z) (u:Z): Prop := forall (i:Z), ((l <= i)%Z /\
+  (i < u)%Z) -> ((map.Map.get a1 i) = (map.Map.get a2 i)).
+
+(* Why3 assumption *)
+Definition array_eq_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
+  a)) (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
+  (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
+  (map_eq_sub (elts a1) (elts a2) l u))).
+
+(* Why3 assumption *)
+Definition array_eq {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
+  a)): Prop := ((length a1) = (length a2)) /\ (map_eq_sub (elts a1) (elts a2)
+  0%Z (length a1)).
+
+(* Why3 assumption *)
+Definition exchange {a:Type} {a_WT:WhyType a} (a1:(map.Map.map Z a))
+  (a2:(map.Map.map Z a)) (l:Z) (u:Z) (i:Z) (j:Z): Prop := ((l <= i)%Z /\
+  (i < u)%Z) /\ (((l <= j)%Z /\ (j < u)%Z) /\ (((map.Map.get a1
+  i) = (map.Map.get a2 j)) /\ (((map.Map.get a1 j) = (map.Map.get a2 i)) /\
+  forall (k:Z), ((l <= k)%Z /\ (k < u)%Z) -> ((~ (k = i)) -> ((~ (k = j)) ->
+  ((map.Map.get a1 k) = (map.Map.get a2 k))))))).
+
+Axiom exchange_set : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(map.Map.map Z a)) (l:Z) (u:Z) (i:Z) (j:Z), ((l <= i)%Z /\
+  (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) -> (exchange a1
+  (map.Map.set (map.Map.set a1 i (map.Map.get a1 j)) j (map.Map.get a1 i)) l
+  u i j)).
+
+(* Why3 assumption *)
+Definition exchange1 {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
+  (i:Z) (j:Z): Prop := ((length a1) = (length a2)) /\ (exchange (elts a1)
+  (elts a2) 0%Z (length a1) i j).
+
+(* Why3 assumption *)
+Definition permut {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
+  (l:Z) (u:Z): Prop := ((length a1) = (length a2)) /\ (((0%Z <= l)%Z /\
+  (l <= (length a1))%Z) /\ (((0%Z <= u)%Z /\ (u <= (length a1))%Z) /\
+  (map.MapPermut.permut (elts a1) (elts a2) l u))).
+
+(* Why3 assumption *)
+Definition permut_sub {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array a))
+  (l:Z) (u:Z): Prop := (map_eq_sub (elts a1) (elts a2) 0%Z l) /\ ((permut a1
+  a2 l u) /\ (map_eq_sub (elts a1) (elts a2) u (length a1))).
+
+(* Why3 assumption *)
+Definition permut_all {a:Type} {a_WT:WhyType a} (a1:(array a)) (a2:(array
+  a)): Prop := ((length a1) = (length a2)) /\ (map.MapPermut.permut (elts a1)
+  (elts a2) 0%Z (length a1)).
+
+Axiom exchange_permut_sub : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z) (l:Z) (u:Z), (exchange1 a1
+  a2 i j) -> (((l <= i)%Z /\ (i < u)%Z) -> (((l <= j)%Z /\ (j < u)%Z) ->
+  ((0%Z <= l)%Z -> ((u <= (length a1))%Z -> (permut_sub a1 a2 l u))))).
+
+Axiom permut_sub_weakening : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(array a)) (a2:(array a)) (l1:Z) (u1:Z) (l2:Z) (u2:Z),
+  (permut_sub a1 a2 l1 u1) -> (((0%Z <= l2)%Z /\ (l2 <= l1)%Z) ->
+  (((u1 <= u2)%Z /\ (u2 <= (length a1))%Z) -> (permut_sub a1 a2 l2 u2))).
+
+Axiom exchange_permut_all : forall {a:Type} {a_WT:WhyType a},
+  forall (a1:(array a)) (a2:(array a)) (i:Z) (j:Z), (exchange1 a1 a2 i j) ->
+  (permut_all a1 a2).
+
+(* Why3 goal *)
+Theorem WP_parameter_bottom_up_mergesort : forall (a:Z) (a1:(map.Map.map Z
+  elt)), (0%Z <= a)%Z -> forall (tmp:Z) (tmp1:(map.Map.map Z elt)),
+  ((0%Z <= tmp)%Z /\ ((tmp = a) /\ forall (i:Z), ((0%Z <= i)%Z /\
+  (i < tmp)%Z) -> ((map.Map.get tmp1 i) = (map.Map.get a1 i)))) ->
+  forall (len:Z) (a2:(map.Map.map Z elt)), let a3 := (mk_array a a2) in
+  (((1%Z <= len)%Z /\ ((permut_all (mk_array a a1) a3) /\ forall (k:Z),
+  let l := (k * len)%Z in (((0%Z <= l)%Z /\ (l < a)%Z) -> (sorted_sub a3 l
+  (ZArith.BinInt.Z.min a (l + len)%Z))))) -> ((len < a)%Z -> forall (i:Z)
+  (lo:Z) (a4:(map.Map.map Z elt)), let a5 := (mk_array a a4) in
+  ((((0%Z <= lo)%Z /\ (lo = ((2%Z * i)%Z * len)%Z)) /\ ((permut_all a3 a5) /\
+  ((forall (k:Z), let l := (k * len)%Z in (((lo <= l)%Z /\ (l < a)%Z) ->
+  (sorted_sub a5 l (ZArith.BinInt.Z.min a (l + len)%Z)))) /\ forall (k:Z),
+  let l := (k * (2%Z * len)%Z)%Z in (((0%Z <= l)%Z /\ (l < lo)%Z) ->
+  (sorted_sub a5 l (ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z)))))) ->
+  ((~ (lo < (a - len)%Z)%Z) -> ((forall (k:Z), let l :=
+  (k * (2%Z * len)%Z)%Z in (((0%Z <= l)%Z /\ (l < a)%Z) ->
+  ((l = ((k * 2%Z)%Z * len)%Z) /\ (((l < lo)%Z -> (sorted_sub a5 l
+  (ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z))) /\ ((lo <= l)%Z ->
+  ((sorted_sub a5 l (ZArith.BinInt.Z.min a (l + len)%Z)) /\
+  ((((ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z) = (ZArith.BinInt.Z.min a (l + len)%Z)) /\
+  ((ZArith.BinInt.Z.min a (l + len)%Z) = a)) /\ (sorted_sub a5 l
+  (ZArith.BinInt.Z.min a (l + (2%Z * len)%Z)%Z))))))))) -> forall (len1:Z),
+  (len1 = (2%Z * len)%Z) -> forall (k:Z), let l := (k * len1)%Z in
+  (((0%Z <= l)%Z /\ (l < a)%Z) -> (sorted_sub a5 l
+  (ZArith.BinInt.Z.min a (l + len1)%Z)))))))).
+intros a a1 h1 tmp tmp1 (h2,(h3,h4)) len a2 a3 (h5,(h6,h7)) h8 i lo a4 a5
+((h9,h10),(h11,(h12,h13))) h14 h15 len1 h16 k l (h17,h18).
+subst l len1.
+destruct (h15 k); clear h15; intuition.
+assert (case: (k * (2 * len) < lo \/ lo <= k * (2 * len))%Z) by omega.
+destruct case; intuition.
+Qed.
+