问题标签 [idris]

将 Coq 源代码转换为 Idris 有哪些有用的指导方针（例如，它们的类型系统有多相似以及翻译证明可以做什么）？据我所知，Idris 的内置战术库很小但可扩展，所以我想通过一些额外的工作应该可以做到这一点。

我想将一个向量划分为两个新向量。

我们无法知道各个向量的长度是多少，但结果向量的总和必须等于参数。我试图捕获这个属性如下：

但是 Idris 报告（指向“分区 p []”）在详细说明 Main.partition 的左侧时：

为什么会这样？

对我来说，如果 "0 = m + n" 比 m = n = 0 似乎很明显。如果让 Idris 相信这一点，该怎么办？

我已经阅读了 Fortify 静态检查工具的一些文档。此工具使用的概念之一称为taints。某些来源（例如 Web 请求）提供的数据以一种或多种方式受到污染，而某些接收器（例如 Web 响应）则要求数据不受污染。

Fortify 的好处是您可以拥有多种类型的污点。例如，您可以使用标记srand输出，NON_CRYPTO_RAND然后要求在将变量用于加密目的时不存在此污点。其他示例包括非绑定检查号码等。

是否可以使用 Haskell 中使用的更强大的静态类型系统或其他具有更复杂类型系统的编程语言来建模污点？

在 Haskell 中，我可以做诸如此类的类型，Tainted [BadRandom,Unbounded] Int但使用它们进行计算似乎相当困难，因为这种新的类型约束也是不限制污点的操作。

有更好的方法来实现这一点吗？关于该主题的任何现有工作？

我试图证明，在我看来是一个合理的定理：

归纳证明到了我需要证明这一点的地步：

当我尝试使用交互式证明者来证明它（为了简单起见，引理）时会发生这种情况：

我觉得我一定错过了关于减号的定义的一些东西，所以我在源代码中查找了它：

我需要的定义就在那里！minus left Z = left. 我的理解是 Idris 应该只是替换minus m 0为mhere，然后这是反身成立的。我错过了什么？

我正在写一篇关于依赖类型有用性的本科论文。我正在尝试构造一个容器，它只能构造成一个排序列表，以便证明它是按构造排序的：

SMore需要运行时证明被前置的元素小于或等于排序列表中的最小（第一个）元素。

为了对未排序的列表进行排序，我创建了一个函数sinsert，它接受一个排序的列表并插入一个元素并返回一个排序的列表：

我在构建证明 ( ?iins21, ?iins22) 时遇到了麻烦，我将不胜感激。我可能依赖于一个不成立的假设，但我看不到它。

我还想鼓励您为构建排序列表提供更好的解决方案（也许是一个带有证明值的普通列表，它是排序的？）

我是依赖类型的新手，对两者之间的区别感到困惑。似乎人们通常说一种类型由另一种类型参数化并由某个值索引。但是在依赖类型语言中，类型和术语之间不是没有区别吗？参数和指数之间的区别是基本的吗？你能告诉我一些例子，说明它们在编程和定理证明中的含义不同吗？

我只阅读了标准教程并且摸索了一下，所以我可能会遗漏一些简单的东西。

如果这在 Idris 中是不可能的，请解释原因。此外，如果可以用另一种语言完成，请提供代码示例并解释使之成为可能的该语言类型系统的不同之处。

这是我的方法。问题首先出现在第三部分。

创建一个已知类型的空列表

这在 REPL 中编译并显示为[] : List Nat. 优秀的。

泛化到任何提供的类型

不出所料，这有效并且v' == v.

Ord将类型约束到类的实例

最后一行失败并出现此错误：

Nat是 的一个实例Ord，那么有什么问题呢？我尝试将Natsv''替换为Bool（不是 的实例Ord），但错误没有变化。

另一个角度...

使Ord t显式参数满足类型检查器吗？显然不是，但即使它确实要求调用者传递冗余信息也不理想。

这次错误更详细：

我可能错过了一些关于如何根据类型声明检查值的关键见解。

我想对此进行编译：

这无法编译，因为编译器无法n与n + m. 我知道这是因为takefor Vect's 的签名，但我不知道如何去向编译器展示它们可以统一 if m = 0。

在 idris 中，如何约束 Algebraic Data Type 中的参数类型？

在haskell，我会这样做：

我可以在伊德里斯这样做吗？

在 haskell 中，可以这样写：

是否可以在 Idris 中编写等效的东西，而不用ifThenElse（我的实际情况比上面的情况更复杂）？