问题标签 [lean]

我在 Ubuntu 上下载了适用于 Linux 的精益，提取它，安装了 Emacs，通过 MELPA 安装了精益模式和公司精益，它抱怨没有设置精益根目录变量。当我尝试设置它时，我得到标题中的错误。

我正在使用Lean来尝试形式化欧几里得空间 (R^n) 子集的概念。

我尝试了以下方法：

尝试输入英语：

1. 实数 (R) 在mathlib的分析组件中定义。
2. 我们需要将其推广到 k 维，所以我们想要 R 与其自身任意多次的笛卡尔积。
3. repeated_prod允许一个人采用任意类型并多次应用笛卡尔积。
4. euclidean_space是 R 情况的特化。
5. 我们说，euclidean_subset如果存在某个欧几里得空间（注意：我试图避免提及维度，所以它是某个R^n。），它是集合 ( M) 的子集。

然而，这给出了错误：

虽然，我承认我不知道默认值trace.class_instances是什么，但我将其设置为10000，它花费了更长的时间，并且给出了相同的错误消息，导致我认为错误消息具有误导性。似乎找不到很多关于这种语言的信息，包括我收到的错误消息，任何解决此错误的帮助将不胜感激。

在上一个问题中，我询问了关于形式化欧几里得空间子集的问题，我收到了以下关于如何创建 n 维欧几里得空间的回复：

我收到了以下关于创建欧几里得空间子集的回复：

运行我修改后的代码，编译的所有内容都很棒，并且相信答案（至少，大部分）是正确的。我想尝试对代码进行一些基本检查。特别是，我希望：

给：

好吧，它没有。它超时了。然后我继续尝试其他一些套装。我修改euclidean_space为：

虽然，不再忠实于它的名字，人们应该期待

给：

好吧，几乎，它给出了：

鉴于结果我删除了set调用并重新定义euclidean_space为：

减少产生了预期的结果。然后我返回并用ℝ替换了ℕ：

euclidean_subset仍然编译，但是#reduce仍然使用 ℝ 给出超时。为什么ℕ不超时？

我Type*在这个项目中看到了一些实例。跑步#check Type*给予Type u_1 : Type (u_1+1)和#check Type给予Type : Type 1。

搜索语言参考和ingCtrl-F表达式章节似乎没有提供任何关于Type*. 从概念上讲，它是用来做什么的？另外，如果可能的话，我链接的项目中使用了什么？

（*很难搜索，如果这是重复的，请见谅。）

我正在尝试使用精益证明一个代数定理。我的代码是

请让我知道如何消除最后的括号。也就是说，我只想获得

a * c + b * c + e* c + a * d + b * d + e * d

非常感谢。

我已经查看但没有找到文档中描述的任何机制，它允许您通过其签名来描述一个部分。例如，在下面的部分中，def 的语法需要右手边（这里很抱歉）

有没有类似签名的东西可以让你转发声明一个部分的内容？比如下面的组成语法。

我使用实际语法最接近的是以下，它声明了两次证明，第二次是为了使右侧的证明尽可能短。

我正在尝试在 Lean 中创建合并排序定义，并创建了以下代码：

使用合并定义

和 fhalf / sndhalf 定义：

但是，我收到以下错误消息：

未能证明递归应用正在减少，有根据的关系

可能的解决方案：

• 在定义的末尾使用using_well_founded关键字来指定合成有根据的关系和减少证明的策略。

• 默认的递减策略使用“假设”策略，因此可以使用“有”表达式提供提示（也称为本地证明）。嵌套异常包含递减策略的失败状态。

谁能帮我证明归并排序正在减少？

在精益中，“选择”是根据以下实施的：

我们的选择公理现在简单地表达如下：

只给定 α 非空的断言 h，选择 h 神奇地产生了 α 的一个元素。

现在，如果我阅读有关集合论和选择公理的文献（Jech）：

选择公理 (AC)。每个非空集合族都有一个选择函数。

如果 S 是一个集合族并且 ∅ 不在 S 中，则 S 的选择函数是 S 上的函数 f，使得对于每个 X ∈ S，f(X) ∈ X。

对我来说，这些东西似乎并不等同。有人可以详细说明一下吗？

我正在处理两个二元关系：g_o 和 pw_o，并且我在下面定义了 pw_o：

我需要证明以下几点：

我从这些策略开始：

我有这个：

由于 pw_o 是用通用量词定义的，所以我想用 x 替换 w，那么我将有 (g_o xy → g_o xz) ∧ (g_o zx → g_o yx)。在用“cases”策略分离出第一个连词之后，我可以在第一个连词和 h1 上使用 modus ponens。

如何告诉 Lean 将 pw_o 定义中的 w 替换为 x 并将 pw_o 定义中的 x 和 y 分别替换为 y 和 z？

我正在尝试学习精益，我正在尝试弄清楚如何I*M = {i*m | i in I, m in M}从理想的 I 和 R 模块 M中创建一个新的 R 模块。

所以我的尝试是首先定义一个映射ideal_mult来创建一个新的 R 模块，然后弄清楚如何为它分配一个好的符号。

我该如何定义它，以便我可以例如陈述一个假设(h: I*M = M)？

感谢您的帮助！