Доказательство соединения Isar

Я пытаюсь что-то доказать с помощью Isar; пока что я достиг цели, которая выглядит так:

(∀P Q. P ≠ Q ⟶ (∃!l. plmeets P l ∧ plmeets Q l)) ∧
(∀P l. ¬ plmeets P l ⟶ (∃!m. affine_plane_data.parallel plmeets l m ∧ plmeets P m)) ∧
(∃P Q. P ≠ Q ∧ (∃R. P ≠ R ∧ Q ≠ R ∧ ¬ affine_plane_data.collinear plmeets P Q R))

(здесь plmeets - это функция, которую я определил, где plmeets P l - сокращение от «точка P лежит на прямой l» в аффинной плоскости, но я не думаю, что это важно для моего вопроса.)

Эта цель - сочетание трех вещей. На самом деле я уже доказал леммы, которые, как мне кажется, очень близки к каждой из этих вещей. Например, у меня есть

lemma four_points_a1: "P ≠ Q ⟹ ∃! l . plmeets P l ∧ plmeets Q l"

который производит вывод

theorem four_points_a1: ?P ≠ ?Q ⟹ ∃!l. plmeets ?P l ∧ plmeets ?Q l

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

Я хотел бы сказать: «из-за леммы four_points_a1 нам осталось доказать только item2 ∧ item3», и я почти уверен, что есть способ сделать это. Но просмотр книги «Программирование и испытание» ничего мне не говорит. В Isabelle, а не Isar, я бы применил conjI дважды, чтобы разделить одну цель на три, а затем решить первую цель.

Но я не вижу, как это сделать в Isar.


isabelle isar
person John    schedule 06.03.2019    source источник
comment
Полагаю, я бы применил конъюнктуру дважды, чтобы разделить одну цель на три, а затем разрешил бы первую цель. Это возможно сделать в рамках доказательства Isar. Однако может быть лучше использовать метод проверки intro вместо нескольких применений rule conjI, т.е. вы можете использовать apply(intro conjI), чтобы разделить цель на 3 подцели. Затем вы можете использовать subgoal для подтверждения каждой подцели в отдельности. Однако, если вы не предоставите свое приложение полностью, будет сложно сказать, существуют ли лучшие методы.   -  person user9716869    schedule 07.03.2019
comment
Спасибо. Похоже, это то, что мне нужно, чтобы пройти через этот конкретный блокпост. Я разместил его как ответ сообщества-вики, чтобы я мог принять его через несколько дней, оставив меньше оставшихся без ответа вопросов. (Если вы предпочитаете написать это как ответ, я приму его).   -  person John    schedule 07.03.2019

Ответы (1)


arrow_upward
1
arrow_downward

Согласно @xanonec:

Полагаю, я бы применил конъюнктуру дважды, чтобы разделить одну цель на три, а затем разрешил бы первую цель.

Это возможно сделать в рамках доказательства Isar. Однако может быть лучше использовать вводную часть метода доказательства вместо нескольких применений правила conjI, т.е. вы можете использовать apply(intro conjI), чтобы разделить цель на 3 подцели. Затем вы можете использовать subgoal для подтверждения каждой подцели в отдельности. Однако, если вы не предоставите свое приложение полностью, будет сложно сказать, существуют ли лучшие методы.

Согласно @John: синтаксис этого процесса, который действительно работал, был следующим:

  proposition four_points_sufficient: "affine_plane plmeets"
    unfolding affine_plane_def
    apply (intro conjI)
    subgoal using four_points_a1 by blast

Мне не ясно, как «это можно сделать [то есть применить conjI дважды] в рамках доказательства Isar», но, возможно, мне сейчас и не нужно знать.

person Community    schedule 06.03.2019
comment
Это можно сделать [т. Е. Применить conjI дважды] в рамках доказательства Isar. Можно использовать список методов, разделенных запятыми (последовательная композиция, также см. П. 6.4 в справочном руководстве) как в скриптах Isar, так и в apply, например lemma "True" proof fix A B :: "'a ⇒ bool" have "∀x y. A x ∧ B y ⟶ B y ∧ A x" by (rule allI, rule allI, simp) .... - person user9716869; 07.03.2019
comment
Кроме того, нет ничего, что могло бы помешать использовать сценарий стиля apply внутри блока proof. Насколько мне известно, это не считается очень хорошей практикой, но также не считается особенно плохой практикой (см. Не переключаться с применения на доказательство в середине доказательства в https://proofcraft.org/blog/isabelle-style.html). - person user9716869; 07.03.2019