问题标签 [lean]

对于一个通过 LEAN 文档工作的新手来说，当更困难的问题显然已经解决时，看到一些简单的问题变成真正的瓶颈有时会非常令人沮丧。这是一个简单的自制练习，结果变成了几个小时的挫败感（当然，没有其他方法可以学习）：

问题似乎是order有类型2<3，但需要的是a<b，虽然在我看来应该很清楚a=2and b=3，但 LEAN 不这么认为。请帮我看看我在这里缺少什么！

在经历了大多数练习并在 LEAN 手册第 3 章末尾的前五个命题有效性/属性中解决/证明后，我仍然无法理解以下含义（证明属性 6 所需的含义之一):

我面临的困难主要是由于p不正确的情况，因为我不知道如何结合，使用精益工具，and假设中的两侧获得事实，即两者都q必须r在该场景下成立。我将不胜感激这里的任何帮助；请帮助我了解如何在上述设置中构建此证明，而无需导入除标准精益中的策略之外的任何其他策略。为了完整起见，这是我对另一个方向的证明：

LEAN 教程第 3 章末尾的两个证明我仍然在努力（因此阻止我进一步阅读手册）如下：

为此，我试图证明正确的含义在这一点上停止了：

显然我还不知道如何使用¬p. 也不知道如何显示左边的含义。另一个是这样的：

我应该使用（作为正确的含义）来显示以下内容：

在这里，我得到了左侧：

帝国理工学院开发的自然数博弈是一个很棒的想法，它极大地帮助了用 LEAN 编写证明的基础知识。在经历了大部分之后，还有一个“额外”的问题，我还无法弄清楚。下面是这个问题的精简版本，可以放在一个空文件中，并且可以在 LEAN 中独立运行。

该rw策略无法在此处识别应该替换的模式，尽管它的打印与目标中出现的完全一样。在线提供的解决方案没有解释为什么会发生这种情况，而是使用了ring绕过它的策略。但是，游戏的作者说有一个解决方案，只使用rw. 你能帮我理解这里有什么问题吗？此外，任何额外的代码或提示都会很棒！我从来没有上过抽象代数课，虽然我很喜欢这个游戏并且学到了很多东西，但这里可能有些东西我没有意识到。

我的证明如下，但它是错误的，我不知道如何更正

来自第一原理的基本含义的证明，“精益中的定理证明”4.4 中的一个练习，击败了我迄今为止的所有尝试：

之后intro我不知道怎么用nAxpx才能走得更远。我想过by_contradiction，但那只引入了否定存在nExnpx，不能与 一起使用cases，所以我不能产生一个x : α。排除中间似乎也无济于事。我可以用mathlib战术来证明，

但没有足够的知识将其转换回战术模式，所以这无助于我的理解。

为什么 mathlib 对 UFD 的定义是这样的：

（要求通过类型类推断来推断积分域结构）但它对PID的定义是这样的：

扩展积分域结构？有什么区别？旧的结构命令与它有关吗？

这个证明是 Avigad 等人的“逻辑与证明”中的一个基于策略的版本。

哪个有效。我试图在精益手册中倒退，因为战术模式对我来说更直观。在没有策略的情况下尝试相同的方法时，我遇到了麻烦exists.elim，因为精益手册中的所有示例都显示了如何使用它来实现最终目标，而不是中间步骤。谁能帮我修复这段代码？是否可以let或match也可用于相同目的？

精益文档显示了以下两个示例，其中只有一个变量：

在这两种情况下，普遍假设（h2在前一个例子中，hw在后一个例子中）只取决于一个变量。

现在假设我们得到（我解释原来的问题）：

在h2中，想象P和R就像nat.is_even，并且Q就像“x,y 形成一对偶数”。

exists.elim我想，需要的内部推导如下：

但我不确定如何将它与存在消除一起使用 - 因为基本上需要一次完成两个消除。exists.elim h1a (exists.elim h1b (assume ... show Q, from ...))似乎不起作用。

给定一个自定义类型来表示从类型 b 到 a 的嵌入：

我正在尝试定义一个restrict给定关系的函数，r:a -> a -> Prop 并且嵌入e:Embedding b a返回一个关系b

我无法解构我的嵌入以访问底层注入。

在 Coq 中做同样的事情效果很好：

如果有人能提出一些解决这个问题的建议，我将不胜感激。Prop我熟悉 Coq 的限制，即当目标为 Sort Setor时无法解构 sort 的术语Type i，因此可以理解 Lean 中的类似限制，但这似乎是这里的问题。我试图做Embedding一个归纳谓词（所以返回Prop而不是Sort u），但这并没有解决错误。

我热衷于将我的 Coq 开发转化为学习精益的一种方式，因此我很乐意打破这个障碍 :)