问题标签 [lean]

我创建了以下 poset 定义，双重定义不检查反对称。我不确定如何使它工作，有什么建议吗？

鉴于(a : Z)和(a >= 0)，我想有(n : N)这样的n = a。这当然有点麻烦，因为n = a是异构平等。

我发现nat_abswhich 做了类似的事情，除了当我有一个负整数时它也处理这种情况，我知道我没有。

在精益中如何处理这种情况？

真正的初学者在这里提问。如何在精益中表示多个假设的问题？例如：

给定

• 一个
• A→B
• A→C
• B→D
• C→D

证明命题 D。

（问题取自 The Incredible Proof Machine，第 2 课第 3 题。我实际上正在阅读逻辑与证明，第 4 章，精益中的命题逻辑，但那里的练习较少）

显然，通过两次应用 ponens 来证明这完全是微不足道的，我的问题是我如何首先表示这个问题？！这是我的证明：

试试看！

我想我已经做了太多的打包问题然后拆包的饭菜，有人可以告诉我一个更好的方式来表达这个问题吗？

我在 Coq 的 SSReflect 扩展中发现了两个约定，它们看起来特别有用，但我还没有看到它们在较新的依赖类型语言（Lean、Agda、Idris）中被广泛采用。

首先，可能的谓词表示为布尔返回函数，而不是归纳定义的数据类型。这在默认情况下带来了可判定性，为计算证明开辟了更多机会，并通过避免证明引擎需要携带大量证明条款来提高检查性能。我看到的主要缺点是在证明时需要使用反射引理来操纵这些布尔谓词。

其次，具有不变量的数据类型被定义为包含简单数据类型和不变量证明的相关记录。例如，固定长度的序列在 SSReflect 中定义如下：

Aseq和该序列长度为某个值的证明。这与 Idris 定义这种类型的方式相反：

一种依赖类型的数据结构，其中不变量是其类型的一部分。SSReflect 方法的一个优点是它允许重用，例如，许多为它们定义的函数seq和关于它们的证明仍然可以与tuple（通过在底层上操作seq）一起使用，而使用 Idris 的方法，像reverse,append和类似的函数需要被重写为Vect. Lean 实际上在其标准库中具有等效的 SSReflect 样式vector，但它也具有 Idris 样式array，该样式似乎在运行时具有优化的实现。

一本面向 SSReflect 的书甚至声称Vect n A样式方法是一种反模式：

在依赖类型语言和 Coq 中，一个常见的反模式是将这些代数属性编码到数据类型和函数本身的定义中（这种方法的典型示例是长度索引列表）。虽然这种方法看起来很吸引人，因为它展示了依赖类型捕获数据类型和函数的某些属性的能力，但它本质上是不可扩展的，因为总会有另一个感兴趣的属性，这是设计者没有预见到的数据类型/函数，因此无论如何它都必须被编码为外部事实。这就是为什么我们提倡这种方法，其中数据类型和函数的定义尽可能接近程序员定义它们的方式，并且它们的所有必要属性都被单独证明。

因此，我的问题是，为什么这些方法没有被更广泛地采用。有没有我遗漏的缺点，或者它们的优点在对依赖模式匹配的支持比 Coq 更好的语言中不太重要？

如何在编程代码引用中省略一部分编程代码？

特别是我有以下代码片段（来自精益证明助手）：

我想省略一部分，比如：

对于文本引用，我知道我们可以使用 [...] 来省略部分引用。

但是在编程代码引号的情况下我们使用什么？

我是一个绝对的初学者，而不是程序员，正在尝试使用Logic 和 Proof学习形式验证。我不能在精益中导入任何东西。

我提取二进制文件的 tar 文件，/tmp然后执行

除非我导入任何东西，否则它可以工作。所以如果我的文件test.lean只是说

没有错误。但是，如果相同的文件改为说

我收到错误消息

类似的错误发生在import data.nat.

我做错了什么，我该怎么办？我正在使用 Ubuntu 16.04。请注意，由于我是初学者，我从未从源代码编译过任何东西。

试图证明正数之和是正数。

在声明中sw_pos，Lean 抱怨说它“不知道如何合成占位符上下文” sw。

如何解决此错误？

我在 VS Code 上使用Lean，这是一种开源定理证明器和编程语言。许多命令需要'\'编写数学符号，就像 LaTeX 一样。

Lean on VS Code 和 LaTeX 的本质区别在于，为了编译数学符号（例如，get\forall和数学'forall'符号之间的区别），当您在符号后面键入字符时，必须出现下划线\。

我遇到的问题是这个下划线

1) 在我输入时并不总是出现\

2) 消失得太快。

我的问题是：这是一个错误，还是有办法更改 VS 代码中的设置，使下划线始终出现在\?

任何答案将不胜感激。