为何Coq中的specialize tactic是合法的证明步骤？

在《Software Foundations》一书中，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，但这难道不是在证明一个新定理吗？这种证明怎么能推广到原定理？

核心逻辑：全称命题的实例化与蕴含传递性 #

specialize的合法性，本质基于两个基础逻辑规则：

1. 全称实例化：如果全称命题∀x, P(x)成立，那么对任意具体取值t，P(t)必然成立。
2. 蕴含传递性：如果A → B且B → C，那么A → C。

放到这个例子里拆解：

• 首先通过intros n H拿到任意的n和全称假设H: ∀m, m*n=0。
• specialize H with (m:=1)是对全称假设做实例化：既然H断言所有m都满足m*n=0，那取m=1时，1*n=0必然成立——这一步完全符合逻辑，只是从原假设中提取了它蕴含的具体结论，没有添加或删减条件。
• 接下来我们证明的是从1*n=0可以推出n=0，结合前面的结论「从H可以推出1*n=0」，通过蕴含传递性，自然就能得到「从H可以推出n=0」——这正是原定理要证的结论。

通俗类比理解 #

假设你要证：「如果所有城市都下雨，那么北京会积水」。
你不需要直接对着「所有城市下雨」这个大前提来证，而是可以：

1. 先从「所有城市都下雨」推出「北京下雨」；
2. 再证明「如果北京下雨，那么北京会积水」；
3. 最后结合这两步，就能得出「如果所有城市都下雨，那么北京会积水」。

这里的specialize就相当于第一步，把全称的「所有城市」缩小到具体的「北京」，但整个推理链条完全严谨，并没有改变原命题的要求。

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