基于分情况函数的定理证明：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，它的类型签名如下：

mergePreservesNonEmpty : (f : Order a) -> (xs : List a) -> (ys : List a) ->
                         xs /= [] -> ys /= [] -> merge f xs ys /= []

证明思路与实现 #

证明的核心逻辑非常直观：当两个输入列表xs和ys都非空时，它们必然可以被解构为x :: xs'和y :: ys'的形式，此时merge函数会进入第三个匹配分支。不管x f y的结果是True还是False，函数都会返回一个以x或y作为首元素的列表——这样的列表显然是非空的。

我们可以直接通过模式匹配和case分析来完成证明：

mergePreservesNonEmpty f (x :: xs') (y :: ys') _ _ =
  case x `f` y of
    True => Refl  -- 此时结果是x :: ...，显然非空，Refl直接构造相等性证据
    False => Refl -- 此时结果是y :: ...，同样非空，Refl构造证据

解释一下证明细节 #

1. 我们直接对xs和ys做模式匹配，因为前提已经保证了它们非空，所以可以安全地解构为x :: xs'和y :: ys'，两个下划线_代表我们不需要使用xs /= []和ys /= []这两个前提的具体证据。
2. 接着对x f y的结果做case分析：
   • 如果结果是True，merge返回x :: merge f xs' (y :: ys')，这个列表的首元素是x，显然不等于空列表[]，用Refl就能构造出merge f xs ys /= []的证据。
   • 如果结果是False，merge返回y :: merge f (x :: xs') ys'，同理，这个列表以y开头，必然非空，同样用Refl完成证明。

这样就完整证明了这个定理，整个过程完全贴合merge函数的定义逻辑，没有复杂的额外步骤。

内容的提问来源于stack exchange，提问作者0xd34df00d