coq - 学习coq，不知道错误是什么意思 NNPP

Question

所以我刚刚开始学习coq（到目前为止它已经超出了我的想象）并且我正在尝试做一个基本的证明并且我很迷茫，到目前为止找到了一些帮助但是我认为我应该做 coq 会引发错误。所以在我的编辑部分我有：

Section wut.
Variables p q: Prop.
Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.

在打样框中我有：

1 subgoal
p, q : Prop
H : ~ q -> ~ p
H0 : p
______________________________________(1/1)
q

在错误框中我有：

The reference NNPP was not found in the current environment.

当前环境下找不到是什么意思？

Answer 1

引理是双重否定消除原理：NNPP它说~ ~ P蕴含P。要修复错误消息，您必须导入NNPP定义的 Coq 库：

Require Import Coq.Logic.Classical.

Section wut.
Variables p q: Prop.
Theorem T1 : (~q->~p)->(p->q).
Proof.
intros.
apply NNPP.
intro.
apply H in H1.
contradiction.
Qed.