Я пытаюсь доказать эквивалентность P \/ Q и ~ P -> Q в предположении исключенного среднего,
Theorem eq_of_or :
excluded_middle ->
forall P Q : Prop,
(P \/ Q) <-> (~ P -> Q).
где исключенная середина следующая.
Definition excluded_middle := forall P : Prop, P \/ ~ P.
На самом деле, доказательство одного направления не требует Исключенного Середины. Пытаясь доказать обратное направление, я застреваю, когда пытаюсь использовать Исключенное Середину среди гипотез,
Proof.
intros EM P Q. split.
{ intros [H | H]. intros HNP.
- unfold not in HNP. exfalso.
apply HNP. apply H.
- intros HNP. apply H. }
{ intros H. unfold excluded_middle in EM.
unfold not in EM. unfold not in H.
}
где текущая среда следующая:
1 subgoal
EM : forall P : Prop, P \/ (P -> False)
P, Q : Prop
H : (P -> False) -> Q
______________________________________(1/1)
P \/ Q
Я понимаю, что при таких обстоятельствах нам нужно сделать что-то вроде «анализа случая» P, включая использование тактик left и right, если мое доказательство имеет смысл до сих пор.
Заранее спасибо за любые советы и предложения!
Undo. Однако, вдохновленный вашим объяснением, мне удалось закончить доказательство, добавив эти три строки:destruct (EM P) as [H' | H']. - left. apply H'.- right. apply H. apply H'.06.07.2017Undo- это не тактика, это часть Vernacular, которая отменяет действия предыдущей тактики. Итак,apply (H np).фактически завершает доказательство. Я добавил две другие версии на всякий случай. Просто шаг через доказательство, и вы получите его. 06.07.2017