为什么嵌套归纳策略也将归纳假设嵌套在 lambda 下？

Question

Theorem mult_comm : forall m n : nat,
  m * n = n * m.
Proof.
intros.
induction n.
- simpl. rewrite (mult_0_r m). reflexivity.
- simpl.
  rewrite <- IHn.
  induction m.
    simpl. reflexivity.
    simpl.

以上内容来自软件基金会第二章。

1 subgoal
m, n : nat
IHn : S m * n = n * S m
IHm : m * n = n * m -> m * S n = m + m * n
______________________________________(1/1)
S (n + m * S n) = S (m + (n + m * n))

我真的很困惑IHm 应该在这里。按照我的理解，Coq 策略在后台编译为一些功能程序，但我真的不确定这里发生了什么。我很确定这不是我的本意。

我想做的是类似于下面的 Idris 程序。

add_comm : {a,b : Nat} -> a + b = b + a
add_assoc : {a,b,c : Nat} -> (a + b) + c = a + (b + c)

total
mult_comm : {m,n : Nat} -> (m * n) = n * m
mult_comm {m = Z} {n = Z} = Refl
mult_comm {m = Z} {n = (S k)} = mult_comm {m=Z} {n=k}
mult_comm {m = (S k)} {n = Z} = mult_comm {m=k} {n=Z}
mult_comm {m = (S k)} {n = (S j)} = 
    let prf1 = mult_comm {m=k} {n=S j}
        prf2 = mult_comm {m=S k} {n=j}
        prf3 = mult_comm {m=k} {n=j}
        prf_add_comm = add_comm {a=k} {b=j}
        prf_add_assoc = add_assoc {a=k} {b=j} {c=j*k}
        prf_add_assoc' = add_assoc {a=j} {b=k} {c=j*k} 
    in
        rewrite prf1 in
        rewrite sym prf2 in
        rewrite prf3 in
        rewrite sym prf_add_assoc in
        rewrite sym prf_add_assoc' in
        rewrite (add_comm {a=k} {b=j}) in
        Refl

更具体地说，我需要 prf1、prf2 和 prf3，这是我使用对 mult_comm 的递归调用获得的。在 Coq 中，这两个证明被困在一个 lambda 中，我不确定这是怎么发生的。我看到 Coq 的 induction 策略没有做我认为应该做的事情。

除了上面的解释之外，我还想问一下 Coq 的介绍材料是否比 Software Foundations 多，以防我在某些策略上再次陷入这种困境？请注意，我知道如何在 Coq 中解决这个问题，因为我在网上找到了解决方案。

早在 2016 年，我就曾尝试将 SF 书作为依赖类型编程的介绍来解决，但现在事后看来，我发现 Little Typer 和 Idris 书在这方面要好得多。

Answer 1

当您调用induction 策略时，Coq 使用启发式方法来确定您想要通过归纳证明的谓词P : nat -> Prop。在第二次调用induction之前，证明状态是这样的：

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

发生的事情是，Coq 决定在归纳谓词中包含前提 IHn，从而推断为

P m := m * n = n * m -> m * S n = m + m * n

这正是您在归纳假设中所拥有的。在这种情况下，您可能会说 Coq 使用该前提是愚蠢的，但在某些情况下，放弃它会导致无法证明的目标。例如，考虑以下证明尝试：

Lemma double_inj : forall n m, n + n = m + m -> n = m.
Proof.
  intros n m H.
  induction n as [|n IH].
  (* ... *)

如果在调用induction 后H 被丢弃，则您必须证明forall n m, n = m，这显然不成立。

这个例子是为什么在一个 Coq 证明中多次调用 induction 经常是一个坏主意的原因之一。正如我们在软件基础练习中建议的那样，最好证明一个辅助引理，因为您可以明确地了解归纳谓词。对于此示例，还有其他选项。例如，您可以调用 clear IHn 来删除 IHn 前提，这将导致 Coq 找到正确的谓词。现在随 Coq 一起提供的 ssreflect 证明语言有一种不同的策略来执行归纳，称为 elim，它允许您更明确地选择谓词。

我同意您的最终评论，但我应该补充一点，软件基础的目标不是介绍依赖类型编程。尽管 Coq 支持这种范式，但是直接编写这样的程序通常很麻烦，并且使用策略来证明简单类型程序的引理要容易得多。例如，您的 mult_comm 证明被 Idris 接受，因为它的终止检查器足够聪明，可以将所有递归调用识别为递减，即使它们相对于固定参数没有递减（在第二个子句中，n 递减，而在第三个m 中是这样）。这在 Coq 中是不可能的，您必须将定义拆分为多个递归函数，每个参数一个，或者对自然数对使用有根据的归纳法，这对于本示例来说是多余的。

Adam Chlipala 有另一本名为 CPDT 的 Coq 教科书，您可能想看看。但是，我认为您也不会在那里找到对 Coq 策略的全面描述。像induction 一样，很多策略都依赖于启发式，很难详细解释。

最后一点，Matthieu Sozeau 开发了一个名为 Equations 的包，它使 Coq 中的依赖类型编程更接近于 Idris 或 Agda。如果您发现这种证明方式更直观，可以尝试使用它。