title: Loop Invariant of QuickSort Partition
body: <p>I'm having trouble defining and proving a <strong>loop invariant</strong> for some implementation of Quicksort algorithm. This is neither Lomuto's nor Hoare's partition version.</p>
  
  <p>If you know about some known version of Quicksort that is implemented this way, let me know, please.</p>
  
  <p>Algorithm's implementation in Python:</p>
  
  <pre class="lang-py prettyprint-override"><code>def partition(arr: list, p: int, r: int):
      y = arr[p]
      i = p
      j = r + 1
  
      while i &lt; j:
          i = i + 1
  
          while i &lt;= r and A[i] &lt; y:
              i = i + 1
  
          j = j - 1
  
          while j &gt;= p and A[j] &gt; y:
              j = j - 1
  
          if i &lt;= j:
              swap(arr, i, j)
  
      swap(arr, j, p)
  
      return j
  
  
  def quicksort(arr: list, p: int, r: int):
      if p &lt; r:
          q = partition(arr, p, r)
          quicksort(arr, p, q - 1)
          quicksort(arr, q + 1, r)
  
  
  def swap(arr: list, i, j):
      tmp = arr[i]
      arr[i] = arr[j]
      arr[j] = tmp
  </code></pre>
  
  <p>I have managed to define the following loop invariant (<em>it might be incorrect</em>):</p>
  
  <blockquote>
    <p>At the beginning of each iteration of the <code>while</code> loop, for each index <code>k</code> in array <code>A</code>:</p>
    
    <ul>
    <li><p>if <code>k = p</code>, so <code>A[k] = y</code></p></li>
    <li><p>if <code>p &lt; k &lt;= i</code>, so <code>A[k] &lt; y</code></p></li>
    <li><p>if <code>j &lt;= k &lt;= r</code>, so <code>A[k] &gt; y</code></p></li>
    </ul>
  </blockquote>
  
  <p>Please help me to define a loop invariant for the <code>while</code> loop in <code>partition()</code> method (if the above is incorrect), and prove it.</p>