1

我正在尝试使用 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”，我很确定有办法做到这一点。但是看“编程和证明”这本书对我没有任何建议。在伊莎贝尔，而不是伊萨尔，我想我会申请conjI两次将一个目标分成三个，然后解决第一个目标。

但我看不到如何在 Isar 中做到这一点。

4

1 回答 1

1

根据@xanonec：

我想我会应用 conjI 两次将一个目标分成三个，然后解决第一个目标。

在 Isar 证明中可以做到这一点。但是，最好使用 proof 方法 intro 而不是 rule 的多个应用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 证明中如何做到这一点[即应用两次]”，但也许我现在不需要知道。

于 2019-03-06T22:50:20.770 回答