今天在看代码源文件求diff的原理的时候看到了LCS算法。这个算法应该不陌生，动规的经典算法。具体算法做啥了我就不说了，不知道的可以直接看《算法导论》动态规划那一章。既然看到了就想回忆下，当想到算法正确性的时候，发现这个算法的正确性证明并不好做。于是想了一段时间，里面有几个细节很trick，容易陷进去。想了几轮，现在把证明贴出来，有异议的可以留言一起交流。
先把一些符号和约定说明下：
假设有两个数组，A和B。A[i]为A的第i个元素，A(i)为由A的第一个元素到第i个元素所组成的前缀。m(i, j)为A(i)和B(j)的最长公共子序列长度。
由于算法本身的递推性质，其实只要证明，对于某个i和j：
m(i, j) = m(i-1, j-1) + 1 （当A[i] = B[j]时）
m(i, j) = max( m(i-1, j), m(i, j-1) ) （当A[i] != B[j]时）
第一个式子很好证明，即当A[i] = B[j]时。可以用反证，假设m(i, j) > m(i-1, j-1) + 1 （m(i, j)不可能小于m(i-1, j-1) + 1，原因很明显），那么可以推出m(i-1, j-1)不是最长的这一矛盾结果。
第二个有些trick。当A[i] != B[j]时，还是反证，假设m(i, j) > max( m(i-1, j), m(i, j-1) )。
由反证假设，可得m(i, j) > m(i-1, j)。这个可以推出A[i]一定在m(i, j)对应的LCS序列中（反证可得）。而由于A[i] != B[j]，故B[j]一定不在m(i, j)对应的LCS序列中。所以可推出m(i, j) = m(i, j-1)。这就推出了与反正假设矛盾的结果。
得证。