Coq中dependent induction/destruct战术的作用、用法及适用场景详解

适用场景 #

当你遇到以下情况时，普通的induction或destruct无法搞定，就得用上这两个战术：

• 命题的结论类型直接依赖某个归纳类型的项，比如要证明forall v : vector A n, R v n（vector的长度是n，结论R同时关联v和n）；
• 前提里有等式把归纳项和其他变量绑定，比如forall l : list A, length l = 3 -> Q l，此时拆分list l时，length l的信息会和前提里的3绑定，普通destruct会丢失这种关联。

简单来说：只要你的证明目标里，某个归纳项的“类型参数”和目标/前提里的变量绑定在一起，普通战术搞不定时，就考虑用这俩。

工作原理 #

普通的induction/destruct只会对归纳项本身做模式匹配，但当结论类型依赖这个归纳项时，匹配后的分支里，结论的类型不会自动跟着调整，导致类型不兼容报错。

而dependent induction/dependent destruct的核心是同步处理归纳项和依赖它的类型部分：

• 拆分归纳项时，会自动更新所有和它绑定的变量、结论里的类型参数，确保整个目标的类型始终合法；
• 比如对vector A n做dependent destruct，拆成cons A a v'时，n会自动替换成S n'，前提或结论里所有用到n的地方也会同步更新，不会出现“预期n是S n'但实际是n”的类型错误。

两者的区别：

• dependent destruct只做拆分，不生成归纳假设，适合不需要递推的分支证明；
• dependent induction会生成对应的归纳假设，适合需要用递推逻辑的证明（比如归纳法证明）。

dependent induction的具体功能与使用方法 #

核心功能 #

它是induction的依赖类型增强版，专门用于带依赖关系的归纳证明：自动生成正确的归纳假设，同时全程维护归纳项与类型参数的绑定关系，避免类型错误。

基础用法 #

1. 直接归纳：dependent induction <归纳项>
   比如你要归纳的依赖项是v : vector bool n，直接执行dependent induction v，Coq会自动处理所有依赖绑定，生成对应的归纳分支和假设。

2. 自定义归纳假设名称：dependent induction <归纳项> as <模式>
   如果你想给归纳假设起个好记的名字，比如dependent induction v as [|a v' IH]，其中IH就是归纳假设的名称，后续证明里可以直接引用它。

3. 结合前提处理：dependent induction <归纳项> in <前提>
   如果有前提（比如H : n = 2）和归纳项绑定，加上in H可以让Coq同步更新前提里的绑定信息，避免前提失效。

示例演示 #

假设当前目标是：

n : nat
v : vector bool n
H : n = 2
______________________________________(1/1)
exists b1 b2 : bool, v = cons bool b1 (cons bool b2 (nil bool))

执行dependent induction v后，Coq会自动生成两个分支：

• 分支1：v是nil bool，此时n被自动替换为0，结合前提H: 0 = 2，Coq会自动识别矛盾，直接完成这个分支；
• 分支2：v是cons bool b1 v'，此时n变成S n'，前提H同步更新为S n' = 2（即n' = 1），接着对v'做归纳拆分，得到v' = cons bool b2 (nil bool)，此时直接构造exists b1 b2即可完成证明。

内容的提问来源于stack exchange，提问作者blonded04