list - 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 )，我将不胜感激。我可能依赖一个不成立的假设，但我看不到它。

我还想鼓励您为构建排序列表提供更好的解决方案(也许是一个带有证明值的普通列表，它是排序的？)

Answer 1

我认为您的证明的主要问题在于，正如 Cactus 在评论中指出的那样，您没有插入排序证明工作所需的传递性和反对称等属性。但是，您仍然可以创建一个多态容器:contrib 中 Decidable.Order 的 Poset 类包含您想要的属性。但是，Decidable.Order.Order 在这种情况下更好，因为它封装了关系的整体，确保对于任何两个元素，我们都可以得到其中一个更小的证据。

我有另一种使用 Order 的插入排序算法；它还显式分解 Empty 之间的区别和 NonEmpty列出并保存 max (现在可以添加到列表中的最大元素)类型为 NonEmpty 的值列表，这在一定程度上简化了证明。

我也在学习Idris，所以这段代码可能不是最地道的；另外，非常感谢#idris Freenode IRC channel 上的 Melvar 和 {AS} 帮助我弄清楚为什么以前的版本不起作用。

奇怪的with (y) | <pattern matches on y> sinsert 中的语法有没有为了绑定(bind)y对于 assert_smaller ，因为，由于某种原因，y@(NonEmpty xs)不起作用。

我希望这是有帮助的!

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