在Coq中提供示例，其中(A B:Prop)，P:Prop->键入，以使A<-> B，但不能用P B代替P A [英] Provide example in Coq where (A B: Prop), P: Prop -> Type, such that A <-> B, but one cannot replace P A with P B

问题描述

按照标题的要求，我希望举一个例子:

As the title asks, I wish for an example where:

Section Question:
Definition A: Prop := <whatever you like>.
Definition B:Prop := <whatever you like>.
Definition/Inductive/Fixpoint P: Prop -> Type := <whatever you like>.

Theorem AEquivB: A <-> B.
Proof. <supply proof here>. Qed.

(* Question 1. can we pick a P, A, B to prove this? *)
Theorem PA_not_equals_Pb: P A <> P B.
Proof. <supply proof here>. Qed.

(* Question 1.5. can we pick a P, A, B to prove this? *)
Theorem PA_not_equiv_PB: ~(P A <-> P B)
Proof. <supply proof here>. Qed.  

总的来说，我很想了解等价证明"在某种意义上是否足以等同"用作平等"，或者是否存在可以使用P A和A <-> B的情况，但不是 P B.

In general, I am interested to understand whether "proof equivalence" is "good enough" to be used as "equality" in a sense, or whether there are situations where we can have P A, and A <-> B, but not P B.

推荐答案

forall A B : Prop, (A <-> B) -> A = B与Coq一致. (也就是说，您可以将其添加为公理，并且该理论不会崩溃.)该公理称为命题可扩展性.正如A = B快速给出forall P : Prop -> Prop, P A <-> P B一样，没有术语P，A，B这样的(A <-> B) /\ ~(P A <-> P B)，因为这将与公理相抵触，但是我们知道它是一致的.同样，我们也很快得到P A = P B，这意味着我们也不能得到P A <> P B.请注意，即使不存在违反命题扩展性的P，A，B，我们仍然不能证明命题扩展性. Coq根本没有能力谈论自己(这很好，因为这意味着您可以对其进行自定义)，这就是为什么如果需要的话，需要添加命题可扩展性作为公理.

It is consistent with Coq that forall A B : Prop, (A <-> B) -> A = B. (That is, you can add this as an axiom and the theory won't collapse.) This axiom is called propositional extensionality. As A = B quickly gives forall P : Prop -> Prop, P A <-> P B, there are no terms P, A, B such that (A <-> B) /\ ~(P A <-> P B), since this would contradict the axiom, but we know it is consistent. Similarly, we also quickly get P A = P B, which means we cannot also get P A <> P B. Note that even though such P, A, B that violate propositional extensionality do not exist, we still cannot prove propositional extensionality. Coq simply doesn't have the strength to talk about itself like that (which is good, since that means you can customize it), which is why propositional extensionality needs to be added as an axiom if you want it.

这篇关于在Coq中提供示例，其中(A B:Prop)，P:Prop->键入，以使A<-> B，但不能用P B代替P A的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！