用案例证明关于函数的定理

Question

假设我们有一个函数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

似乎有理由希望wut_1和wut_2的类型与merge的案例表达式的相应分支相匹配(因此wut_1会像NonEmpty (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在这里没有帮助，除了纯粹的实现之外，还有什么原因没有将其行为与with的行为相匹配，还有其他方法可以编写这个证明吗？

Answer 1

只有当新信息以某种方式向后传播到参数时，|左侧的东西才是必需的。

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) with (x `f` y)
| True = IsNonEmpty
| False = IsNonEmpty
-- for contrast
sym' : (() -> x = y) -> y = x
sym' {x} {y} prf with (prf ())
-- matching against Refl needs x and y to be the same
-- now we need to write out the full form
sym' {x} {y=x} prf | Refl = Refl

至于为什么会这样，我相信这只是实现，但更了解的人可能会对此提出异议。

Answer 2

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

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