问题标签 [lean]

我已经在列表上定义了一个反向函数，并且我试图证明一个空列表的反向是空的琐碎属性。它应该可以通过反身性来证明：

但是，当我运行此代码时，出现错误：

这是什么意思？

我正在尝试将 Coq 术语的字面翻译成精益术语，但意识到我不知道如何翻译 Coq 原语fix，如下所示：

我不是在问如何在精益文档中很好地解释的归纳类型上定义递归函数，而是如何定义“递归让”，即其主体调用自身的 lambda 抽象。我假设精益中存在等效的原语。

谢谢你。

说我的证明目标包括nat.succ (nat.succ 0)，我想快速重写它说2；我可以定义一个全新的定理：

然后将该定理与 一起使用rw，但这似乎很笨拙。在我的证明中，有没有办法在一行中做到这一点？

在自然数游戏中，use关键字通过为量化变量分配具体值来解决包含存在量词的目标。单独使用精益似乎无法使用；你做什么呢？

我正在玩自然数游戏，我已经完成了mul_add. 证明如下所示：

为什么我不需要hA在这个证明中使用归纳假设？直觉上，我似乎应该“用尽”证明过程中产生的一切。作为参考，产生的两个归纳假设是

我在带有美式键盘的 macOS Catalina 下使用 VS Code 中的 Lean。如何输入暗示箭头、联合、交集、子集等符号？

是否有一些内置或附加调色板来促进这一点？或者我是否必须使用 Option 组合键，如果是，我在哪里可以找到合适的代码？

尝试在精益文档中进行第3 章练习，但很难理解所有术语，因为我对编写证明的了解几乎为零。我想了解更多，但需要一些帮助。

我一直在尝试解决这个例子：

example : p ∨ q ↔ q ∨ p := sorry

不知道从哪里开始。是否有我缺少解释的答案键？

如果我做出定义

然后按预期#check f返回f:nat -> nat -> nat。

相反，如果我尝试定义

然后 Lean 抱怨说 x 有 typenat但应该有 type nat -> nat。

为什么是这样？

下面的代码验证失败，并显示“无法为...合成类型类实例⊢ has_pow R R”。

这看起来很奇怪，因为我^在封闭范围内的相同类型上使用了相同的运算符 ()，并且没有问题！具有相同签名的第二个定理可以很好地进行类型检查。

为什么它只在重写内部失败？如何在不更改定理类型签名的情况下修复它？

当我执行我的精益定理证明的正常过程时，我意识到我当前的文件需要很长时间才能编译。然后我将问题缩小到我试图证明两个字符串是不同的部分：

仅这个小引理就需要 15 秒才能在我的（尽管）慢机器上编译。事情严重错误。

我不是一个流利的精益用户，所以猜测我不应该使用这种cases策略 string。我还可以做些什么？

Coq 中相应的引理可以正常工作，没有任何时间问题：