2

我试图证明->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.

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

4

1 回答 1

5

Coq 的逻辑不是命题为真或假的经典逻辑。相反，它基于类型理论，默认情况下具有直觉主义风格。1在类型论中，你应该认为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，以及和。不过，我们仍然可以再引入一个类型术语，因为目标是. 你能看到如何使用和和一个元素来产生一个元素吗？提示：你会通过. 另外，请记住和是函数。QRH1: P -> QH2: Q -> RPP -> RH1H2PRQH1H2

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

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

于 2019-03-22T08:18:23.243 回答