问题标签 [lean]

我希望在精益定理证明器中证明这个定理。首先，我需要定义偏序集之类的东西，以便我可以定义下确界/上确界。这是如何在精益中完成的？本教程提到了 setoid，它们是具有相关等价关系的类型。但我不清楚这有什么帮助。

以下代码有一个奇怪的行为

在向我展示 eq.symm 的类型时，我希望 check 不会考虑不相关的隐式变量 toto。这真的是故意的吗？

嗨，我正在尝试在精益证明助手中做一些数学运算，看看它是如何工作的。我认为与交换环的幂等一起玩应该很有趣。这是我尝试过的：

然后我得到错误

所以 Lean 似乎忘记了 A 是一个环？

例如，如果我将定义更改为

那么一切都很好。但这意味着我必须携带额外的簿记数据。有没有办法使用变量来解决保留簿记的需要。

我正在尝试定义以下数量部分：

但得到错误

由于 Hdecp，我如何帮助 Lean 认识到 (pi p) 确实是可判定的？

我无法理解如何触发 Lean 对类型类的使用。这是一个小例子的尝试：

关键是我希望 Lean 看到它可以使用 HA 从引理 T 中推断出 toto A。我错过了什么？

如何使用形状假设

在战术模式？在术语模式下，我会使用

我已经完成了精益教程的前 3 章，并且已经完成了一些命题逻辑的证明。

现在我试着回过头来问自己一些愚蠢的问题。

我的理解是：

1. 术语可以有类型：constant A : Type. A是一个术语，Type是 的类型A。
2. 术语可以变成类型：constant a : A.
3. 一个术语的类型可以取决于另一个术语的类型constant B : A -> Type：constant B' : Π (a : A), Type

但是这种理解显然是错误的，因为这段代码没有进行类型检查：

开头的所有行constant C，即第 9、11 和 13 行都会抛出错误error: type expected at B

为什么？我怀疑并非所有术语都可以成为类型。我怀疑类型依赖于其他类型的术语不能成为 types。为什么？

我尝试使用归纳数据类型的语法，但它收到一条错误消息“相互归纳类型必须编译为具有依赖消除的基本归纳类型”。

下面是我尝试定义命题even和odd自然数的示例

还有一个相关的问题：定义相互递归函数的语法是什么？我似乎无法在任何地方找到它的记录。

精益拒绝以下定义：

带有错误消息“'natlist.cons' 的 arg #2 不是递归的，但它发生在递归参数之后”

正如预期的那样，接受以下定义：

精益执行此命令的原因是什么？