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

Posted 2023-05-08

【中文标题】如何或有可能在 Coq 中证明或证伪 `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.`？

【英文标题】：How or is that possible to prove or falsify `forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.` in Coq?

【发布时间】：2014-12-21 17:14:22

【问题描述】：

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

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

Lemma True_neq_True2 : True = True2 -> False.

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

所以我的问题是：

如何或有可能在 Coq 中证明或伪造forall (P Q : Prop), (P -> Q) -> (Q -> P) -> P = Q.？ 为什么inversion H 什么都不做；是不是因为 coq 的证明独立性，如果是这样，为什么 Coq 这样做会浪费精力。

【问题讨论】：

“为什么”不是编程问题。

【参考方案1】：

您提到的原则forall P Q : Prop, (P <-> Q) -> P = Q 通常称为命题扩展性。这个原则在 Coq 的逻辑中是不可证明的，并且最初的逻辑是被设计成可以作为公理添加而不会造成伤害的。因此，在标准库 (Coq.Logic.ClassicalFacts) 中，可以找到许多关于这一原则的定理，并将其与其他著名的经典推理逻辑原则联系起来。出人意料的是，被recently 发现Coq 的逻辑与这个原理不兼容，但是出于一个非常微妙的原因。这被认为是一个错误，因为已经设计了逻辑，以便可以将其作为公理添加而不会造成伤害。他们想在新版本的 Coq 中解决这个问题，但我不知道它的当前状态是什么。从 8.4 版开始，Coq 中的命题外延性不一致。

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

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.

如果您尝试对Prop 中的bool 版本执行相同操作，则会收到一个信息量更大的错误：

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 被设计为与另一个称为 证明无关性 的原则兼容（我认为这就是您所说的“证明独立性”）。

【讨论】：

感谢您的精彩回答。我最初的目标是证明：forall (P Q : Prop) (F : Prop -> Prop), (P Q) -> (F P F Q)。但我做不到，所以我试图证明上述命题。不幸的是，我又失败了。

你的初始目标和提到的命题在 Coq 中实际上是等价的，没有任何额外的公理。 (forall F, F P -> F Q) 甚至被称为莱布尼茨等式。

@jbapple 我相信你误读了：原始目标的前提是逻辑等价，而不是平等。如果它是平等的，它确实会起作用。

让我试着更清楚一点：有一个 Coq 证明（没有附加公理） (forall (PQ : Prop) (F : Prop -> Prop), (P Q) - > (FP FQ)) (forall (PQ : Prop), (P Q) -> P = Q).

@TorosFanny 这就是依赖模式匹配的工作方式。在我们的 return 子句中，我们说我们将返回 if b then True else False 类型的东西，其中 b 的确切值可能在每个模式匹配分支上有所不同。只有一个分支，即eq_refl 一个，在那个分支上b = true。因此，我们必须返回if true then True else False = True 类型的东西。然而，在外部，我们匹配的是true = false，因此返回类型实际上是if false then True else False = False。