问题描述
我正在证明 Coq 中有关超滤器的一些基本事实，并且我的许多证明最终都到了必须证明目标的阶段，例如
(False -> False) = True
或
False /\ P = False
或
True
或其他一些琐碎的同义反复。 simpl 和 auto 似乎都没有做任何事情，那么我该如何解决这些 Prop 目标？
解决方法
我不确定您是如何对超滤器进行编码的，但您的前两个目标无法证明。事实上，他们断言不同类型之间的相等性，这在普通 Coq 中无法证明。然而，有多种不同的方法可以解决这个问题。
最简单（在我看来也是最好的）解决方案是在所有定义中用逻辑等价代替命题的等价。例如，在您的第一种情况下，您将获得 (False -> False) <-> True，这确实是一个重言式。
或者，您可以完全用布尔值替换命题，即在定义超过滤器中使用 bool 代替 Prop，并依赖布尔连接词而不是命题连接词。你的第二种情况会变成类似 false && P = false 的东西，这又是可证明的，因为你处理的是归纳类型元素之间的相等性，而不是命题之间的相等性。但是这个变化比前一个更重要，因为它意味着你的发展会有更多的变化，以使用布尔值而不是命题进行推理。如果你走这条路，你可能想看看 MathComp，它在这种设置中经常使用布尔值。
最后一种可能性有点棘手，它依赖于所谓的命题外延公理，即两个命题只要等价就相等。在 Coq 中，它对应于
prop_ext : forall P Q : Prop,(P <-> Q) -> P = Q.
使用这个公理，您可以将各种平等目标简化为等价，正如第一个解决方案中提到的那样。类似的公理出现在同伦类型理论 (HoTT) 的上下文中，这是其中核心的单价公理的结果，尽管 Coq 和 HoTT 中的命题概念有些不同。如果您对等式和等价之间的区别感到好奇，您可能想检查一下，这就是我提到它的原因，但我建议您使用第一个解决方案，因为它避免了依赖不必要的公理。>