Proof of correct of the dynamic programming approach to min edit distance

I couldn't find any satisfying proof so I made one. All the proofs that I've read do not actually prove that the cases are collectively exhaustive.

(A) There always exists at least one optimal series of edits and let it be called Eo

This is trivial.

(B) In Eo there are characters that never get inserted or changed. Let the last of such characters be called pivot.

If there isn't any, we can use the start of the string as pivot. In Eo, this common subsequence never gets changed from the beginning to the end. We are not assuming it to be the longest common subsequence or anything.

e.g.) #KITTEN, #SITTING → pivot : '#ITTN'[-1] = 'N'

There are a few properties of this pivot which makes the problem much easier.

1. The left side and the right side of the pivot are independent to each other. Whatever edits that happen on one side cannot affect the other.
2. By the definition (B), all characters on the right side of the pivot of the target string should be made correct by either replacement or addition.

Because of (1) we only need to consider the right side of the pivot of the original string and the target string. Let's just assume the left side is optimal(greedy) and the number of edits will be added to the total.
e.g)
#weofanbmcdepmqu -> #eopasbctdewni
only consider pmqu → wni
Using (2) this subproblem can be solved as follow.
len(original)>len(target): asdfgh→qwer
Remove len(original)-len(target) times to fit the length, and replace len(target) times to fit the characters. It can be done in any order since they are all equivalent distancewise. Removing the last character at the last edit is one of such solutions which is equal to dp(original[:-1]→target) + 1.
len(original)<len(target): asdf→qwerty
Add len(target)-len(original) times to fit the length, and replace len(original) times to fit the characters. Adding the last character at the last edit is equal to dp(original→target[:-1])+1.
len(original)==len(target)!=0: asdf→qwer
Replace for the length. It is equal to replacing the last character at the last edit. dp(original[:-1]→target[:-1])+1
len(original)==len(target)==0: ' '→' '
The last character is the pivot. This happens when the last characters are the same characters. You don't edit the pivot so it is same as dp(original[:-1]->target[:-1])

This is my proof:

To get from string A to B we perform an optimal set of operations from left to right. There are 4 operations: EQ (keep the character), SWAP (change the character), INS (insert a character), DEL (delete a character). This is the definition of the edit distance, with cost of EQ == 0.

Define the length of A as a, and the Length of B as b.

Define d[a,b] as the edit distance between the first a characters of A and the first b characters of B, which means the number of operations (besides EQ) required to do on A in order to get to B.

If we look at an optimal series of operations (there must be one), there are 4 options for the last operation. We don’t know the last operation, so we check all 4 options and take the best one (best means MINIMUM edit distance).

If the last operation was EQ that means that A[a]==B[b] and that the edit distance equals to d[a-1, b-1], because EQ is not considered as an “edit distance” cost.

If the last operation was SWAP that means that A[a]!=B[b] and that the edit distance equals to d[a-1, b-1] + 1.

If the operation was INS it means that edit distance is d[a, b-1] + INS(to B) If the operation was DEL it means that the edit distance is d[a-1, b] + DEL(from A)

We simply try all combinations of the 4 operations from LAST to FIRST until we find the best path. Actually it’s 3 operations every step, because we can decide if to check EQ or SWAP depending on if the current characters are equal or not. (if they are equal, no need to check SWAP operation and vice versa).

Since we try all possible operations, the recursion formula must be true.

Say we are editing a string A of length m into a string B of length n using a minimal edit sequence.

A key fact to notice is that in a minimal edit sequence, each of the characters in A and B is operated on at most once. (This is easy to show; if a character is operated on twice, we can combine those operations into a single equivalent operation.)

It follows that we can partition the characters in A and B as:

• Characters in A that are deleted (and are not in B)
• Characters in B that are inserted (and are not in A)
• Pairs of a character from A and a character from B which are either:
  • Substituted (and are therefore different)
  • Left alone (and are therefore the same)

Consider A[m] and B[n], the last characters of A and B. The following are possible cases for the minimal edit sequence; we claim that at least one of them is true:

1. A[m] is deleted
2. B[n] is inserted
3. A[m] is paired with B[n]

If 1) is false, then A[m] must be paired with a character A[m]' in B, and if 2) is also false, then B[n] must be paired with a character B[n]' in A.
Note that all edit operations preserve the order of the characters. So we cannot have A[m]' before B[n] and B[n]' before A[m] -- otherwise the pairs have changed order.
Thus, A[m]' is B[n] and B[n]' is A[m] -- that is, A[m] is paired with B[n], and the claim is demonstrated.

What remains is simple recursion on each of the three possible cases. Let A[..m-1] represent all of A except its last character A[m], and B[..n-1] represent all of B except its last character B[n].

In case 1), to edit A into B we must delete A[m] and edit A[..m-1] into B, which in total can be done in a minimum of 1 + distance(A[..m-1], B) operations.

In case 2), to edit A into B we must edit A into B[..n-1] and insert B[n], which in total can be done in a minimum of 1 + distance(A, B[..n-1]) operations.

And in case 3), we must either substitute A[m] into B[n] if it has changed, or leave it alone if it has not, and then edit A[..m-1] into B[..n-1], which in total can be done in a minimum of 1 + distance(A[..m-1], B[..n-1]) operations or distance(A[..m-1], B[..n-1]) operations respectively.

As these are the only possible cases, choosing a case for which this minimum number of operations is smallest yields an edit sequence with the smallest possible number of operations.

I found these sources useful:
https://blog.cykerway.com/posts/2021/04/10/minimum-edit-distance.html
https://cstheory.stackexchange.com/questions/10391/proof-of-levenshtein-distance/48178#48178