Quicksort with Bentley-Bull trick

in 0.83, fully automatic but with combining Alt-ergo, Yices, Z3.

module QuickSort

  use import int.Int
  use import ref.Ref
  use import array.Array
  use import array.IntArraySorted
  use import array.ArrayPermut
  use import array.ArrayEq

  predicate div_sub (a: array int) (l m u: int) =
  (forall i: int. l <= i < m -> a[i] <= a[m]) /\
  (forall j: int. m+1 <= j < u -> a[m] <= a[j])

  lemma sorted_div_sorted_sub:
    forall a: array int. forall l m u : int.
       sorted_sub a l m -> div_sub a l m u -> sorted_sub a (m+1) u
      -> sorted_sub a l u

  lemma permut_sub_trans:
    forall a1 a2 a3: array 'a, l u: int.
    permut_sub a1 a2 l u -> permut_sub a2 a3 l u ->
    permut_sub a1 a3 l u

  let swap (a: array int) (i: int) (j: int) =
    requires { 0 <= i < length a /\ 0 <= j < length a }
    ensures { exchange (old a) a i j }
   let v = a[i] in
    a[i] <- a[j];
    a[j] <- v

  let rec quick_sort1 (a: array int) lo hi =
    requires { 0 <= lo <= length a /\ 0 <= hi <= length a }
    ensures { sorted_sub a lo hi /\ permut_sub (old a) a lo hi}
'L:
    if lo < hi - 1 then begin
    let i = ref (lo + 1) in
    for j = lo + 1 to hi - 1 do
      invariant { lo < !i <= j }
      invariant {forall k: int. lo+1 <= k < !i ->  a[k] <= a[lo]}
      invariant {forall k': int. !i <= k' < j -> a[lo] <= a[k']}
      invariant {permut_sub (at a 'L) a (lo+1) hi}
      if a[j] < a[lo] then begin
          swap a !i j;
          i := !i + 1
      end
      done;
      assert {permut_sub (at a 'L) a lo hi };
      swap a lo (!i-1);
      assert {permut_sub (at a 'L) a lo hi };
      assert {div_sub a lo (!i-1) hi };
      quick_sort1 a lo (!i - 1);
      assert {permut_sub (at a 'L) a lo hi };
      assert {div_sub a lo (!i-1) hi };
      quick_sort1 a !i hi;
      assert {permut_sub (at a 'L) a lo hi };
      assert {div_sub a lo (!i-1) hi }
    end

  let quick_sort (a: array int) =
    ensures { sorted a /\ permut_all (old a) a}
    quick_sort1 a 0 (Array.length a)

end