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

Question

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

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

关键是，在逻辑上，证明将是归纳法。据我所知，道具不是归纳定义的。如何在 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 中所述。

Answer 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.