精益定理证明的第 4.4 节显示以下内容：

在这里，我将重点介绍从右到左的情况：

方法一

我们知道我们将有一个类型的参数，¬ (∃ x, ¬ p x)所以让我们从它开始：

我们知道我们必须返回一个类型的表达式，(∀ x, p x)所以让我们开始构造它：

此时我们需要返回一个类型的值，p x目前尚不清楚我们是否可以构建一个。也许我们需要尝试提出一个false值。

该函数hnExnpx返回false给定一个(∃ x, ¬ p x). 因此，让我们尝试构建其中一个，应用hnExnpx到它，然后使用false.elim：

现在我们又需要另一个false值了。

方法二

第 3 章提到有时需要经典逻辑。

一种幼稚的方法(em (∀ x, p x))将我们带到这里：

同样，我们需要一个p x值或一个false. 我们唯一的新东西是hnAxpx : ¬∀ (x : α), p x. 目前尚不清楚如何获得p x. hnAxpx确实返回 false 但我们需要 a(∀ x, p x)这是我们正在寻找的原始东西。:-)

也许这涉及更精细地使用经典逻辑？

欢迎任何建议！

更新

这是一种基于下面 simon1505475 评论的方法，该方法似乎有效：

示例： ¬ (∃ x, ¬ px) → (∀ x, px) :=

精益定理证明的第 4.4 节显示以下内容：

在这里，我将重点介绍从右到左的情况：

我们知道我们将有一个类型的参数，¬ (∀ x, ¬ p x)所以让我们从它开始：

此时，如果我们尝试使用exists.introwith x：

我们会得到一个错误，因为x它是一个未知的标识符。

然而，作为这组练习的一部分，我们得到：

所以让我们尝试使用exists.intro它：

我们没有，p a所以让我们尝试通过以下方式使用经典逻辑em：

的第一个子句or.elim以简单的方式处理：

由于我们有一个从(∀ x, ¬ p x)to false(ie hnAxnpx) 的函数，让我们尝试构建一个 type 的值(∀ x, ¬ p x)。然后我们可以调用hnAxnpx它并使用false.elim.

在这一点上，我们似乎如此接近！我们被告知我们需要一个¬p a下划线所在的位置。似乎这hnpa就是这样一个价值。所以让我们试试：

但是，我们得到以下错误：

我应该继续使用上面说明的方法吗？还是应该考虑完全不同的方法？

更新

这是另一种方法：

但是，那时，我不清楚如何false在下划线处获得值。

更新

关于最后一种方法，leanprover zulip 小组的 Mario Carneiro提供了以下非常有用的提示：

不要false.elim在你做过的地方使用；这会丢弃我们试图证明的信息(∃ x, p x)并导致无法解决的状态

改用 by_contradiction ，这也给了你一个假设¬ (∃ x, p x)

根据这个建议，我们得到：

这似乎有效。

我收到以下错误，我不知道如何解决此问题。

请帮忙。我尝试从 Github 存储库中提取我的主题，并按照 git 中的以下说明进行操作。

向下滚动时，Linux 的说明位于底部

我试图证明逻辑语句r → (∃ x : α, r)，其中r是 a Prop（命题或语句）并且α是 a Type。通过本书的练习，我已经证明了精益中的一些事情，但我被困在这一点上。

我真的不确定我什至不明白为什么这是真的。由于不存在任何类型，无人居住不会α使这是一个错误的陈述吗？xα

我最好的“尝试”是 1）希望精益的阐述者能满足我的需要，

但它不能推断出一些 type α，这是有道理的。2）我还认为这可能是一个非建设性的证明，所以我正在考虑做一个反证法。然而，我在纸上得到的最远距离是

我不确定如何在精益中执行第一个含义，即使我这样做了，我仍然需要一个xof 类型α来消除∀.

任何提示将不胜感激。

我正在尝试将倾斜堆形式化为精益。我已经定义了简单的树类型：

接下来，我想通过以下方式定义融合操作：

但是，当然，Lean 不接受这个函数，因为它“未能证明递归应用是递减的、有根据的关系”。显然，它使用了树木大小的字典乘积……显然失败了。

我怎样才能告诉它使用大小的总和？

为了在 Lean 中定义倾斜堆并证明一些结果，我定义了一种树类型以及一个融合操作：

然后，即使是非常简单的结果，例如

我被困住了。我真的不知道开始写这个证明。如果我这样开始：

我可以refl用于 where tis的情况lf，但如果它是 a 则不能nd。

我有点迷茫，因为在阿格达，这真的很容易。如果我定义这个：

那么前面的结果直接用 a 得到refl：

我错过了什么？

我定义了一种树，以及fusion如下操作：

然后，我有一个计数函数，它返回给定整数在树中出现的次数：

我想证明(occ x (fusion t1 t2)) = (occ x t1) + (occ x t2)，但在证明过程中，我遇到了一个问题，因为我不知道如何处理给定的归纳假设。

到目前为止，我已经想到了这个：

但我拼命地卡住了。ih 处理fusion d1 (nd g2 x2 d2))我想要的东西fusion (nd g1 x1 d1) d2。

我很乐意欢迎任何建议。

我刚刚阅读了 Lean 的文档，并尝试执行3.7。练习，
还没有完成所有练习，但这里是前四个练习（没有经典推理）：

变量 pqr : 道具

-- ∧ 和 ∨<br> 的交换性 示例：p ∧ q ↔ q ∧ p := sorry
示例：p ∨ q ↔ q ∨ p := sorry

-- ∧ 和 ∨<br> 的结合性 示例：(p ∧ q) ∧ r ↔ p ∧ (q ∧ r) := sorry
示例：(p ∨ q) ∨ r ↔ p ∨ (q ∨ r) := sorry

这是我为前四个练习所做的：

我认为这是有效的，但它很长，这是我们能做的最好的，还是有更好的方法来用精益编写这些证明，任何建议都将不胜感激。

在 Lean 的官方教程中，我看到了如何在 Vscode 和 Emacs 中使用 Lean 程序。我想知道如何从终端运行精益。例如，假设我编写了一个程序来检查是否存在无限多个素数，infinite_primes.lean并且我想通过执行来运行它

在终端。但是这个选项似乎不可用。

谁能帮助我理解如何编写一个可以通过归纳轻松获得的简单结果的证明，例如第一个n自然数之和的公式：1+2+...+n = n(n+1)/2，使用 LEAN 定理证明器？