如何证明Coq中的命题扩展性？

Question

我试图证明一个关于道具的替代定理,而且我失败了.可以在coq中证明以下定理,如果不是,为什么不.

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

关键是逻辑上的证据是归纳的.就我所见,Prop没有归纳定义.如何在Coq中证明这样的定理？

Answer 1

这就是答案:我所寻找的属性称为命题扩展性,意味着forall p q : Prop, (p <-> q) -> (p = q).相反,是微不足道的.这是Library Coq.Logic.ClassicalFacts与经典(即非直觉主义)逻辑中的其他事实一起定义的内容.调用上述定义prop_extensionality,可以按如下方式使用:Axiom EquivThenEqual: prop_extensionality.现在你可以应用它EquivThenEqual,用它来重写等等.感谢Kristopher Micinski指向扩展性.

Answer 2

您正在寻找的称为“外延性：”

http://coq.inria.fr/V8.1/faq.html#htoc41

http://coq.inria.fr/stdlib/Coq.Logic.FunctionalExtensionality.html

http://en.wikipedia.org/wiki/Extensionality

编辑：

您可以承认谓词外延性，如 Coq FAQ 中所述。