了解 Coq 中 intros 关键字的工作原理

Pap*_*ika 2 coq gallina

Theorem law_of_contradiction : forall (P Q : Prop),\n  P /\\ ~P -> Q.\nProof.\n  intros P Q P_and_not_P.\n  destruct P_and_not_P as [P_holds not_P].\n
Run Code Online (Sandbox Code Playgroud)\n

我正在尝试真正理解这个intros关键字。假设我们想证明P /\\ ~P -> Q。好的,以某种方式intros P Q介绍PQ。但是这是什么意思?它能识别出PQ证明的事物吗?关于什么P_and_not_P?它是什么?为什么P和Q使用相同的名称,而is却P_and_not_P定义了一个名称?

\n

更新:

\n

看起来它是逐项匹配的:

\n
Theorem modus_tollens: forall (P Q : Prop),\n  (P -> Q) -> ~Q -> ~P.\nProof.\nintro P.\nintro Q.\nintro P_implies_Q.\nintro not_q.\nintro not_p.\n
Run Code Online (Sandbox Code Playgroud)\n

给出

\n
P Q \xe2\x84\x99\nP_implies_Q P \xe2\x86\x92 Q\nnot_q ~ Q\nnot_p P\n
Run Code Online (Sandbox Code Playgroud)\n

但为什么不not_p等于~P

\n

Li-*_*Xia 6

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

(* Starting goal *)

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

(* Goal after [intros A] *)

A : Prop
------------
forall Q, A /\ ~A -> Q
Run Code Online (Sandbox Code Playgroud)

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

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

Coq 中的含义是量化,其中假设未命名:P /\ ~ P -> Q相当于forall (H : P /\ ~P), Q,注意H没有在正文中使用Q。因此,当您这样做时intros P_and_not_P,您正在重命名H,但未使用该名称,因此您不会看到目标发生变化。您可以禁用漂亮打印来查看这一点。

Unset Printing Notations.
Run Code Online (Sandbox Code Playgroud)
(* 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
Run Code Online (Sandbox Code Playgroud)

的否定,表示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
Run Code Online (Sandbox Code Playgroud)