证明连接两个递增列表会产生递增列表

Question

让我们考虑一个表明列表中的元素按递增顺序排列的谓词（为了简单起见，我们只处理非空列表）：

mutual
  data Increasing : List a -> Type where
    SingleIncreasing  : (x : a) -> Increasing [x]
    RecIncreasing     : Ord a => (x : a) ->
                                 (rest : Increasing xs) ->
                                 (let prf = increasingIsNonEmpty rest
                                  in x <= head xs = True) ->
                                 Increasing (x :: xs)

  %name Increasing xsi, ysi, zsi

  increasingIsNonEmpty : Increasing xs -> NonEmpty xs
  increasingIsNonEmpty (SingleIncreasing y) = IsNonEmpty
  increasingIsNonEmpty (RecIncreasing x rest prf) = IsNonEmpty

现在让我们试着用这个谓词写一些有用的引理。让我们首先展示连接两个递增列表会产生一个递增列表，前提是第一个列表的最后一个元素不大于第二个列表的第一个元素。这个引理的类型是：

appendIncreasing : Ord a => {xs : List a} ->
                            (xsi : Increasing xs) ->
                            (ysi : Increasing ys) ->
                            {auto leq : let xprf = increasingIsNonEmpty xsi
                                            yprf = increasingIsNonEmpty ysi
                                        in last xs <= head ys = True} ->
                            Increasing (xs ++ ys)

现在让我们尝试实现它！一个合理的方法似乎是在 xsi 上区分大小写。 xsi 是单个元素的基本情况是微不足道的：

appendIncreasing {leq} (SingleIncreasing x) ysi = RecIncreasing x ysi leq

另一种情况比较复杂。鉴于

appendIncreasing {leq} (RecIncreasing x rest prf) ysi = ?wut

通过依赖 leq 递归证明加入 rest 和 ysi 的结果似乎是合理的，然后使用 prf。此时 leq 实际上是 last (x :: xs) <= head ys = True 的证明，而对 appendIncreasing 的递归调用则需要有 last xs <= head ys = True 的证明。我没有找到直接证明前者暗示后者的好方法，所以让我们回过头来重写并首先写一个引理，表明列表的最后一个元素不会因添加到前面而改变：

lastIsLast : (x : a) -> (xs : List a) -> {auto ok : NonEmpty xs} -> last xs = last (x :: xs)
lastIsLast x' [x] = Refl
lastIsLast x' (x :: y :: xs) = lastIsLast x' (y :: xs)

现在我希望能够写

appendIncreasing {xs = x :: xs} {leq} (RecIncreasing x rest prf) ysi =
  let rest' = appendIncreasing {leq = rewrite lastIsLast x xs in leq} rest ysi
  in ?wut

但我失败了：

When checking right hand side of appendIncreasing with expected type
        Increasing ((x :: xs) ++ ys)

When checking argument leq to Sort.appendIncreasing:
        rewriting last xs to last (x :: xs) did not change type last xs <= head ys = True

我该如何解决这个问题？

而且，也许我的证明设计不是最理想的。有没有办法以更有用的方式表达这个谓词？

Answer 1

如果 rewrite 没有找到正确的谓词，请尝试用 replace 明确说明。

appendIncreasing {a} {xs = x :: xs} {ys} (RecIncreasing x rest prf) ysi leq = 
  let rekPrf = replace (sym $ lastIsLast x xs) leq
               {P=\T => (T <= (head ys {ok=increasingIsNonEmpty ysi})) = True} in
  let rek = appendIncreasing rest ysi rekPrf in
  let appPrf = headIsHead xs ys {q = increasingIsNonEmpty rek} in
  let extPrf = replace appPrf prf {P=\T => x <= T = True} in
  RecIncreasing x rek extPrf

和

headIsHead : (xs : List a) -> (ys : List a) ->
             {auto p : NonEmpty xs} -> {auto q : NonEmpty (xs ++ ys)} ->
             head xs = head (xs ++ ys)
headIsHead (x :: xs) ys = Refl

一些建议：

使用Data.So x代替x = True，使run-time函数更容易写。
将Ord a从构造函数提升到类型，使其成为更清楚使用哪种顺序（并且您不必匹配我猜 {a} 在 appendIncreasing。
别忘了你可以匹配构造函数中的变量，而不是重复 Increasing xs 有 NonEmpty xs, 只需使用 Increasing (x :: xs).

导致：

data Increasing : Ord a -> List a -> Type where
  SingleIncreasing : (x : a) -> Increasing ord [x]
  RecIncreasing    : (x : a) -> Increasing ord (y :: ys) ->
                                So (x <= y) ->
                                Increasing ord (x :: y :: ys)

appendIncreasing : {ord : Ord a} ->
                   Increasing ord (x :: xs) -> Increasing ord (y :: ys) ->
                   So (last (x :: xs) <= y) ->
                   Increasing ord ((x :: xs) ++ (y :: ys))

应该使证明事情变得容易得多，特别是如果你想包含空列表。

证明连接两个递增列表会产生递增列表

Proving that concatenating two increasing lists produces an increasing list

idris