你的调整法证明可能假了！

看到 P1012 被升蓝，以及 Register_int 的帖子，感慨良多。

事实上，我发现自己之前许多调整法/交换论证的证明是假的。所以写这篇文章来整理交换论证相关。

邻项交换

若对于相邻两项 $x, y$，让 $x$ 在 $y$ 前面更优，我们称 $x < y$。

很多证明可能到这一步就停止了。然而这是错误的。仅仅具备这样的性质，并不能保证“对于任意相邻两项 $x, y$，其中靠前的 $x$ 满足 $x < y$”的序列是唯一的。

简单的反例：$x < y, y < z, z < x$。这时 $(x, y, z)$ 与 $(z, x, y)$ 均满足条件。

不同的序关系

oi-wiki 有所提及：https://oi-wiki.org/math/order-theory/

重点在于定义的那些性质，以及全序、偏序、严格偏序、弱序、严格弱序等不同种类的序关系。

众所周知，如果把 $\lambda x . \lambda y . \; (x\leq y)$ 放进 std::sort 中，很有可能会得到死循环的结果。因为它要求严格弱序，即需要非自反性和非对称性。简单来说，$x < y \text{ and } y < x$ 与 $x < x$ 两个性质都是恒不成立的。同时，严格弱序还要求不可比性是一个等价关系（即满足自反性、传递性和对称性，如果不可比性不是等价关系，则这只是严格偏序而不是严格弱序）。

而事实上，要进行“排序”，确定唯一的序列，我们需要全序。如果仅仅是确定最大的答案，严格弱序即可。并且这时，交换相等的相邻元素（“相等”意味着在严格弱序关系下不可比）不改变答案。

如何证明传递性？

一般而言有几种方法。一种是强化邻项交换，变成“交换任意（可能不相邻）的两项一定不劣/严格更优”。

另一种则是刻画关系的性质。如果发现存在一个函数 $f$ 的目标集合是实数，且 $x < y$ 当且仅当 $f(x) < f(y)$，这样严格弱序就直接得证了。因为实数的 $<$ 是全序。

当对任意不等的 $x, y$ 有 $f(x) \neq f(y)$ 时，我们能够由实数比较的全序直接推到原来的关系的全序。