Coq中_the_hidden_goal_错误含义及解决原理疑问

我来帮你理清这个问题的核心原因——其实是ssreflect导入后改变了Coq策略的默认行为，而你的原文件（来自Software Foundations）应该没有导入mathcomp的ssreflect库，所以两者行为不一致。

问题背景回顾 #

你的代码里，在destruct (string_dec x y) as [H |Hs]的第二个分支：

• 上下文里的Hs是x <> y（来自string_dec的sumbool返回类型）
• 当前子目标是x = y -> eqb_string x y = true，展开eqb_string后实际等价于x = y -> False（因为这个分支里string_dec x y为false，所以eqb_string x y是false，要证x=y推导出false=true，本质是要构造矛盾）

当你写intros H后，H是x = y，接下来尝试rewrite H in Hs想把Hs里的x换成y，得到y <> y（即False），然后destruct Hs就能完成证明。

为什么rewrite H in Hs会报错？ #

因为你导入了mathcomp的ssreflect库，它修改了Coq中rewrite策略的默认规则：

• 在标准Coq（无ssreflect）中，rewrite H in Hs只会修改假设Hs，不管目标是否依赖它。
• 但在ssreflect模式下，Coq会跟踪假设和目标之间的依赖关系。如果某个假设被目标间接依赖（比如这里的Hs是用来反驳H的关键前提，目标隐含依赖Hs来产生矛盾），直接单独修改这个假设会被判定为不安全，于是抛出错误：Hs is used in hypothesis _the_hidden_goal_。

为什么rewrite H in Hs *能解决问题？ #

*是ssreflect的语法扩展，它表示：将rewrite操作应用到所有相关的假设（包括那些被目标引用的假设）。

• 加上*后，Coq会同时处理Hs以及目标中依赖Hs的部分，确保修改后上下文和目标的一致性。
• 执行后Hs会变成y <> y（即False），此时destruct Hs就能直接消除这个矛盾子目标。

替代方案 #

如果你不想用ssreflect的*语法，也可以用标准Coq的方式调整策略顺序，比如先保留原始假设再修改：

intros H. pose proof Hs as Hs'. rewrite H in Hs'. destruct Hs'.

不过显然rewrite H in Hs *是最简洁的ssreflect风格解决方案。

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