dk_list.dk

#NAME dk_list.

(; Polymorphic lists ;)
list : cc.uT -> cc.uT.
List : cc.uT -> Type.
[A] cc.eT (list A) --> List A.

(; Constructors ;)
nil : A : cc.uT -> List A.
cons : A : cc.uT -> cc.eT A -> List A -> List A.

(; Case distinction ;)
def match : A : cc.uT ->
            P : (List A -> cc.uT) ->
            cc.eT (P (nil A)) ->
            (a : cc.eT A -> l : List A -> cc.eT (P (cons A a l))) ->
            l : List A ->
            cc.eT (P l).

[Hnil]      match _ _ Hnil _ (nil _) --> Hnil
[Hcons,a,l] match _ _ _ Hcons (cons _ a l) --> Hcons a l.

(; Non dependant case distinction ;)
def simple_match : A : cc.uT ->
               return : cc.uT ->
               cc.eT return ->
               (cc.eT A -> List A -> cc.eT return) ->
               List A ->
               cc.eT return
             :=
               A : cc.uT =>
               return : cc.uT =>
               match A (_x : List A => return).

(; Append ;)
def append : A : cc.uT -> List A -> List A -> List A.
[l] append _ (nil _) l --> l
[A,a1,l1,l2] append A (cons _ a1 l1) l2 --> cons A a1 (append A l1 l2).

(; Associativity rule, breaks confluence automatic verification. ;)
(; [A,l1,l2,l3] append A (append _ l1 l2) l3 --> append A l1 (append A l2 l3). ;)

(; Map ;)
def map : A : cc.uT ->
          B : cc.uT ->
          (cc.eT A -> cc.eT B) -> List A -> List B.
[B] map _ B _ (nil _) --> nil B
[A,B,f,a,l] map A B f (cons _ a l) --> cons B (f a) (map A B f l).

(; Composition rule, breaks confluence automatic verification. ;)
(; [A,B,C,f,g,l] map B C g (map A _ f l) --> map A C (x : cc.eT A => g (f x)) l. ;)

def mem : A : cc.uT ->
          (cc.eT A -> cc.eT A -> cc.eT dk_bool.bool) ->
          cc.eT A ->
          List A ->
          cc.eT dk_bool.bool.
[] mem _ _ _ (nil _) --> dk_bool.false
[A,eq,a1,a2,l]
    mem A eq a1 (cons _ a2 l) --> dk_bool.or (eq a1 a2) (mem A eq a1 l).



def map_id :
      B : cc.uT ->
      l : List B ->
      dk_logic.eP (dk_logic.equal (list B) (map B B (x : cc.eT B => x) l) l).
[B] map_id B (nil _) --> dk_logic.refl (list B) (nil B)
[A,a,l]
    map_id A (cons _ a l)
      -->
    dk_logic.equal_congr
      (list A)
      (list A)
      (cons A a)
      (map A A (x : cc.eT A => x) l)
      l
        (map_id A l).


dlist : A : cc.uT -> cc.eT A -> cc.uT.
dnil : A : cc.uT -> a : cc.eT A -> cc.eT (dlist A a).
dcons : A : cc.uT ->
        a : cc.eT A ->
        f : (cc.eT (dlist A a) -> cc.uT) ->
        l : cc.eT (dlist A a) ->
        cc.eT (f l) ->
        cc.eT (dlist A a).