Elim гипотеза двойного отрицания в Coq Proof Assistant?

Может ли кто-нибудь объяснить мне, почему мы должны доказать ~A после elim Ha.?

Перед "элим ха"

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 A

После

1 subgoals
 A : Prop
 Ha : ~ ~ A
______________________________________(1/1)
 ~ A

Правильно ли это означает ~~A true, ~A true -> A true?

Насколько я знаю, я знаю только правило ~E является ~A true, A true -> FalseHood true

1 ответ

Решение

В Кок, ~ P это обозначение для P -> False, Если я не ошибаюсь, используя elim на гипотезе формы ~ P так же, как непосредственно используя False_rect (вы можете Print False_rect для получения дополнительной информации) с P в качестве входа.

Делая так, вы говорите Coq "Я знаю, что P держит, поэтому с помощью P -> FalseЯ могу получить доказательство False"который закрывает цель противоречием. Вот почему каждый раз, когда вы elim ~ PCoq просит вас предоставить подтверждение P, В твоем случае, P является ~ A,

Другие вопросы по тегам