证明方法、归纳法与不变式

多项式 $n^2+n+41$ 在整数零到三十九上都给出质数，很容易猜测它永远如此。但四十时得到 $1681=41^2$，因此无限主张为假。四十个成功例子为猜想提供有用证据，一个有效反例就能否定；更多成功测试不能修复该全称陈述。

证明的义务是从明确假设与定义出发，覆盖规定论域中的每种情况。程序证明还有另一层区别：说明返回答案正确，不保证程序最终会返回。若约定承诺完成，就需要结果论证与终止论证。

回忆检查：写蕴含的逆否，描述等价类，并用任意成员证明简单包含。按需复习模块 02与模块 03。使用经典逻辑、普通有限列表和含零自然数。未说明时，“所有列表”指所有有限列表。

定理（theorem）是已证明陈述，假设（hypotheses）规定结论成立的前提，引理（lemma）是用于另一论证的已证明辅助结果，正确性标准相同。猜想（conjecture）还需要论证。成功例子可说明定理或支持猜想，不能替代无限主张的证明。

选方法前，明确论域与逻辑结构。“奇数相乘仍为奇数”意为任意整数 a、b，若两者奇则乘积奇。全称蕴含提示：取任意满足假设的整数，应用奇数定义。不必枚举整数或使用高级定理。

论证结构是：取任意允许输入，展开假设，做有理由的变换，识别结论定义。只写代数漏掉符号为何存在及括号为何整数；只说奇乘奇为奇则重复主张。证明要连接两者。

假设只在作用域内可用。证明 $P\Rightarrow Q$ 可以假设 P 推导 Q，不能先假设 Q 并把其后果当证明。反向计算有时可用，但必须每步可逆并说明。平方方程或乘可能为零的量可失去等价或引入候选；蕴含链不自动是等价链。

全称证明的输入须在论域内任意。“令 n=4”只证明四处事实。存在证明则可选具体值，但必须验证见证。集合相等通过任意成员的双向一致性确立。逻辑结构决定证据形式。

保持符号稳定。k 若代表奇数见证，不要突然改为列表索引或别的见证。不同存在假设提供的整数用不同名字，除非已证明相等。每个符号角色和每个结论理由清晰，证明更易审查；简短不能省略必要联系。

反例也须严格。否定 $\forall x\in D,P(x)$ 要给 $x\in D$ 且 P 假。否定条件式要前提真、结论假。负输入不能反驳非负输入主张，前提不满足的例子不能反驳蕴含；它们可以说明范围，但应标明用途。

直接证明（direct proof）由假设推出结论，奇数乘积就是例子。分类证明（proof by cases）把允许论域分为覆盖完整的情况，各自证明。可以重叠，不能漏掉输入。分类应依据定义或运算在不同区域的行为。

证明 $P\Rightarrow Q$ 的逆否方法确立 $\neg Q\Rightarrow\neg P$，模块 02 已证明等价。当非 Q 比 P 易表示时有用。不要与逆命题 $Q\Rightarrow P$ 或否命题 $\neg P\Rightarrow\neg Q$ 混淆，它们通常是不同主张。

反证法（proof by contradiction）假设前提与结论否定，推出不可能。在经典逻辑中，没有允许情况能一致满足这些假设，因此结论成立。应指出具体矛盾：陈述与其否定、严格大于又不大于，或违反已证明事实。

逆否与反证相似但起点不同。逆否假设非 Q 来证明非 P；反证假设 P 且非 Q 来推出假。方法应简化论证，不应把待证结论隐藏于假设。

否定主张可用反例。“所有函数保持加法”被平方函数在二与三上否定；反向极端“没有函数保持加法”也为假，恒等函数保持。否定全称只是某个失败，不是所有对象都失败。

软件分类也要覆盖完整。搜索有成功位置与缺失标记两种返回，只验证成功分支不证明缺失。递归对象可能多个基础构造，只处理一个不覆盖其他对象。先列定义要求的情况，再审代数。

使用外部定理时明确陈述并检查前提。后续 AI 论证可能要求可微或凸，当前函数满足后才可使用结论。本模块依赖基本奇偶、整数算术及已证明逻辑规则；显式记录依赖可避免循环论证。

存在陈述要求至少一个满足性质的对象。构造性证明（constructive proof）给对象或生成方法，再验证性质与论域。“应该有解”不是证据。代数若引入候选或改变定义域，须代回验证。

$\exists!x,P(x)$ 结合存在与至多一个。仅证明任意两解相同，只得至多一个，无解时也可成立。实数 $x^2=-1$ 无解，对两个假设解的条件比较不说明存在。只找到一个也不说明唯一，$x^2=1$ 有正负一。

构造可以依赖给定输入。每个整数 x 有更大整数，可定义 $x+1$ 并验证，证明 $\forall x\exists y,y>x$，不证明一个固定 y 超过全部 x。量词顺序在证明中仍重要；构造见证的算法应声明输入论域与保证。

有时存在通过间接论证确立：假设没有见证导致矛盾，在经典逻辑中可证明存在，却未给便于实现的构造。数学定理可能够用，要求实际返回对象的程序则还需操作方法与资源论证。

唯一论证常比较任意假设解。偏序两个最小元 a、b 互相在对方之下，反对称推出相等。它不证明每个偏序有最小元。模块 03 的不可比单元素集反驳存在。不要把唯一性引理扩大成存在定理。

定义可供构造：非空有限整数列表的最小值，可从首项开始，遇更小项更新。完整正确性需要“不变式：候选是已处理前缀最小值”，终止依赖有限项数。构造提示证明，却不能只说算法显然找到。

证明两个表示对应，可构造双向映射并验证复合恢复输入。记录与标识双射给唯一逆，多对一类别标签不能。构造逆必须同时覆盖逆论域并保证输出唯一。

反例也可构造：选择对象，验证确切违反点。“每个对称关系传递”被三对象接近关系否定：两已有配对、一个缺闭合。见证不需大或真实，只需满足前提；小见证更易保存与理解。

数学归纳（mathematical induction）证明自然数索引陈述族。对全部 $n\ge n_0$，先证明基础 P($n_0$)，再对任意 $k\ge n_0$，暂时假设 P(k)，推导 P(k+1)。临时假设称归纳假设；它合法，因为归纳步证明蕴含，基础启动链。

缺基础可能留下假族但有一致代数步。错误奇数和 $\sum_{i=0}^{n-1}(2i+1)=n^2+1$ 加 $2n+1$ 后仍得 $(n+1)^2+1$，多出的一持续传播。然而零处基础假，所以归纳不能成立。假前件的蕴含不会制造真结论。

强归纳（strong induction）允许假设 P($n_0$) 到 P(k) 的全部较早情况来证明下一项，适合依赖多个或不紧邻较小输入。强归纳与普通归纳证明能力相同：普通归纳可跟踪更强命题“到 k 的全部情况成立”，得到下一步所需强假设。

每个整数 n≥2 都可表示为质数乘积。基础二为质数。强归纳步考虑 k+1：若质，已是一因子乘积；否则为 ab，$2\le a,b<k+1$，假设给 a、b 的质数乘积，合并得到 k+1。这里只证明分解存在，不证明唯一，后者需要额外论证。

基础覆盖由向后依赖决定。若步向后减三，一个基础未必覆盖各余数链。例如全部 n≥8 可写 $3a+5b$，a、b 非负：基础 8=3+5、9=3+3+3、10=5+5；n≥11 时 n−3≥8 已有表示，再加三。此特定论证需要三个基础。

良序原理（well-ordering principle）说自然数每个非空子集有最小成员。若陈述族有失败，选最小失败索引；它非已证明基础，较前索引成功，归纳步又使它成功，矛盾。这解释归纳，但依赖有下界的自然索引，不适用于没有最小元的任意集合。

明确起始索引、假设范围和归纳步目标。证明 P(k+1) 时假设 P(k+1) 是循环。只有 P(k) 到 P(k+2) 与基础零可能只覆盖偶数。测试可揭错误，书面证明仍须说明基础与步覆盖全部论域。

有些对象由构造规则定义。有限列表或为空，或由头与更小尾组成；有限满二叉树或为叶，或为恰好两个子树的节点。递归定义必须给全部构造、允许较小部分与基础。这些规则定义结构证明的论域。

列表空写 $[]$，头 h 与尾 t 写 $h::t$。长度 $\ell([])=0$，$\ell(h::t)=1+\ell(t)$；拼接 $[]\mathbin{+\!+}b=b$，$(h::t)\mathbin{+\!+}b=h::(t\mathbin{+\!+}b)$。这不是 Python 语法；Python 列表 + 可实现有限行为，高效实现不必照搬递归定义。

结构归纳（structural induction）证明基础构造，再对每个复合构造，假设较小组成部分的性质并证明整体。它遵循对象语法，不能假设正在证明的整体性质。有限构造规则生成的每个对象都由这些情况覆盖。

树可能需两个假设。有限满二叉树叶数 L、内部节点数 I，主张 L=I+1。叶基础 L=1,I=0。两个子树 A、B 的节点，叶数相加，内部数 $1+I(A)+I(B)$；用两假设给 $L(A)+L(B)=I(A)+I(B)+2=I(T)+1$。“恰好两子”至关重要，一般树未必成立。

递归计算还需终止。有限非空列表递归调用尾，长度减一直到空；再次调用同一列表则无进展。终止度量取自然数并在每次调用严格减小，有限长度可用。任意实数递减不够，$1,1/2,1/4,\ldots$ 可永远递减而不为零。

整数递归需允许论域与可达基础。非负 n 的倒数，零为基础，n>0 时调用 n−1，在自然数中递减而终止。允许负数但无其他基础，反复减一可能远离零。有基础语句不够，全部允许调用路径必须到达已处理情况。

结构归纳与按大小归纳相关，但构造形状让假设更清楚。两子树需要各自假设，表达式语言多个构造就多个情况。漏一构造便留下论域一部分未证明，哪怕所有例子都来自已处理构造。

证明递归性质不保证实现快。正确性与操作数量不同。某语言的递归拼接可能反复复制，长度恒等式仍数学正确。模块 06 分析增长与递推；当前先证明定义良好、允许有限结构上终止且满足性质。

循环不变式（loop invariant）是在从前置条件可达的每次迭代指定点成立的谓词。正确性需要初始化、保持、退出结论。它无需描述每行，但观察点应一致。几次断言成功是工具反馈，不是一般证明。

考虑固定有限整数列表 a、长度 n、整数目标 t。i 从零开始，循环条件 i<n，若 $a_i=t$ 返回 i，否则 i 加一；正常退出返回 −1。假设比较和访问会终止，列表搜索中不变。这明确状态模型，排除变化数据悄悄破坏论证。

循环头不变式为：

它表示合法边界及已处理前缀无匹配。初始 i=0，前缀空，两条件真。保持：假设不变式与 i<n，当前不匹配就加一。旧前缀无匹配，新加入的旧 i 也无匹配，所以新前缀无匹配，新边界至多 n。

不变式给部分正确性：凡返回都符合约定。终止用变式（variant） $V=n-i$，每个循环头为非负整数；不返回而继续的迭代使 i 加一，V 严格减一。非负整数不能无限严格下降，最多 n 次失败比较；成功分支立即终止。

不变式本身未必有进展。错误循环不断检查首个不匹配项，保持 i=0，“i 之前无匹配”永真，但可能不返回。部分正确性条件未必失败，完全正确性却失败。反过来，程序可以终止并返回错误位置，两义务独立。

检查一项后，处理区从小于 i 变成至多 i；增加索引后，同一区又可说小于新 i。混淆新旧值常导致保持错误。不清楚时使用 $i_{old}$ 与 $i_{new}=i_{old}+1$，明确断言位置。

方法也适用于最小值、计数与累加。“累加器等于 i 前项和”的不变式用空和初始化，加下一项保持，退出给完整和；未处理数量变式给终止。每个算法需要自己的谓词，仅复制义务名称而不分析转换不是证明。

断言可揭不变式错误，边界测试可揭遗漏分支，证明则覆盖假设下任意允许有限输入。真实代码若改变列表、停止条件或返回后续重复项，须对照已证明转换规则，不能自动移用定理。

使用 Python 3.11 或更新版本，全部标准库。运行方法见 Python 入门。每次预测、解释数学义务、诊断变化；十分分为预测三、解释四、故障三。断言验证实际执行，书面证明仍要覆盖任意允许输入。

五十分钟：预测有限和与多项式首个反例，运行。解释九次成功和检查不能证明无限族，四十处却否定质数猜想。第二时段后重建第 4 节归纳。改变范围使其排除 n，找最小失败非负输入，保存反例并区分实现故障与假定理。

下载 lab1_evidence.py

"""Successful finite checks support debugging; one valid counterexample refutes."""
from math import isqrt


def prime(n):
    return n >= 2 and all(n % divisor for divisor in range(2, isqrt(n) + 1))


def main():
    for n in range(9):
        actual = sum(range(n + 1))
        expected = n * (n + 1) // 2
        assert actual == expected
        print(f"n={n}: sum={actual}, formula={expected}")
    first_failure = next(n for n in range(51) if not prime(n * n + n + 41))
    value = first_failure * first_failure + first_failure + 41
    assert first_failure == 40 and value == 41 * 41
    print("Polynomial prime claim passes n=0 through 39.")
    print(f"Counterexample n={first_failure}: value={value}=41*41")
    print("The sum checks cover n=0..8; its general proof is separate.")


if __name__ == "__main__":
    main()

n=0: sum=0, formula=0
n=1: sum=1, formula=1
n=2: sum=3, formula=3
n=3: sum=6, formula=6
n=4: sum=10, formula=10
n=5: sum=15, formula=15
n=6: sum=21, formula=21
n=7: sum=28, formula=28
n=8: sum=36, formula=36
Polynomial prime claim passes n=0 through 39.
Counterexample n=40: value=1681=41*41
The sum checks cover n=0..8; its general proof is separate.

五十分钟，在第 6 节之后：预测晚匹配、缺失、首项重复与空列表的循环头行。运行并标注初始化、保持、成功返回与正常退出。区别不变式断言与变式递减断言。把增量一改成二，找跳过匹配的情况，解释旧保持论证为何不再覆盖整个已处理前缀。

下载 lab2_search_invariant.py

"""First-match search with assertions at the loop head and a separate variant."""


def first_match(items, target):
    n, i = len(items), 0
    while i < n:
        invariant = 0 <= i <= n and all(value != target for value in items[:i])
        assert invariant
        print(f"  head: i={i}, prefix={items[:i]}, invariant={invariant}, variant={n-i}")
        if items[i] == target:
            assert all(value != target for value in items[:i])
            return i
        previous_variant = n - i
        i += 1
        assert n - i < previous_variant
    assert i == n and all(value != target for value in items)
    print(f"  exit: i={i}, invariant=True, variant=0")
    return -1


def main():
    cases = [([2, 5, 2, 7], 7, 3), ([2, 5, 2, 7], 3, -1), ([4, 9, 4], 4, 0), ([], 9, -1)]
    for items, target, expected in cases:
        print("items=", items, "target=", target)
        result = first_match(items, target)
        assert result == expected
        print("  result=", result)
    print("Assertions check these executions; the lesson proves the general obligations.")


if __name__ == "__main__":
    main()

items= [2, 5, 2, 7] target= 7
  head: i=0, prefix=[], invariant=True, variant=4
  head: i=1, prefix=[2], invariant=True, variant=3
  head: i=2, prefix=[2, 5], invariant=True, variant=2
  head: i=3, prefix=[2, 5, 2], invariant=True, variant=1
  result= 3
items= [2, 5, 2, 7] target= 3
  head: i=0, prefix=[], invariant=True, variant=4
  head: i=1, prefix=[2], invariant=True, variant=3
  head: i=2, prefix=[2, 5], invariant=True, variant=2
  head: i=3, prefix=[2, 5, 2], invariant=True, variant=1
  exit: i=4, invariant=True, variant=0
  result= -1
items= [4, 9, 4] target= 4
  head: i=0, prefix=[], invariant=True, variant=3
  result= 0
items= [] target= 9
  exit: i=0, invariant=True, variant=0
  result= -1
Assertions check these executions; the lesson proves the general obligations.

五十分钟：错误奇数和有一致代数步却有假基础，预测四行并解释不能启动归纳。递归跟踪故意限制展示五次，避免实验挂起；重复相同 n 表示无进展。解释展示上限不是错误递归的终止证明，以及修复倒数为何有自然数度量。

下载 lab3_faulty_arguments.py

"""Expose a missing induction base and a non-decreasing recursive measure."""


def main():
    print("Proposed identity: sum of first n odd numbers = n^2 + 1")
    for n in range(4):
        actual = sum(2 * i + 1 for i in range(n))
        candidate = n * n + 1
        step_matches = candidate + 2 * n + 1 == (n + 1) ** 2 + 1
        print(f"n={n}: actual={actual}, candidate={candidate}, proposed step consistent={step_matches}")
    print("Base at n=0 fails: 0 != 1. A valid algebraic step does not supply a base.")
    faulty_trace = [5] * 5
    correct_trace = list(range(5, -1, -1))
    print("Bounded illustration of faulty calls countdown(n):", faulty_trace)
    print("Correct calls countdown(n-1):", correct_trace)
    faulty_decreases = all(b < a for a, b in zip(faulty_trace, faulty_trace[1:]))
    correct_decreases = all(b < a for a, b in zip(correct_trace, correct_trace[1:]))
    assert not faulty_decreases and correct_decreases
    print("Natural-number measure strictly decreases:", faulty_decreases, correct_decreases)
    print("Five displayed faulty calls are a trace limit, not termination of that recursion.")


if __name__ == "__main__":
    main()

Proposed identity: sum of first n odd numbers = n^2 + 1
n=0: actual=0, candidate=1, proposed step consistent=True
n=1: actual=1, candidate=2, proposed step consistent=True
n=2: actual=4, candidate=5, proposed step consistent=True
n=3: actual=9, candidate=10, proposed step consistent=True
Base at n=0 fails: 0 != 1. A valid algebraic step does not supply a base.
Bounded illustration of faulty calls countdown(n): [5, 5, 5, 5, 5]
Correct calls countdown(n-1): [5, 4, 3, 2, 1, 0]
Natural-number measure strictly decreases: False True
Five displayed faulty calls are a trace limit, not termination of that recursion.

练习 1–12 预计 140 分钟，每题五分；两扩展额外 25 分钟。说明假设、范围与关键理由。只有空证明模板不满足义务。

九道选择自动反馈，书面证明概要自评后供第十分。答案应指出满足与尚未解决的义务。

必读二十五分钟：在 MIT Mathematics for Computer Science 链接开放教材中阅读证明方法与归纳介绍，标记假设、基础、归纳假设与目标，比较直接和间接论证。

必读十一分钟：阅读递归数据/结构归纳，关注一种有限结构的构造，列准确基础与步，指出假设应用的较小对象。

必读九分钟：阅读状态机或不变式讨论，指出观察点，分别说明状态性质与进展/终止依据。三选段总计四十五分钟，较长证明可选。

选读：官方 Python assert 文档 说明可执行断言限制。本课证明与图为原创。

证明遵循逻辑结构：全称取任意输入，存在给见证，唯一比较假设解，分段覆盖情况。归纳覆盖索引链或递归结构；程序正确性的不变式绑定程序点，终止另需良基度量。

综合早期思想的检查点：搜索请求列表第一个满足 $admin\lor(owner\land approved)$ 的条目。用模块 02 翻译谓词，把搜索不变式中的“不等于目标”改为“谓词失败”。证明返回首个合格位置，−1 表示没有合格项。解释括号错误如何改变证明的规格，即使循环本身正确。

结业任务：不看例子完成直接证明、完整归纳及搜索正确性/终止论证。练习六十、实验三十、测验十分。缺基础、循环假设、进展失败都应修正并解释。模块 05 用这些工具证明计数，而非只套公式。