WedX - журнал о программировании и компьютерных науках

Как использовать гипотезу, содержащую forall в Coq?

Я пытаюсь доказать эквивалентность 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, если мое доказательство имеет смысл до сих пор.

Заранее спасибо за любые советы и предложения!

06.07.2017

Ответы:


1

Вы можете создать экземпляр EM : forall P : Prop, P \/ ~ P с любым предложением (я создал его с помощью P ниже и немедленно уничтожил), поскольку EM по сути является функцией, которая принимает произвольное предложение P и возвращает доказательство либо P, либо ~ P.

Theorem eq_of_or' :
  excluded_middle ->
  forall P Q : Prop, (~ P -> Q) -> P \/ Q.
Proof.
  intros EM P Q.
  destruct (EM P) as [p | np].     (* <- the key part is here *)
  - left. apply p.
  - right.
    apply (H np).
    (* or, equivalently, *)
    Undo.
    apply H.
    apply np.
    Undo 2.
    (* we can also combine two `apply` into one: *)
    apply H, np.
Qed.
06.07.2017
  • Спасибо за ваше решение! Я действительно новичок в Coq, и я еще не научился использовать тактику Undo. Однако, вдохновленный вашим объяснением, мне удалось закончить доказательство, добавив эти три строки: destruct (EM P) as [H' | H']. - left. apply H'.- right. apply H. apply H'. 06.07.2017
  • Undo - это не тактика, это часть Vernacular, которая отменяет действия предыдущей тактики. Итак, apply (H np). фактически завершает доказательство. Я добавил две другие версии на всякий случай. Просто шаг через доказательство, и вы получите его. 06.07.2017
  • Новые материалы

    Объяснение документов 02: BERT
    BERT представил двухступенчатую структуру обучения: предварительное обучение и тонкая настройка. Во время предварительного обучения модель обучается на неразмеченных данных с помощью..

    Как проанализировать работу вашего классификатора?
    Не всегда просто знать, какие показатели использовать С развитием глубокого обучения все больше и больше людей учатся обучать свой первый классификатор. Но как только вы закончите..

    Работа с цепями Маркова, часть 4 (Машинное обучение)
    Нелинейные цепи Маркова с агрегатором и их приложения (arXiv) Автор : Бар Лайт Аннотация: Изучаются свойства подкласса случайных процессов, называемых дискретными нелинейными цепями Маркова..

    Crazy Laravel Livewire упростил мне создание электронной коммерции (панель администратора и API) [Часть 3]
    Как вы сегодня, ребята? В этой части мы создадим CRUD для данных о продукте. Думаю, в этой части я не буду слишком много делиться теорией, но чаще буду делиться своим кодом. Потому что..

    Использование машинного обучения и Python для классификации 1000 сезонов новичков MLB Hitter
    Чему может научиться машина, глядя на сезоны новичков 1000 игроков MLB? Это то, что исследует это приложение. В этом процессе мы будем использовать неконтролируемое обучение, чтобы..

    Учебные заметки: создание моего первого пакета Node.js
    Это мои обучающие заметки, когда я научился создавать свой самый первый пакет Node.js, распространяемый через npm. Оглавление Глоссарий I. Новый пакет 1.1 советы по инициализации..

    Забудьте о Matplotlib: улучшите визуализацию данных с помощью умопомрачительных функций Seaborn!
    Примечание. Эта запись в блоге предполагает базовое знакомство с Python и концепциями анализа данных. Привет, энтузиасты данных! Добро пожаловать в мой блог, где я расскажу о невероятных..


    Для любых предложений по сайту: wedx@cp9.ru