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
~ P
Coq просит вас предоставить подтверждение P
, В твоем случае, P
является ~ A
,