为什么“专门化”在证明中不是无效策略？

Question

在软件基础书籍（已存档）中，引入了

specialize

策略作为简化假设的一种方法。

我不明白，为什么这是证明中的有效步骤。

提供的示例增加了我的困惑：

Theorem specialize_example: forall n,
     (forall m, m*n = 0)
  -> n = 0.
Proof.
  intros n H.
  specialize H with (m := 1).
  simpl in H.
  rewrite add_comm in H.
  simpl in H.
  apply H. Qed.

当我将假设

(forall m, m*n = 0) -> n = 0.

替换为

1*n = 0 -> n = 0.

时，我发现我们现在正在成功证明

n=0

这个新假设。

我不明白为什么这被接受为原始定理的证明

forall n, (forall m, m*n = 0) -> n = 0.

。我们现在不是在继续证明一个新定理吗

forall n, 1*n = 0 -> n = 0.

？

新定理的证明如何推广为原定理的有效证明？

---

文本将

specialize

策略描述为 “本质上只是

assert

和

apply

”的组合。
也许使用

specialize

和

assert

而不是

apply

将这个证明脚本（或使用

specialize

的另一个示例）重写为另一个证明脚本可能会解决问题。

Answer 1

[我宁愿将其作为评论发布，但我对此仍然太新了。]

我不愿意回答你问题的第一部分，以免破坏练习：逻辑基础尤其是一个旅程和一个进展，而不是食谱纲要，以及该练习的智力组成部分，但不要破坏它，我认为至关重要。

至于你对这种变换的有效性的怀疑，也许我明白你的意思：如果我们要证明一个应该对所有 n 都成立的定理，那么我们怎么能只对某些 n 证明它呢？但现在请注意，我们上面专门讨论的并不是 n，那么如果您还思考应用假设是如何工作的......