Idris中的排序列表（插入排序）

Question

我正在撰写一篇本科论文，关于依赖类型的实用性。 我试图构建一个容器，只能构建成排序列表，以证明它是通过构造而排序的：

import Data.So

mutual
  data SortedList : (a : Type) -> {ord : Ord a) -> Type where
    SNil : SortedList a
    SMore : (ord : Ord a) => (el: a) -> (xs : SortedList a) -> So (canPrepend el xs) -> SortedList a

  canPrepend : Ord a => a -> SortedList a -> Bool
  canPrepend el SNil = True
  canPrepend el (SMore x xs prf) = el <= x

SMore需要一个运行时证明，证明要插入的元素小于或等于排序列表中最小（第一个）元素。

为了对未排序的列表进行排序，我创建了一个函数sinsert，它接受一个已排序的列表并插入一个元素，并返回一个已排序的列表：

sinsert : (ord : Ord a) => SortedList a {ord} -> a -> SortedList a {ord}
sinsert SNil el = SMore el SNil Oh
sinsert (SMore x xs prf) el = either 
  (\p => 
    -- if el <= x we can prepend it directly
    SMore el (SMore x xs prf) p
  ) 
  (\np =>  
    -- if not (el <= x) then we have to insert it in the tail somewhere
    -- does not (el <= x) imply el > x ???

    -- we construct a new tail by inserting el into xs
    let (SMore nx nxs nprf) = (sinsert xs el) in
    -- we get two cases:
    -- 1) el was prepended to xs and is now the 
    --    smalest element in the new tail
    --    we know that el == nx
    --    therefor we can substitute el with nx
    --    and we get nx > x and this also means 
    --    x < nx and also x <= nx and we can
    --    prepend x to the new tail
    -- 2) el was inserted somewhere deeper in the
    --    tail. The first element of the new tail
    --    nx is the same as it was in the original
    --    tail, therefor we can prepend x to the
    --    new tail based on the old proof `prf`
    either 
      (\pp => 
        SMore x (SMore nx nxs nprf) ?iins21
      )
      (\npp => 
        SMore x (SMore nx nxs nprf) ?iins22
      ) (choose (el == nx))
  ) (choose (el <= x))

我在构建证明时遇到了麻烦(?iins21,?iins22)，希望能得到一些帮助。我可能在依赖一个不成立的假设，但我没有看出来。

我还想鼓励您提供更好的解决方案来构建排序列表（也许是一个普通列表，并附带一个证明值表明它已经排序？）

- bssstudio

---

我在Agda中有一个答案，我应该发布吗？ - effectfully

我认为你无法编写这些证明，因为你的 SortedList 类型对于排序的复杂性太过“盲目”。例如，当 Ord 类型类没有任何证明义务时，你无法证明像 transitivity : Ord a => {x : a} -> So (x <= y) -> So (y <= z) -> So (x <= z) 这样的东西。 - Cactus

你可以通过将a固定为例如Nat并使用像x\LTE`y这样的命题来代替So(x<=y)`，从而可能取得更大的进展。 - Cactus

Answer 1

我认为你的证明主要问题在于，正如Cactus在评论中指出的那样，你没有像传统插入排序证明所需的可传递性和反对称性等属性。但是，你仍然可以创建一个多态容器：contrib中Decidable.Order中的Poset类恰好包含你所需的属性。然而，在这种情况下，Decidable.Order.Order更好，因为它封装了关系的完全性，确保我们可以为任何两个元素获得一个证明，其中一个较小。我有另一个插入排序算法正在进行中，它也使用Order；它还明确地区分了Empty和NonEmpty列表，并将max（现在可以添加到列表中的最大元素）值保留在NonEmpty列表类型中，这样可以简化证明。我还在学习Idris，所以这段代码可能不是最惯用的；同时，非常感谢Melvar和{AS}在#idris Freenode IRC频道上帮助我解决之前版本的问题。

在`sinsert`中，奇怪的`with (y) | <pattern matches on y>`语法是为了绑定`y`用于`assert_smaller`，因为由于某种原因，`y@(NonEmpty xs)`无法工作。请注意保留HTML标签。

希望这对您有所帮助！

import Data.So
import Decidable.Order

%default total

data NonEmptySortedList :  (a : Type)
                        -> (po : a -> a -> Type)
                        -> (max : a)
                        -> Type where
  SOne   : (el : a) -> NonEmptySortedList a po el
  SMany  :  (el : a)
         -> po el max
         -> NonEmptySortedList a po max
         -> NonEmptySortedList a po el

data SortedList : (a : Type) -> (po : a -> a -> Type) -> Type where
  Empty : SortedList _ _
  NonEmpty : NonEmptySortedList a po _ -> SortedList a po

head : NonEmptySortedList a _ _ -> a
head (SOne a) = a
head (SMany a _ _) = a

tail : NonEmptySortedList a po _ -> SortedList a po
tail (SOne _) = Empty
tail (SMany _ _ xs) = NonEmpty xs

max : {m : a} -> NonEmptySortedList a _ m -> a
max {m} _ = m

newMax : (Ordered a po) => SortedList a po -> a -> a
newMax Empty x = x
newMax (NonEmpty xs) x = either (const x)
                                (const (max xs))
                                (order {to = po} x (max xs))

either' :  {P : Either a b -> Type}
        -> (f : (l : a) -> P (Left l))
        -> (g : (r : b) -> P (Right r))
        -> (e : Either a b) -> P e
either' f g (Left l) = f l
either' f g (Right r) = g r

sinsert :  (Ordered a po)
        => (x : a)
        -> (xs : SortedList a po)
        -> NonEmptySortedList a po (newMax xs x)
sinsert x y with (y)
  | Empty = SOne {po = po} x
  | (NonEmpty xs) = either' { P = NonEmptySortedList a po
                            . either (const x) (const (max xs))
                            }
                            insHead
                            insTail
                            (order {to = po} x (max xs))
  where insHead : po x (max xs) -> NonEmptySortedList a po x
        insHead p = SMany x p xs
        max_lt_newmax : po (max xs) x -> po (max xs) (newMax (tail xs) x)
        max_lt_newmax max_xs_lt_x with (xs)
          | (SOne _) = max_xs_lt_x
          | (SMany _ max_xs_lt_max_xxs xxs)
            = either' { P = po (max xs) . either (const x)
                                                 (const (max xxs))}
                      (const {a = po (max xs) x} max_xs_lt_x)
                      (const {a = po (max xs) (max xxs)} max_xs_lt_max_xxs)
                      (order {to = po} x (max xxs))
        insTail : po (max xs) x -> NonEmptySortedList a po (max xs)
        insTail p = SMany (max xs)
                          (max_lt_newmax p)
                          (sinsert x (assert_smaller y (tail xs)))

insSort :  (Ordered a po) => List a -> SortedList a po
insSort = foldl (\xs, x => NonEmpty (sinsert x xs)) Empty

- Lucy Maya Menon