问在Coq中，“归纳”n、“m”和“归纳n”的区别是什么？

EN

我很难让induction n, m为n和m创建归纳假说，但经过一些尝试，情况似乎并非如此。顺便说一句，我假设是forall (n m : nat)。

那么，induction n, m induction n. induction m和induction n; induction m的区别是什么呢？

以下是我目前的理解：

我知道;是一个组合子，所以a; b可以在a生成的每个子目标上回放b，所以induction n; induction m会为induction n的每个子目标生成m的诱导低幂，对吗？

从同样的意义上说，induction n. induction m只会为当前的目标产生感应功能低下，因此这似乎并不特别有用。

我希望induction n, m就像在这两个变量上一样，它为自然数生成四个目标，就像我预期的那样，但是我希望IHm在第四个目标上，但是它不是！我错过了什么？

--

还在对此进行研究，似乎IHm在第四个目标上被IHn合并了，这是正确的吗？

-编辑2

下面是一些基于加法交换性的例子

因此，首先是induction n, m版本：

Example add_comm' : forall (n m : nat), n + m = m + n.
  intros. induction n, m; try auto using plus_n_O.

这解决了琐碎的3个第一个目标，给我留下了第四个目标

n, m : nat
IHn : n + S m = S m + n

========================= (1 / 1)

S n + S m = S m + S n

现在是induction n; induction m版本：

n, m : nat
IHn : n + S m = S m + n
IHm : n + m = m + n -> S n + m = m + S n

========================= (1 / 1)

S (n + S m) = S (m + S n)

因此，对于这个特殊情况，induction n, m更好，但我无法解释(也无法理解)它在做什么。

在手册中，,在归纳中的唯一情况是

变体induction term+, using qualid 这个语法用于大小写，qualid表示带有复杂谓词的归纳原则，因为函数或函数式可能产生的归纳原则。

但是我不使用using qualid，所以我不确定是否是这样

-编辑3 --

正如Andrey在其评论中所说的，using qualid变体是被触发的，但我不知道它所做的解释是什么。