如何在 Coq 中证明命题外延性？答案

【问题标题】：How can I prove propositional extensionality in Coq?如何在 Coq 中证明命题外延性？
【发布时间】：2012-06-17 12:08:35
【问题描述】：

我正在尝试证明关于 Prop 的替换定理，但我失败了。下面的定理能否在 coq 中被证明，如果不能，为什么不能。

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

关键是逻辑上的证明将是归纳法。据我所知，道具不是归纳定义的。如何在 Coq 中证明这样的定理？

【问题讨论】：

我不认为你可以证明这一点，但我不知道细节......
我可以将它添加为公理，但这有点粗俗，不是吗？
@MayerGoldberg 抱歉，您的问题看得太快了 ;-)

标签： coq

【解决方案1】：

答案如下：我正在寻找的属性称为命题扩展性，意思是forall p q : Prop, (p <-> q) -> (p = q)。反之，微不足道。这是在Library Coq.Logic.ClassicalFacts 中定义的东西，以及来自经典的其他事实，即非直觉逻辑。上面的定义叫做prop_extensionality，可以这样使用：Axiom EquivThenEqual: prop_extensionality。现在您可以申请 EquivThenEqual，将其用于重写等。感谢 Kristopher Micinski 指出可扩展性。

【讨论】：

该死的，你打败了我 ;-)，我正要向你指出常见问题解答中的部分
当您自己的答案最合适时，您可以通过将您的答案标记为已接受来帮助我学习 Coq。你会得到声望点。不要害羞——Stack Overflow 就是这样工作的。

【解决方案2】：

你要找的东西叫做“extensionality：”

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 常见问题解答中所述。

【讨论】：

我不认为这是扩展性：请注意，我只使用一个函数（用作上下文），而不是两个函数，就像扩展性一样。我想要的是所谓的参照透明性：如果 A B，那么我应该能够在任何表达式中用 B 代替 A，而不是任何包含 A 的表达式。另一方面，也许你的意思是“命题外延”，即'不一样，但似乎给了我想要的。

【解决方案3】：

这是命题外延性。

Lemma blah: forall (P Q: Prop), (forall (f:Prop -> Prop), f Q -> f P) -> P = Q.
  intros P Q H.
  apply (H (fun x => x = Q)).
  reflexivity.
Qed.

Section S.

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

Lemma prop_subst_is_ext: forall P Q, (P <-> Q) -> P = Q.
  intros.
  apply blah.
  intro f.
  destruct (prop_subst f P Q); assumption.
Qed.

End S.

Check prop_subst_is_ext.

【讨论】：