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).
