Coq入门疑问：为何无法弱化目标？

核心问题在于：ax作为归纳类型，其上下文参数是严格匹配的，Coq不会默认认为“小上下文里成立的命题，扩展上下文后也成立”。你手里的假设H: ax Gamma (Impl alpha beta)和子目标ax (alpha :: Gamma) (Impl alpha beta)是两个不同的命题，参数Gamma和alpha::Gamma不匹配，所以exact H必然失败。

你的直觉是对的：如果一个公式在上下文Gamma中可证（或作为公理/假设成立），那么给上下文新增公式后，这个公式肯定还是成立的。但这个“上下文弱化”的性质不是Coq自动提供的，你需要手动证明对应的引理。

解决步骤 #

1. 证明弱化引理
   先定义一个引理，描述“扩展上下文后ax命题仍然成立”的性质：

   Lemma weaken_ax : forall Gamma phi alpha, ax Gamma phi -> ax (alpha :: Gamma) phi.
   

   这个引理需要通过对ax的归纳定义进行证明——因为ax是归纳类型，归纳法是处理这类结构的标准手段。假设你的ax是希尔伯特风格的公理/假设判断，证明大概长这样：

   Proof.
     intros Gamma phi alpha H.
     induction H.
     - (* 假设情况：原上下文包含phi，扩展后也包含 *)
       apply AxHyp. left. reflexivity.
     - (* 公理情况：直接应用对应的公理构造子，因为公理对任意上下文都成立 *)
       apply AxImpl1. (* 替换成你定义里的公理构造子 *)
     - (* 其他公理情况同理，直接复用构造子即可 *)
       apply AxImpl2.
   Qed.
   

2. 在原证明中使用引理
   回到你的主证明，当你得到子目标ax (alpha :: Gamma) (Impl alpha beta)和假设H: ax Gamma (Impl alpha beta)时，先把H转换成扩展上下文版本：

   apply weaken_ax in H.
   

   现在H的类型变成了ax (alpha :: Gamma) (Impl alpha beta)，和子目标完全匹配，直接用exact H就能完成这个子目标了。

补充说明 #

这是Coq中处理上下文相关归纳类型的常见模式——很多我们直觉上“显然”的元理论性质（比如弱化、收缩、置换），都需要手动证明对应的引理，因为Coq的类型系统是严格的，不会自动推导这些跨上下文的性质。

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