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.