0 
Theorem law_of_contradiction : forall (P Q : Prop),
  P /\ ~P -> Q.
Proof.
  intros P Q P_and_not_P.
  destruct P_and_not_P as [P_holds not_P].

我正在尝试重新理解intros关键字。假设我们要证明P /\ ~P -> Q。好的，以某种方式intros P Q介绍Pand Q。但是这是什么意思？它是否从要证明的事物中识别P和？Q怎么样P_and_not_P？它是什么？为什么 P 和 Q 使用相同的名称，而P_and_not_Pis 是定义名称？

更新：

看起来它是逐词匹配的：

Theorem modus_tollens: forall (P Q : Prop),
  (P -> Q) -> ~Q -> ~P.
Proof.
intro P.
intro Q.
intro P_implies_Q.
intro not_q.
intro not_p.

给

P Q ℙ
P_implies_Q P → Q
not_q ~ Q
not_p P

但为什么不not_p等于~P？

4

1 回答 1

4

intro A（相当于）的作用：如果intros A您有一个形式为 的目标forall (P : _), ...，它将重命名P为A，从目标的开头删除forall，并将假设A放入目标中。

(* Starting goal *)

-----------
forall P Q : Prop, P /\ ~P -> Q

(* Goal after [intros A] *)

A : Prop
------------
forall Q, A /\ ~A -> Q

如果这样做intros P Q，通过选择目标中已有的名称，无需重命名，因此名称不会发生变化。

您提到的其他情况intros是该行为的特殊情况。

Coq 中的含义是未命名假设的量化：P /\ ~ P -> Q等价于forall (H : P /\ ~P), Q，注意H在 body 中没有使用Q。因此，当你这样做时intros P_and_not_P，你正在重命名H，它没有被使用，所以你看不到目标的变化。您可以禁用漂亮的打印来查看。

Unset Printing Notations.

(* Starting goal; a name that is not used becomes "_" *)

----------
forall (P Q : Prop) (_ : and P (not P)), Q.

(* After [intros P Q R] *)

P : Prop
Q : Prop
R : and P (not P)
----------
Q

的否定，P表示为~P，在 Coq 中定义P -> False（这在直觉逻辑中很典型，其他逻辑可能不同）。您可以通过该策略看到这一点unfold not

(* Starting goal *)

----------
forall (P Q : Prop), (P -> Q) -> ~Q -> ~P.


(* After [unfold not] *)

----------
forall (P Q : Prop), (P -> Q) -> (Q -> False) -> P -> False.


(* After [intros P Q R S T] *)

P : Prop
Q : Prop
R : P -> Q
S : Q -> False
T : P
----------
False
于 2021-12-26T15:54:39.053 回答