什么样的策略“感应”跟随着一个数字呢？

Question

以下策略对目标和假设有何影响？我知道对变量和命名假设的归纳是什么，但我不清楚对数字的归纳。

Induction 1

Answer 1

来自Coq参考手册：https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacn.induction

（...）induction num表现为intros until num，其次是induction应用于最后引入的假设。

而对于intros until num：https://coq.inria.fr/distrib/current/refman/proof-engine/tactics.html#coq:tacv.intros

intros until num：重复介绍直到num-th非依赖产品。

Example

在子目标forall x y : nat, x = y -> y = x上，战术intros until 1相当于intros x y H，因为x = y -> y = x是第一个非依赖产品。

在子目标forall x y z : nat, x = y -> y = x上，战术intros until 1相当于intros x y z，因为z上的产品可以改写为非依赖产品：forall x y : nat, nat -> x = y -> y = x。

作为参考，手册中有一个标准策略索引，可以很容易地查找它们：https://coq.inria.fr/distrib/current/refman/coq-tacindex.html

（还有其他指数你也可能会感兴趣。）