Correctness proof of the algoritm to generate permutations in lexicographic order

The following algorithm generates the next permutation lexicographically after a given permutation. It changes the given permutation in-place.

• Find the largest index k such that a[k]

• Find the largest index l greater than k such that a[k]

• Swap the value of a[k] with that of a[l].

• Reverse the sequence from a[k + 1] up to and including the final element a[n].

(from https://en.wikipedia.org/wiki/Permutation#Generation_in_lexicographic_order)

I would like to know a (possible formal) proof.

One can try to come up with the algorithm by oneself (thereby proving its correctness) after incremental understanding of: (a) how to define a permutation as "larger" (lexciographically) than another one, (b) what really the very next permutation of $P$ "looks like" compared to $P$ (how/where it differs from $P$). Once we find-out some properties, we may be able to write this algorithm ourselves.

Some outline:

-
define the "lexicographic order" of permutations $P_1$ and $P_2$. Say, $k$ is the very first index at which they differ. Then the "order" of their elements at index $k$ decides the "lexicographic order" of $P_1$ and $P_2$.

-
So what should be the smallest and largest permutation of array $a$ ?

-
Suppose array $a$ currently holds permutation $P$. Say $P'$ is the very next permutation of $P$ in the lexicographic-order, and they first differ at index $k$. Now, use the definition in (1) and the observation in (2) to find out what is the structure of elements in $P/P'$ at index $k$ and after it. You can argue that:

• elements in $P$ after $k$ must form a decreasing-sequence (call it $S$).

• element in $P$ at $k$ must be smaller than the largest element of $S$, which is $a[k+1]$.

• due to above, we must have an element $a[l]$ in $S$ which is the smallest element in $S$ larger than $a[k]$. In $P'$, this element must appear at index $k$.

• so the remaining (after $k$) elements of $P'$ are simply $S$ with $a[l]$ removed and $a[k]$ added.

• these remaining (after $k$) elements of $P'$, must be in increasing order (for $P'$ to be the smallest possible, but larger than $P$). The 4th step in the posted algorithm is simply obtaining this increasing order by reversing the existing decreasing-sequence $S$ (now modified via swap, but continues to remain decreasing).

For further details, refer to section "Lexicographical Order" in this article (written by me).

StackExchange Computer Science Q#68974, answer score: 3