用案例证明函数定理

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 的 case 表达式的相应分支匹配似乎是合理的（所以 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 we ultimately had to remove all cases in such functions and define separate top-level helpers that match on the case condition, e.g., like here.

用案例证明函数定理

Proving theorems about functions with cases

idris