如何证明Coq中的命题可扩展性？ [英] How can I prove propositional extensionality in Coq?

问题描述

我试图证明关于Prop的代换定理，但我失败了。可以在coq中证明以下定理，如果不能，则为什么呢？

I'm trying to prove a substitution theorem about Prop, and I'm failing miserably. Can the following theorem be proven in coq, and if not, why not.

  Theorem prop_subst:
    forall (f : Prop -> Prop) (P Q : Prop), 
      (P <-> Q) -> ((f P) <-> (f Q)).

重点是逻辑上的证明是归纳法。据我所知，道具没有归纳定义。

The point is that the proof, in logic, would be by induction. Prop isn't defined inductively, as far as I can see. How would such a theorem be proven in Coq?

推荐答案

在这里，答案是：我要寻找的属性称为命题可扩展性，表示 forall pq：Prop，（p<-> q）-> （p = q）。相反，是微不足道的。这是在 Library Coq.Logic.ClassicalFacts 中定义的，以及来自古典（即非直觉逻辑）的其他事实。上面的定义称为 prop_extensionality ，可以按以下方式使用：公理EquivThenEqual：prop_extensionality 。现在您可以应用 EquivThenEqual ，将其用于重写等。感谢Kristopher Micinski指出了可扩展性。

Here's the answer: The property I was looking for is called propositional extensionality, and means that forall p q : Prop, (p <-> q) -> (p = q). The converse, is trivial. This is something that is defined in Library Coq.Logic.ClassicalFacts, together with other facts from classical, i.e., non-intuitionistic logic. The above definition is called prop_extensionality, and can be used as follows: Axiom EquivThenEqual: prop_extensionality. Now you can apply the EquivThenEqual, use it for rewriting, etc. Thanks to Kristopher Micinski for pointing towards extensionality.

这篇关于如何证明Coq中的命题可扩展性？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！