Можно ли доказать 'implies_to_or -> de_morgan_not_and_not', не прибегая к другим классическим законам?

Question

Theorem implies_to_or_to_de_morgan_not_and_not : 
  implies_to_or -> de_morgan_not_and_not.
Proof.
unfold implies_to_or, de_morgan_not_and_not, not.
intros.
Admitted.

1 subgoal
H : forall P Q : Prop, (P -> Q) -> (P -> False) \/ Q
P, Q : Prop
H0 : (P -> False) /\ (Q -> False) -> False
______________________________________(1/1)
P \/ Q

Это из пятизвездочного упражнения в конце главы SF Logic.

Я уже слишком много часов бьюсь над этой конкретной проблемой, поэтому мне действительно нужно спросить об этом. Я уже доказал excluded_middle <-> peirce, peirce <-> double_negation_elimination, double_negation_elimination <-> de_morgan_not_and_not, implies_to_or <-> excluded_middle, de_morgan_not_and_not -> implies_to_or, поэтому у меня уже есть больше, чем все пройденные пути. Для меня это только делает эту проблему еще более запутанной, и я не понимаю, почему я не могу даже получить это доказательство с земли.

Почему-то здесь не так много работы.

Одним из вариантов было бы сделать exfalso и попытаться сделать что-то оттуда, но это отбросило бы цель P \/ Q, и я подозреваю, что это было бы слишком большой потерей информации, даже если бы я мог сделать что-то вроде прогресса.

Еще один вариант - попытаться уничтожить H, но в этом случае возникает проблема с попыткой доказать P -> Q без чего-либо пригодного для использования в помещении.

У меня были проблемы с упражнениями на прошлой неделе, и я сумел преодолеть их с усилием, но я не достаточно опытен, чтобы просто позволить этой вещи лежать, не спрашивая совета. Что именно я здесь не вижу?

Очевидно, я не хочу конвертировать de_morgan_not_and_not в другие легче решить классический закон (например, исключенную середину), поскольку это было бы помимо точки.

Answer 1

Поскольку в книге «Основы программного обеспечения» явно не предлагается публиковать решения, позвольте мне дать подсказку.

Обратите внимание, что гипотеза H является универсально выраженной в обоих предложениях, о которых она говорит. Это означает, что вы можете предоставить любые предложения для P и Q, даже те же самые . По сути, это наблюдение позволяет вам рассуждать классически, чего достаточно для решения этой проблемы.

Answer 2

Есть ли конкретная причина, по которой вы не хотите использовать другие доказательства, чтобы доказать это?Довольно искусственно избегать использования результата, который, как вы знаете, является безусловно верным.

Вы можете избежать манипулирования de_morgan_not_and_not, используя implies_to_or для выполнения анализа случаев на P и Q (см. Ваше доказательствоimplies_to_or -> excluded_middle).Затем у вас есть четыре случая, и все четыре конечные цели являются простыми 1-3 строчными доказательствами.