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

Question

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

\n

我正在尝试真正理解这个intros关键字。假设我们想证明P /\\ ~P -> Q。好的，以某种方式intros P Q介绍P和Q。但是这是什么意思？它能识别出P要Q证明的事物吗？关于什么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

\n

给出

\n

P Q \xe2\x84\x99\nP_implies_Q P \xe2\x86\x92 Q\nnot_q ~ Q\nnot_p P\n

\n

但为什么不not_p等于~P？

\n

Answer 1

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没有在正文中使用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