coq - 如何证明 Coq 中的命题外延性？

Question

我试图证明一个关于 Prop 的替代定理，但我失败了。下面的定理能否在 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 指出可扩展性。