[phkahler]

I thought his goal was to get the prover to prove it without understanding it himself.

By realizing the low-indexed portion is always sorted, you've already proved the algorithm yourself and the prover is just checking for bugs in your logic.

I'm not saying the proof isnt valuable, just that it's not magical and actually requires the user to understand the majority of the proof already.

[leereeves]

This algorithm is surprising and interesting because it doesn't work at all like it at first seems to.

The low-indexed portion is sorted, but isn't guaranteed to contain the lowest or the highest i elements of the list (except when i=1), and the list is ultimately sorted in decreasing, not increasing order. The final sort doesn't occur until the last iteration of the outer loop when the inequality is reversed (the interesting variable, j, is on the right).

Because of that, the proof outline discussed here doesn't work.

Consider what happens if the unique smallest element starts at position n. It is placed at the start of the list (the correct final position) in the final iteration of the outer loop (i=n), and not before.

Proof (for simplicity the list is indexed 1 to n):

Let A[n] < A[k] for all k != n in the initial list.

Elements are only swapped when A[i] < A[j]. If i != n and j = n, then A[i] > A[n] = A[j], so A[n] is not swapped.

Then, when i = n and j = 1, A[i] = A[n] < A[1] = A[j], so A[1] and A[n] are swapped, placing the smallest element in position 1 at last.

[umanwizard]

It’s not true that it’s sorted in decreasing order. See my comment here: https://news.ycombinator.com/item?id=31978942

[leereeves]

Quite right, that was a silly mistake on my part. I did say the smallest element was placed first, but wrote "the list is ultimately sorted in decreasing, not increasing order" backwards.

I meant to contradict the top post: "the largest number is at position 1...we can treat n+1 as a new array of length N-n and solve using the base case proof", which would result in decreasing order (largest first).

[phkahler]

The largest number is at position 1 after the first pass of the inner j loop. In fact it's at the ith position after each completion of the j loop, and it serves to separate the sorted and unsorted parts of the array.

Beyond that it's just inserting the ith element into the list by finding its place and shifting everything over one position.