Learning 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, Чтобы исправить сообщение об ошибке, вы должны импортировать библиотеку Coq, где NNPP определено:

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.