% Lemmas from Hoare: "Proof of a recursive program: Quicksort",
%             The Computer Journal 14(4)

Definitions:

Sorted(A,m,n) <-> forall p,q. m <= p <= q <= n -> A[p] <= A[q]
Partd(A,i,j,m,n)
  <-> j < i & (forall p,q. m <= p < i & j < q <= n -> A[p] <= A[q])

Properties of Perm:

Perm(A,A,m,n)
Perm(A1,A2,m,n) & Perm(A2,A3,m,n) -> Perm(A1,A3,m,n)
m <= i <= j <= n & Perm(A1,A2,i,j) -> Perm(A1,A2,m,n)
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  -> Perm(A',A,i,j)
Perm(A1,A2,m,n) & i < m -> A1[i] = A2[i]
Perm(A1,A2,m,n) & n < j -> A1[i] = A2[i]

------------------------------------------------------------
proc Quicksort(int m, int n, var array A)=
{A=A0}
if m<n then
  begin
    int i,j;
    Partition(m,n,A,i,j);
    {A=A1 & Partd(A1,i,j,m,n) & Perm(A1,A0,m,n)}
    Quicksort(m,j,A);
    {A=A2 & Sorted(A2,m,j) & Perm(A2,A1,m,j)}
    Quicksort(i,n,A);
    {Sorted(A,i,n) & Perm(A,A2,i,n)}
  end
{Sorted(A,m,n) & Perm(A,A0,m,n)}

Lemma 1: (main condition of Quicksort false)
A = A0 & n <= m -> Sorted(A,m,n) & Perm(A,A0,m,n)

Lemma 2: (main condition of Quicksort true)
Partd(A1,i,j,m,n) & Perm(A1,A0,m,n) &
Sorted(A2,m,j) & Perm(A2,A1,m,j) &
Sorted(A,i,n) & Perm(A,A2,i,n)
  -> Sorted(A,m,n) & Perm(A,A0,m,n)

Lemma 2.ii: (permutations compose)
Perm(A1,A0,m,n) & Perm(A2,A1,m,j) & Perm(A,A2,i,n)
  -> Perm(A,A0,m,n)

Lemma 2.i.a: (partition invariant w.r.t. permutations)
Partd(A1,i,j,m,n) & Perm(A2,A1,m,j) & Perm(A,A2,i,n)
  -> Partd(A,i,j,m,n)

Lemma 2.i.b:
j < i & Sorted(A2,m,j) & Perm(A,A2,i,n)
  -> Sorted(A,m,j)

Lemma 2.i:
Partd(A,i,j,m,n) & Sorted(A,m,j) & Sorted(A,i,n)
  -> Sorted(A,m,n)

------------------------------------------------------------
proc Partition(int m, int n, var array A, var int i, var int j)=
{m<n}
begin
  int r,f;
  f:=(m+n)/2; r:=A[f]; i:=m; j:=n;
  {Perm(A,A0,m,n) "A-inv" &
   m <= f <= n "f-inv" &
   m <= i & (forall p. m <= p < i -> A[p] <= r) "i-inv" &
   j <= n & (forall q. j < q <= n -> r <= A[q]) "j-inv"}
  while i <= j do
    begin
      {"A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv" & i <= j}
      while A[i] < r do i:=i+1; (*find 8*)
      {"A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv"}
      while r < A[j] do j:=j-1; (*find 9*)
      {"A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv"}
      if i <= j then (* find 10,11 *)
        begin
          {A'=A & i <= j &
           "A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv"}
          w:=A[i]; A[i]:=A[j]; A[j]:=w; (*3*)
          {A[i] <= r <= A[j] &
           "A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv"}
          i:=i+1; j:=j-1;
        end
      {"A-inv" & "f-inv" & "m-inv" & "n-inv" & "i-inv" & "j-inv"}
    end
end
{Partd(A,i,j,m,n) & Perm(A,A0,m,n)}

Lemma 3:
A'[i]=A[j] & A'[j]=A[i] & (forall s. s\=i & s\=j -> A'[s]=A[s])
  & m <= i <= j <= n
  -> Perm(A,A0,m,n)

The remaining lemmas can be adapted from find by replacing
1 with m and N with n.