如何证明或伪造“`forall (P，q:支柱)，(P -> Q) -> (Q -> P) -> P=q.”？

Question

我想在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.。这是我的方法。

Inductive True2 : Prop :=
 | One : True2
 | Two : True2.

Lemma True_has_one : forall (t0 t1 : True), t0 = t1.
Proof.
  intros.
  destruct t0. destruct t1.
  reflexivity.
Qed.

Lemma not_True2_has_one : (forall (t0 t1 : True2), t0 = t1) -> False.
Proof.
  intros.
  specialize (H One Two).
  inversion H.

但是，inversion H什么也不做。我认为这可能是因为coq证明了独立性(我不是以英语为母语的人，我不知道确切的单词，请原谅我的无知)，coq使得证明1=2 ->假是不可能的。但是，如果是这样的话，为什么还要消除证据的内容呢？

没有上面的命题，我就无法证明下面的命题或它们的否定。

Lemma True_neq_True2 : True = True2 -> False.

Theorem iff_eq : forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.

所以我的问题是：

1. 如何或是否有可能在Coq中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.？
2. 为什么inversion H什么也不做；这是因为Coq的证明是独立的，如果是的话，为什么Coq在做这件事时浪费能量。

Answer 1

1. 您提到的原则，forall P Q : Prop, (P <-> Q) -> P = Q，通常被称为命题可拓性。这个原理在Coq的逻辑中是不可证明的，最初的逻辑设计是为了使它可以作为一个公理来添加，而不会有任何伤害。因此，在标准库(Coq.Logic.ClassicalFacts)中，人们可以找到许多关于这一原则的定理，并将其与其他著名的经典推理逻辑原理联系起来。令人惊讶的是，recently发现Coq的逻辑不符合这一原则，但原因非常微妙。这被认为是一个错误，因为逻辑是设计出来的，这样就可以将其作为一个公理来添加，而不会造成任何伤害。他们想在新版本的Coq中解决这个问题，但我不知道它的当前状态是什么。在8.4版中，命题扩展性在Coq中是不一致的。 无论如何，如果在Coq的未来版本中修复了这个错误，就不可能在Coq中证明或否定这一原则。换句话说，Coq团队希望这个原则独立于Coq的逻辑。
2. inversion H没有在那里做任何事情，因为关于证明的推理规则(类型是Prop的事物)与关于非证明的推理规则(类型是Type)是不同的。你可能知道Coq中的证明是公正的。在这个框架下，inversion本质上构建了以下术语： 定义true_not_false :真<>假:=有趣H =>匹配H in _=b返回如果b，则true else with eq_refl => i结束。 如果您试图对bool在Prop中的一个版本进行同样的处理，您将得到一个更多信息的错误： 归纳Pbool :支持:= \ Ptrue : Pbool = Pfalse : Pbool。Fail Ptrue_not_Pfalse : Ptrue <> Pfalse :=趣味H =>匹配H in _=b返回如果b，则True else False with eq_refl => i结束。(*命令确实失败了，消息是：*) (* =>错误：*) (*不正确地删除归纳类型“Pbool”中的"b“：*) (*返回类型具有排序" type”，而它应该是"Prop“。*) (*消除排序支持*的归纳对象*) (*不允许在排序类型*中的谓词上删除) (*因为证据只能在构建证明时才能消除。*) 事实上，其中一个原因是Coq被设计成与另一个被称为证据无关的原则兼容(我认为这就是你所说的“证据独立性”的意思)。