Coq：评估/简化 `Prop` 重言式答案

【问题标题】：Coq: evaluating/simplifying `Prop` tautologiesCoq：评估/简化 `Prop` 重言式
【发布时间】：2021-03-16 05:44:49
【问题描述】：

我在 Coq 中证明了一些关于超滤器的基本事实，我的许多证明最终都到了我必须证明一个目标的阶段，例如

(False -> False) = True

或

False /\ P = False

或

True

或其他一些琐碎的重言式。 simpl 和 auto 似乎都没有做任何事情，那么我该如何解决这些 Prop 目标呢？

【问题讨论】：

如果你得到了这样的目标，你通常在你提出问题的方式上做了一些“错误”的事情。正如@Meven 建议的那样，尝试重新表述问题，以便使用<-> 而不是= 来比较命题真理。
为了将来参考，如果你用逻辑等价<->替换等式=，那么你可以用tauto策略证明命题重言式。

标签： coq theorem-proving

【解决方案1】：

我不确定您是如何编码超滤器的，但您的前两个目标无法证明。事实上，他们断言不同类型之间的相等性，这在 vanilla Coq 中无法证明。然而，有多种不同的方法可以解决这个问题。

最简单（在我看来也是最好的）解决方案是在所有定义中用逻辑等价替换命题的相等性。例如，在您的第一种情况下，您将获得(False -> False) <-> True，这确实是一个重言式。

或者，您可以完全用布尔值替换命题，即在超滤器的定义中使用bool 而不是Prop，并依靠布尔连接词而不是命题连接词。你的第二种情况会变成false && P = false 之类的东西，这又是可证明的，因为你正在处理归纳类型的元素之间的相等性，而不是命题之间的相等性。但是这种变化比以前的变化要重得多，因为它意味着对你的开发进行更多的更改，以使用布尔而不是命题进行推理。如果你走这条路，你可能想看看 MathComp，它在这种设置中与布尔值一起发挥了很多作用。

最后一种可能性有点棘手，它依赖于所谓的命题外延性公理，即只要两个命题等价，它们就等价。在 Coq 中，它对应于

prop_ext : forall P Q : Prop, (P <-> Q) -> P = Q.

使用此公理，您可以将各种平等目标简化为等价，正如第一个解决方案中提到的那样。一个类似的公理出现在同伦类型理论 (HoTT) 的上下文中，这是由于单价公理的核心，尽管 Coq 和 HoTT 中的命题概念有些不同。如果您对相等和等价之间的区别感到好奇，您可能想检查一下，这就是我提到它的原因，但我建议您改用第一个解决方案，因为它避免了依赖不必要的公理。

【讨论】：

我明白你的意思，但严格来说，Coq 中的命题外延性并不是单价的结果，因为 HoTT 和 Coq 中的命题是不同的东西：第一个是 Type 上的结构，而第二种是特殊类型。命题外延比完全单价更基本，我认为使用前者而不理解后者是可以的。
对，我想指出一个方向，您可以在其中找到有关命题外延性的更多信息，而忽略了这种差异。我将编辑我的答案以明确这一点。
我将集合编码为函数nat -> Prop，并将（超）过滤器编码为函数set -> Prop。我最初使用 bool 而不是 Prop，但后来我看不到如何定义 Frechet 过滤器：Example Frechet : family := fun A => exists n:nat, forall m:nat, m>n -> m in A.
确实，你不能这样做，因为函数(nat -> bool) -> bool 表示一个可判定的超滤器，而 Frechet 滤波器是不可判定的，因为你通常无法判定给定的函数是否最终总是是的。