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

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，然后使用prf 在x 前面添加rest 和ysi 的结果，递归地证明这一点似乎是合理的。此时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

一些建议：

1. 使用Data.So x 代替x = True，生成运行时函数 更容易编写。
2. 将Ord a从构造函数提升到类型，使其 更清楚使用哪种排序（并且您不必匹配 {a} appendIncreasing，我猜）。
3. 别忘了你可以 匹配构造函数中的变量，所以不要重复 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))

应该使证明事情变得容易得多，尤其是如果您想包含空列表。