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
介绍P
和Q
。但是这是什么意思?它能识别出P
要Q
证明的事物吗?关于什么P_and_not_P
?它是什么?为什么P和Q使用相同的名称,而is却P_and_not_P
定义了一个名称?
更新:
\n看起来它是逐项匹配的:
\nTheorem 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给出
\nP 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
?
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
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)