3.1 直接证明、逆否与分类讨论：搭出可检查的推理链

代码评审里一句“这里肯定不会为空”，不是证明。要让别人检查这个结论，需要说明对象范围、已知条件，以及每一步依据什么定义或定理。

证明的价值不在于写得像数学论文，而在于把“结论为何必然成立”拆成可质疑、可复用的推理链。

先把命题写完整

一个定理通常包含量词、前提和结论：

对任意整数 n，若 n 是偶数，则 n² 是偶数。

形式化为：

∀n∈ℤ (Even(n) → Even(n²))

证明开始时要固定一个任意满足前提的对象，而不是挑一个方便的例子：

任取 n∈ℤ，并假设 n 为偶数。

因为 n 没有任何额外特殊性质，推导出的结论才覆盖所有偶数。

直接证明：展开定义再向目标推进

偶数定义：

Even(n) ⇔ ∃k∈ℤ, n=2k

于是：

设 n=2k，其中 k∈ℤ。
n²=(2k)²=4k²=2(2k²)。
因为 2k²∈ℤ，所以 n² 是偶数。

这个证明的每一步都有来源：偶数定义、代数运算、整数对乘法封闭。最后一句要重新对齐目标定义，不能停在“结果显然”。

直接证明的通用模板：

1. 任取量词范围内的对象；
2. 假设前提；
3. 展开相关定义；
4. 应用已知事实逐步变形；
5. 得到结论的定义形式。

逆否证明：换一个等价方向

命题：若 p → q，其逆否命题是：

¬q → ¬p

两者逻辑等价。若直接从 p 推 q 很难，可以改证逆否。

定理：对整数 n，若 n² 是偶数，则 n 是偶数。

逆否命题：若 n 不是偶数，即 n 为奇数，则 n² 为奇数。

设 n=2k+1，其中 k∈ℤ。
n²=(2k+1)²=4k²+4k+1=2(2k²+2k)+1。
所以 n² 为奇数。

逆否证明与反证法不同。逆否法直接证明一个等价蕴含；反证法则暂时假设待证结论为假并推出矛盾。

还要区分：

原命题：p → q
逆命题：q → p
否命题：¬p → ¬q
逆否命题：¬q → ¬p

原命题总与逆否命题等价；逆命题也总与否命题等价，但这两组一般不等价。例如 p=F,q=T 时，原命题和逆否命题为真，另外两个为假。证明“登录成功需要令牌”并不能推出“有令牌就一定登录成功”。

分类讨论：把所有可能分区

若对象自然分成有限且互斥的情形，可逐类证明。

定理：对任意整数 n，n(n+1) 为偶数。

整数 n 要么偶，要么奇：

• 若 n 偶，则乘积含偶因子 n；
• 若 n 奇，则 n+1 偶，乘积含偶因子 n+1。

两种情形穷尽所有整数，因此结论成立。

分类证明有两个义务：

1. 各情形确实覆盖全部可能；
2. 每个情形下结论成立。

情形不必互斥，但互斥通常让证明更清楚。若有重叠，不影响正确性，只可能重复工作。

软件中常见的分类包括状态枚举、输入符号类别、树节点类型和协议消息种类。default 分支可以在语法上接住新增状态，但旧证明未必说明这些状态满足目标性质。新增状态后，应重新验证该分支的推理，不能把“代码有分支可走”当作“证明已经覆盖”。

双条件要证明两个方向

证明 p ↔ q，必须分别证明：

p → q
q → p

定理：整数 n 为偶数，当且仅当 n² 为偶数。

• 正向已由直接证明确立；
• 反向可用逆否法证明。

只证明一个方向，是规格评审中常见的漏洞。“缓存命中时数据有效”不等于“数据有效时一定缓存命中”。

集合相等是双向包含证明

证明：

A ∩ (B ∪ C) = (A ∩ B) ∪ (A ∩ C)

可用双向包含，也可直接对任意元素做等价链：

x∈A∩(B∪C)
⇔ x∈A ∧ (x∈B ∨ x∈C)
⇔ (x∈A ∧ x∈B) ∨ (x∈A ∧ x∈C)
⇔ x∈(A∩B)∪(A∩C)

中间使用命题逻辑的分配律。好的证明会注明关键转换，而不是让读者猜。

证明写作的最小标准

• 量词范围明确；
• 新变量说明类型和来源；
• 使用定义时写出关键展开；
• 引用前面定理时说明名称；
• 不用几个例子代替全称证明；
• 结尾明确对齐原目标。

形式符号不是越多越好。若自然语言能清楚表达一步，就不必把每个连接词都符号化；但任何可能改变范围、条件或量词顺序的地方，应保持精确。

完成检查

1. 直接证明：两个偶数之和为偶数；
2. 逆否证明：若 ab 为奇数，则 a、b 都为奇数；
3. 分类证明：任意整数的平方除以 4，余数只能是 0 或 1；
4. 分别证明两个方向：A⊆B 当且仅当 A∩B=A；
5. 找一个真实 API 需求，写出其中只成立一个方向、却容易被误读成双条件的约束。

参考资料

• Open Logic Project