->在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。²

证明类型目标的通常方法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，我们看到，我们的带s和s并产生s的函数也是f: P -> Q -> R如此。在（引入了多个术语）之后，我们看到了和。最后一行（在之前）仅将函数应用于并在中获取内容。fPQRintrosq: Qp: PQed.fpqR

对于您的问题，intros介绍了命题P，Q和R以及H1: P -> Q和H2: Q -> R。P由于目标是，我们仍然可以再引入一个类型术语P -> R。您能看到如何使用H1和H2和元素P来产生的元素R吗？提示：您将经历Q。另外，请记住H1和H2是函数。

¹您可以将排除中间定律作为公理添加，这将允许您进行所需的案例分析，但我认为这与Coq无关。

²如果您想知道，的元素Prop仍然是类型，并且具有与Set或元素非常相似的行为Type。唯一的区别是Prop“强制性”，它使命题可以量化所有命题。例如，forall P: Prop, P -> P是的元素Prop，但是forall A: Type, A -> A下一级的元素Type（Type实际上是无限层次结构）。