问题标签 [equational-reasoning]

我正在关注 Coursera 上的 Scala 函数式编程讲座，在视频 5.7 的结尾，Martin Odersky 要求通过归纳证明以下等式的正确性：

当涉及多个列表时如何处理归纳证明？

我检查了 xs 为 Nil 和 ys 为 Nil 的基本情况。我已经通过归纳证明，当 xs 被 x::xs 替换时，等式成立，但是我们是否还需要检查 ys 被 y::ys 替换的等式？

在那种情况下（不会过多地破坏练习......无论如何都没有评分）你如何处理：(xs ++ (y::ys)) map f？

这是我在类似示例中使用的方法，以证明

证明（省略基本情况和简单的 x::xs 情况）：

这是正确的吗 ？

注意这个程序：

和的两个定义与等式推理相同。然而，编译作品的第二个定义，但第一个没有，出现此错误：

似乎RankNTypes打破了等式推理。有没有办法在 Haskell 中拥有教堂编码列表而不会破坏它？

我如何进行归纳以建立陈述moll n = doll n，与

我试图证明 n = 0 的基本情况

现在n+1，证明

但是现在呢？我怎样才能进一步简化它？

return a = return b如果那时，你能证明a=b吗？当我使用 时=，我的意思是在法律和证明意义上，而不是Eq阶级意义上。

我知道的每个 monad 似乎都满足这一点，我想不出一个有效的 monad 不会（Const a是函子和应用程序，但不是 monad。）

我在 Haskell 中找到了这个关于等式推理和证明的练习。给出以下代码：

现在我必须证明这一点exec(comp e) s = eval e : s。

所以到目前为止我找到了这个答案：

我们必须证明这一点exec (comp e) s = eval e : s。

第一种情况：假设e = (Val n). 那么comp (Val n) = [PUSH n]，所以我们要证明这一点exec ([PUSH n]) s = eval ([PUSH n] : s)。我们发现exec ([PUSH n]) s = exec [] (n:s) = (n:s)使用exec的函数定义。

现在eval (Val n) : s = n : s。第一种情况OK！

第二种情况：假设e = (Add x y). 然后comp (Add x y) = comp x ++ comp y ++ [ADD]。

但现在我正在努力解决这种递归使用 comp 的问题。我应该在这些树上使用某种形式的树和归纳法来证明这一点吗？我不完全确定该怎么做。

我正在学习 Haskell 的语义，在那里我遇到了这个问题：

我已经尝试过了，但仍然无法得出答案。如果有人向我解释如何证明这一点，那就太好了。谢谢你。

我马上说这是一个任务，我不是在寻找答案 - 只是一些方向，因为我已经研究了很长一段时间了。给定以下尾递归求和函数：

我们必须通过归纳证明：

在证明了基本情况（在 xs 上感应并将 ys 视为常数）后，我得出：

我们的讲师经历了一个更简单的例子（sum1 xs = sum2 xs，sum1 是简单的递归），当他达到你不能让它们变得更相似的地步时，他证明了一个“更强的属性”，通过注意到类似sum2 xs acc = acc + xs 的总和。然后他设置了一个涉及“for all acc”的归纳假设，然后将 acc 设置为 0。

我遇到的主要问题是 acc 已经在 LHS 和 RHS 上，所以我觉得我已经接近了，但我并没有真正证明更强大的属性（这个问题没有具体要求，但我认为我们应该使用它）。此外，我不确定在将元素取出（或将它们插入）函数时，我可以在多大程度上使用加法的关联性。

任何帮助表示赞赏！

当 f 严格时，它适用于每个 xs 列表。谁能给我举个例子，为什么使用非严格的 f 它不起作用？

我正在尝试为 Setoids（具有等价关系的类型）建模 Agda 风格的等式推理证明。我的设置如下：

使用这样的接口，我可以 Syntax.PreorderReasoning对 Idris 库中的一些等式推理组合器进行建模。

与 Idris 库的主要区别只是将命题等式及其相关函数替换为使用VerifiedEquality接口中的函数。

到目前为止，一切都很好。但是当我尝试使用这样的组合器时，我遇到了我认为与接口解析有关的问题。由于代码是我正在研究的矩阵库的一部分，因此我将其相关部分发布在以下要点中。

错误发生在以下证明中

返回以下错误消息：

至少在我看来，这个错误似乎与与语法扩展不能很好交互的接口解析有关。

我的经验是，这种奇怪的错误可以通过显式传递隐式参数来解决。问题是这样的解决方案会破坏等式推理组合证明的“可读性”。

有没有办法解决这个问题？重现此错误的相关部分可在先前链接的gist中找到。

我在 Idris 中写了以下证明：

但当然那不是我写的。我写的是这样的：

如果我在 Agda 中编写，我可以使用该≡-Reasoning模块来跟踪我的位置；例如，上面可以这样完成（省略实际的证明步骤，因为它们完全相同）：

有没有办法在伊德里斯做类似的事情？

（注意：当然，在 Agda 中我不会手动证明这一点：我只是使用半环求解器并完成它；但https://github.com/FranckS/RingIdris上的 Idris 半环求解器似乎以 Idris 0.11 为目标，而我正在使用 1.1.1 ...)