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

【问题标题】：Learning coq, not sure what the error means NNPP学习coq，不知道错误是什么意思 NNPP
【发布时间】：2019-02-27 02:40:17
【问题描述】：

所以我才刚刚开始学习 coq（到目前为止，它已经超出了我的想象），我正在尝试做一个基本的证明，但我很迷茫，到目前为止找到了一些帮助，但我认为我's should do 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.

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

【问题讨论】：

标签： coq proof coqide

【解决方案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.

【讨论】：