时间戳

首页 > 解决方案 > 用案例证明有关函数的定理

idris - 用案例证明有关函数的定理

问题描述

假设我们有一个函数merge，它只是合并两个列表：

Order : Type -> Type
Order a = a -> a -> Bool

merge : (f : Order a) -> (xs : List a) -> (ys : List a) -> List a
merge f xs [] = xs
merge f [] ys = ys
merge f (x :: xs) (y :: ys) = case x `f` y of
                                   True  => x :: merge f xs (y :: ys)
                                   False => y :: merge f (x :: xs) ys

我们想证明一些聪明的东西，例如，合并两个非空列表会产生一个非空列表：

mergePreservesNonEmpty : (f : Order a) ->
                         (xs : List a) -> (ys : List a) ->
                         {auto xsok : NonEmpty xs} -> {auto ysok : NonEmpty ys} ->
                         NonEmpty (merge f xs ys)
mergePreservesNonEmpty f (x :: xs) (y :: ys) = ?wut

检查孔的类型wut给了我们

wut : NonEmpty (case f x y of   True => x :: merge f xs (y :: ys) False => y :: merge f (x :: xs) ys)

到目前为止有道理！因此，让我们按照这种类型的建议继续进行大小写拆分：

mergePreservesNonEmpty f (x :: xs) (y :: ys) = case x `f` y of
                                                    True => ?wut_1
                                                    False => ?wut_2

希望 and 的类型wut_1与's case 表达式wut_2的相应分支相匹配似乎是合理的（所以会是类似的东西，可以立即满足），但我们的希望落空了：类型与原始 的类型相同。mergewut_1NonEmpty (x :: merge f xs (y :: ys))wut

事实上，唯一的方法似乎是使用 -with子句：

mergePreservesNonEmpty f (x :: xs) (y :: ys) with (x `f` y)
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | True = ?wut_1
  mergePreservesNonEmpty f (x :: xs) (y :: ys) | False = ?wut_2

在这种情况下，类型将与预期的一样，但这会导致每个with分支都重复函数参数（一旦with嵌套，情况会变得更糟），with而且似乎与隐式参数不兼容（但这可能值得一个问题它自己的）。

那么，为什么在这里没有case帮助呢，除了纯粹的实现方式之外，是否还有其他原因不将其行为与 of 匹配with，还有其他方法可以编写这个证明吗？

标签： idris

解决方案

有一个关于证明事情的问题case：https ://github.com/idris-lang/Idris-dev/issues/4001

正因为如此，在idris-bi中，我们最终不得不删除case此类函数中的所有 s 并定义与 case 条件匹配的单独的顶级助手，例如，像here。

推荐阅读