Изар доказательство соединения - PullRequest
Новая
       16

Изар доказательство соединения

1 голос
/ 06 марта 2019

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

(∀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", и я почти уверен, что есть способ сделать это.Но просмотр книги «Программирование и проверка» ничего мне не подсказывает.В Изабель, а не в Изаре, я полагаю, я бы применил conjI дважды, чтобы разделить одну цель на три, а затем разрешить первую.

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

1 Ответ

1 голос
/ 07 марта 2019

Согласно @xanonec:

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

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

Согласно @Джону: Синтаксис этого процесса, который фактически работал, был следующим: 

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

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

...