Coq中的 - >的传递性

Question

我试图在Coq的命题中证明->的传递性：

Theorem implies_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> (P -> R).
Proof.

我想破坏所有命题，简单地处理所有8种反射性的可能性。显然它并不那么简单。这是我试过的：

Theorem implies_trans : forall P Q R : Prop,
  (P -> Q) -> (Q -> R) -> (P -> R).
Proof.
  intros P Q R H1 H2.
  destruct P. (** Hmmm ... this doesn't work *)
Admitted.

这就是我得到的：

1 subgoal
P, Q, R : Prop
H1 : P -> Q
H2 : Q -> R
______________________________________(1/1)
P -> R

然后是这个错误：

Error: Not an inductive product.

非常感谢任何帮助，谢谢！

Answer 1

Coq的逻辑不是命题是真还是假的经典逻辑。相反，它基于类型理论并且默认具有直觉风格。在类型理论中，你应该认为P -> Q是一个函数，从“P类型的东西”到“Q类型的东西”.2

证明P -> Q类型目标的通常方法是使用intro或intros来引入P类型的假设，然后使用该假设以某种方式产生Q类型的元素。

例如，我们可以证明(P -> Q -> R) -> (Q -> P -> R)。在“暗示是一种函数”的解释中，这可以解释为如果我们有一个函数需要P和Q并产生R，那么我们可以定义一个函数，它接受Q和P并产生R。这是相同的功能，但交换了参数。

Definition ArgSwap_1 {P Q R: Prop}: (P -> Q -> R) -> (Q -> P -> R) :=
  fun f q p => f p q.

使用策略，我们可以看到各个元素的类型。

Lemma ArgSwap_2 {P Q R: Prop}: (P -> Q -> R) -> (Q -> P -> R).
Proof.
  intro f.
  intros q p.
  exact (f p q).
Qed.

在intro之后，我们看到f: P -> Q -> R，所以f是我们的功能，需要Ps和Qs并产生Rs。在intros（引入多个术语）之后，我们看到q: Q和p: P。最后一行（在Qed.之前）只是将函数f应用于p和q以获得R中的某些内容。

对于你的问题，intros介绍了命题P，Q和R，以及H1: P -> Q和H2: Q -> R。我们仍然可以引入另一个类型P，因为目标是P -> R。你能看到如何使用H1和H2以及P的元素来生成R的元素吗？提示：你会通过Q。另外，请记住H1和H2是函数。

---

1您可以将排除中间的定律添加为公理，这将允许您想要的案例分析，但我认为它错过了Coq的观点。

2如果你想知道，Prop的元素仍然是类型，并且与Set或Type的元素具有非常相似的行为。唯一的区别是Prop是“不可预测的”，它允许命题量化所有命题。例如，forall P: Prop, P -> P是Prop的一个元素，但是forall A: Type, A -> A是Type的下一级元素（Type实际上是一个无限的等级）。