问题标签 [lean]

使用精益，计算机校样检查系统。

这些证明中的第一个成功，第二个没有。

错误发生在eq.subst和 中，如下所示：

[然后是一些附加信息]

我不明白错误信息。我在假设中尝试了各种明显的排列，例如 0 = n 或 n > 0，但我无法让它工作，或者产生我可以理解的错误消息。

谁能澄清一下？我阅读了关于精益的定理证明部分，congr_arg但这些其他命令对我没有帮助。

我正在阅读第 7 章——“精益中的定理证明”的归纳类型。

我想知道如何以更扩展或“原始”的形式编写依赖非依赖产品的定义。

1. 看起来教程中给出的定义会自动推断出一些细节： inductive prod1 (α : Type u) (β : Type v) | mk : α → β → prod1

2. 一些实验允许填写细节 inductive prod2 (α : Type u) (β : Type v) : Type (max u v) | mk : α → β → prod2

3. 但是以完全扩展的形式给出定义，使用 Pi 类型无法进行类型检查： inductive prod3 : Π (α : Type u) (β : Type v), Type (max u v) | mk : α → β → prod3

正确的书写方式是prod3什么？

最后，下面的定义是否等同于prod1and prod2，即类型检查器是否总能推断出αand的正确类型全域β？

4. inductive prod4 (α : Type) (β : Type) | mk : α → β → prod4

我想用精益做一些拓扑工作。

作为一个好的开始，我想证明几个关于精益集合的简单引理。

例如

或者

或者，也许更有趣

但是我在任何地方都找不到set.unionor的消除规则set.inter，所以我只是不知道如何使用它们。

1. 我如何证明引理？

另外，查看lean 中集合的定义，我可以看到一些语法，看起来很像纸上数学，但我在依赖类型理论的层面上不理解，例如：

2. 如何将上述示例分解为更简单的依赖/归纳类型概念？

给定集合包含的证明及其反面，我希望能够证明两个集合是相等的。

例如，我知道如何证明以下陈述及其相反的陈述：

鉴于这两个包含证明，我如何证明集合相等，即

他们来自微软，似乎他们是证明助理？除了语法上的差异之外，还有哪些实际方面使它们彼此不同（比如自动化能力、表达能力等）？我是形式验证的新手。

编辑：我不是在问哪个更好，我只是对这些工具提供的不同功能之间的技术比较感兴趣。我正在寻找这样的东西

我正在学习精益证明助手。https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html中的一个练习是为自然数定义前置函数。有人可以帮我吗？

对于我的第一次形式化。我想在精益中定义多项式。第一次尝试如下所示：

现在想使用以下方法测试我的定义：

但是我在构建证明项时遇到了麻烦：

也欢迎对定义本身进行反馈。

我正在尝试学习精益并希望定义一个替换函数，该函数需要两个元素x并y替换给定列表中出现的每个xwith y。

我试图这样定义它：

这给了我以下错误：

我的问题是我不能对 type 使用相等α，所以我想我需要限制α为某种可以确定相等的类型类（就像我在 Haskell 中那样）。我怎样才能做到这一点？

我目前的解决方法是将相等函数作为参数：

我有以下状态：

请注意of_nat构造Z.

有没有一种无痛的方式来实现目标？