Coq中induction n,m与induction n; induction m的区别是什么？

1. induction n. induction m #

你的理解完全正确：.是Coq的战术结束符，执行完induction n后，Coq默认聚焦到它生成的第一个子目标（也就是n=0的分支），后续的induction m只会作用在这个单个子目标上，induction n生成的其他子目标（比如n为后继的分支）里的m不会被做归纳处理，所以这个写法除非你刻意要只处理第一个子目标，否则确实实用性很低。

2. induction n; induction m #

你的理解也完全正确：;是Coq的战术组合子，语义是「对前一个战术生成的所有子目标，依次执行后一个战术」。所以induction n会生成2个子目标（n=0、n=S n'带IHn），每个子目标都会再执行induction m，每个induction m又生成2个子目标，总共4个子目标。在后继对后继的分支里，你会得到两个独立的归纳假设IHn和IHm，对应两次独立的归纳步骤。

3. induction n, m #

这个是你疑惑的核心，它的实际行为和前两个完全不同：

• 你确实触发了手册里提到的多参数induction变体：

手册里对应语法的说明为：
Variant induction term+, using qualid
该语法适用于qualid指向带复杂谓词的归纳原则的场景，比如Function或Functional Scheme生成的归纳原则。
就算你没有写using qualid，Coq也会根据逗号分隔的变量的类型，自动推导对应的多元归纳原则，对于两个nat类型的变量来说，Coq自动选择的是二元自然数归纳原则nat_ind2，它的定义如下：

nat_ind2 : forall P : nat -> nat -> Prop,
  P 0 0 ->
  (forall m, P 0 (S m)) ->
  (forall n, P (S n) 0) ->
  (forall n m, P n m -> P (S n) (S m)) ->
  forall n m, P n m

• 这个归纳原则刚好生成你看到的4个子目标，但是第四个后继对后继的分支里，只会有一个归纳假设，也就是P n m（对应当前的(S n, S m)更小的配对(n, m)的命题成立），Coq自动给它起名为IHn，不存在独立的IHm，所以“IHm被合并到IHn里”的说法不准确，不是合并，而是这个二元归纳原则本身就只提供这一个归纳假设。
• 你在加法交换律的例子里觉得它更好用，是因为这个场景下你刚好只需要这个配对的归纳假设，不需要多余的IHm，所以上下文更简洁，证明步骤更少。

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