equality - 如何或可能在 Coq 中证明或伪造 `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` ？

Question

我想证明或证伪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使得无法证明One = Two -> False。但如果是这样，为什么 coq 必须删除证明的内容呢？

没有上述命题，我无法证明以下命题或其否定。

Lemma True_neq_True2 : True = True2 -> False.

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

所以我的问题是:

1. 如何或是否有可能证明或证伪 forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.在 Coq 中？
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 中不一致。

   无论如何，如果这个 bug 在 Coq 的 future 版本中被修复，那么在 Coq 中应该无法证明或反驳这个原理。换句话说，Coq 团队希望这个原则独立于 Coq 的逻辑。

2. inversion H在那里不做任何事情，因为推理证明(类型为 Prop 的事物)的规则与推理非证明(类型为 Type 的事物)的规则不同。您可能知道 Coq 中的证明只是术语。在引擎盖下，inversion本质上是构建以下术语:

   Definition true_not_false : true <> false :=
     fun H =>
       match H in _ = b
               return if b then True else False
       with
       | eq_refl => I
       end.
   

   如果您尝试对 bool 版本执行相同操作在Prop ，您会得到一个信息更丰富的错误:

   Inductive Pbool : Prop :=
   | Ptrue : Pbool
   | Pfalse : Pbool.
   
   Fail Definition Ptrue_not_Pfalse : Ptrue <> Pfalse :=
     fun H =>
       match H in _ = b
               return if b then True else False
       with
       | eq_refl => I
       end.
   
   (* The command has indeed failed with message: *)
   (* => Error: *)
   (*    Incorrect elimination of "b" in the inductive type "Pbool": *)
   (*    the return type has sort "Type" while it should be "Prop". *)
   (*    Elimination of an inductive object of sort Prop *)
   (*    is not allowed on a predicate in sort Type *)
   (*    because proofs can be eliminated only to build proofs. *)
   

   事实上，造成这种情况的原因之一是 Coq 被设计为与另一个称为“证明无关性”的原则兼容(我认为这就是您所说的“证明独立性”的意思)。