Danh sách được sắp xếp theo idris (loại sắp xếp)

Question

Tôi đang viết một luận văn đại học về tính hữu ích của các loại phụ thuộc. Tôi cố gắng để xây dựng một container, mà chỉ có thể được xây dựng thành một danh sách được sắp xếp, vì vậy mà nó được chứng minh được sắp xếp theo trình xây dựng:

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 đòi hỏi một bằng chứng runtime rằng phần tử được thêm vào phía trước là nhỏ hơn hoặc bằng hơn phần tử nhỏ nhất (đầu tiên) trong danh sách được sắp xếp.

Để sắp xếp một danh sách không được phân loại, tôi đã tạo ra một hàm sinsert mà phải mất một danh sách được sắp xếp và chèn một phần tử và trả về một danh sách sắp xếp:

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)) 

tôi đang gặp khó khăn xây dựng chứng minh (?iins21, ?iins22) và tôi sẽ đánh giá cao một số trợ giúp. Tôi có thể dựa vào một giả định không giữ, nhưng tôi không thấy nó.

Tôi cũng muốn khuyến khích bạn để cung cấp một giải pháp tốt hơn cho việc xây dựng một danh sách sắp xếp (có thể là một danh sách bình thường với một giá trị bằng chứng cho thấy nó được sắp xếp?)

Answer 1

Tôi nghĩ rằng vấn đề chính với bằng chứng của bạn có là, như Cactus lưu ý trong một bình luận, là bạn không có tài sản như transitivity và antisymmetry đó là cần thiết cho các bằng chứng của chèn sắp xếp để làm việc. Tuy nhiên, bạn vẫn có thể tạo một thùng chứa đa hình: lớp Poset từ Decidable.Order trong contrib chứa chính xác các thuộc tính mà bạn muốn. Tuy nhiên, Decidable.Order.Order tốt hơn trong trường hợp này vì nó đóng gói toàn bộ quan hệ, đảm bảo rằng đối với bất kỳ hai phần tử nào, chúng ta có thể có được bằng chứng rằng một trong số chúng nhỏ hơn.

Tôi có một thuật toán sắp xếp chèn khác mà tôi vẫn đang làm việc trên đó sử dụng Đơn đặt hàng; nó cũng phân tách rõ ràng khoảng cách giữa các danh sách Empty và NonEmpty và giữ giá trị max (phần tử lớn nhất hiện có thể được thêm vào danh sách) trong loại danh sách NonEmpty, giúp đơn giản hóa chứng minh phần nào.

Tôi cũng đang trong quá trình học Idris, vì vậy mã này có thể không phải là thành ngữ nhất; Ngoài ra, nhiều người cảm ơn Melvar và {AS} trên kênh #idris Freenode IRC để giúp tôi tìm ra lý do tại sao các phiên bản trước đó không hoạt động.

Các lạ with (y) | <pattern matches on y> cú pháp trong sinsert là ở đó để ràng buộc y cho assert_smaller, vì, đối với một số lý do, y@(NonEmpty xs) không hoạt động.

Tôi hy vọng điều này hữu ích!

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