问题标签 [idris]

I've been writing something similar to a Stream. I am able to prove each functor law but I can not figure out a way to prove that it's total:

Gives:

Is there a trick to proving the functor laws over codata which also passes the totality checker?

我试图在 Idris 中创建一个函数，如下所示：

这会将字符串“取消”到它的第一个Char和字符串的其余部分，Nothing如果它为空则返回。

所以我写了这个，但失败了：

所以我然后尝试了这个，有点像Prelude.Strings：

编译并运行没有问题。

我的问题是，为什么我必须使用该with规则以这种方式拆分字符串，为什么我的原始方法会失败？

注意：抱歉，我目前无法访问解释器，因此我还不能在此处编写错误消息。

这是这个后续问题的后续。Zipp 是使用折叠的非递归、非模式匹配的 zip 实现。在无类型 lambda 演算中，我们有：

正如@András_Kovács 所证明的那样，在 Haskell 上，不可能输入这个术语，但 Agda 能够做到，尽管有点复杂。是否可以在 Idris 中优雅地定义这个程序？

我在看中序+预序如何构造唯一的二叉树？并认为用 Idris 写一个正式的证明会很有趣。不幸的是，我很早就被卡住了，试图证明在树中找到元素的方法对应于在它的中序遍历中找到它的方法（当然，我还需要为前序遍历这样做） . 任何想法都会受到欢迎。我对一个完整的解决方案不是特别感兴趣——更多的是帮助我们朝着正确的方向开始。

给定

我至少可以通过两种方式将其转换为列表：

或者

第二种方法似乎使几乎所有事情都变得困难，所以我的大部分努力都集中在第一种上。我这样描述树中的位置：

写起来很容易（使用 的第一个定义inorder）

结果有一个非常简单的结构，对于证明来说似乎相当不错。

编写一个版本也不是很困难

不幸的是，到目前为止，我还没有想出任何方法来编写inorderThenInTree我能够证明是inTreeThenInorder. 我想出的唯一一个用途

我在试图回到那里时遇到了麻烦。

我尝试了一些一般的想法：

1. 使用Vect而不是List尝试使计算左侧和右侧的内容变得更容易。我陷入了它的“绿色粘液”中。

2. 玩弄树的旋转，甚至证明树根处的旋转会导致有充分根据的关系。（我没有玩下面的旋转，因为我从来没有想出一种方法来使用这些旋转的任何东西）。

3. 尝试用有关如何到达它们的信息来装饰树节点。我并没有在这上面花很长时间，因为我想不出一种方法来通过这种方法表达任何有趣的东西。

4. 试图构建我们将回到我们开始的地方的证明，同时构建这样做的函数。这变得非常混乱，我被困在某个地方或其他地方。

在 Haskell 中，我可能会编写一个带有type声明的类型类来创建一个类型族，如下所示：

然后像这样编写实例：

我知道您可以在 Idris 中创建类型类和类型级函数，但是这些方法对给定类型的数据进行操作，而不是对类型本身进行操作。

如何在 Idris 中创建一个类型类约束的类型族，就像上面的那样？

为了学习依赖类型，我正在用 Idris 重写我的旧 Haskell 游戏。目前游戏“引擎”使用内置的整数类型，例如Word8. 我想证明一些涉及这些数字的数值属性的引理（例如，双重否定是身份）。但是，不可能对原始算术运算的行为说些什么。什么会更好，只使用believe_me或其他手动操作（至少对于最基本的属性），或者使用 和其他“高级”数字类型重写我的Nat代码Fin？

我有这个例子

我尝试按此顺序使用策略来证明

所以四步实际上什么都不做。它也与sym. 我做错了什么？伊德里斯本身是否可能存在错误？

Edwin C. Brady 关于 Idris 效果的论文“使用代数效应和相关类型进行编程和推理”包含（未引用的）声明：

尽管 [效果和 monad 转换器] 在功率上不等价 - monad 和 monad 转换器可以表达更多概念 - 捕获了许多常见的有效计算。

有哪些示例可以由单子转换器建模但不能由效果器建模？

我刚开始玩 Idris，并尝试在其中插入一些 Haskell 机器：

但是，我现在想概括Auto a b为AutoM m a b采用一个额外的参数，以便它可以单子生成其输出，并且m是单子。我的直觉是那m会有 type Type -> Type，但随后类型检查器抱怨那不匹配(Type, Type) -> Type。所以我试着让它多态一点：

这至少是类型检查。但是当我尝试时：

然而，这并不好：

而且我无法理解类型错误。为什么在世界上会(a, b)提到类型，而a在定义的任何地方都没有使用const_auto？我觉得自己的定义AutoM已经有问题了，但我真的不知道为什么或如何。

我已经定义了一个运算符，+-（忽略可怕的名字），如下：

目的是它的行为与+上定义的完全一样Fin，但结果的上限更紧 1。据我所知，它可以正常工作。

我遇到的问题是试图证明(FZ +- f) = f任何f : Fin n. 我不希望这通常是真的，因为通常情况下FZ +- f比f调用weakenN. 但是，在FZ具有类型的特定情况下Fin 1，类型（和值）应该匹配。

有没有办法向 Idris 表明我只想在特定情况下断言相等，而不是所有可能的类型FZ？还是我应该采取完全不同的方法？