-- File: list

-- This file introduces lists.
-- It consists of two parts.
-- 1. Axioms, corresponding to Section 4.5
-- 2. Library, corresponding to Section 4.6


-- naming conventions for lemmas:
-- variables for Lists are always ending in s
-- e.g. as,xs,ys

Load "bool"

-----------------------
-----------------------
--                   --
--  1.  A X I O M S  --
--                   --
-----------------------
-----------------------

Var List : *s -> *s
Var nil : @A:*s. List A

-- Name in lemmas: cons
Var (;) : @A:*s. A -> List A -> List A
Implicit 1 (;)    
InfixR 5 (;)   


Var primreclist : @A,B:*s. B-> (A -> List A -> B -> B) -> List A -> B
Implicit 2 primreclist

Var primreclist_nil : @A,B:*s. @nv:B. @sv: A -> List A -> B -> B.
                                 primreclist nv sv (nil A) = nv

Var primreclist_cons : @A,B:*s. @nv:B. @sv: A -> List A -> B -> B.
                         @head:A. @tail:List A.
                                  primreclist nv sv (head;tail) = 
                                  sv head tail (primreclist nv sv tail)

Var indlist : @A:*s. @P:List A->*p. P (nil A) ->
                                    (@a:A. @as:List A. P as -> P (a;as)) ->
                                    (@as:List A. P as)

-------------------------
-------------------------
--                     --
--  2.  L I B R A R Y  --
--                     --
-------------------------
-------------------------

--------------
-- iterlist --
--------------

-- iterlist is also known as foldr
Def iterlist := \A,B:*s. \nv:B. \sv:A->B->B.
                primreclist nv (\a:A. \dummy:List A. sv a) :
                @A,B:*s. B-> (A -> B -> B) -> List A -> B
Implicit 2 iterlist

Prove iterlist_nil : @A,B:*s. @nv:B. @sv: A -> B -> B.
                                iterlist nv sv (nil A) = nv

Prove iterlist_cons : @A,B:*s. @nv:B. @sv: A -> B -> B.
                         @head:A. @tail:List A.
                                  iterlist nv sv (head;tail) = 
                                  sv head (iterlist nv sv tail)

----------
-- tail --
----------

Def tail := \A:*s. primreclist (nil A) (\hd:A.\tl:List A.\p:List A.tl)
Implicit 1 tail

Prove tail_nil : @A:*s. tail (nil A) = nil A

Prove tail_cons : @A:*s. @a:A. @l:List A. tail (a;l) = l

----------
-- head --
----------

Def head := \A:*s. \a:A. iterlist a (\a':A. \prev:A.a') :
            @A:*s. A -> List A -> A
Implicit 1 head

Prove head_nil : @A:*s. @a:A. head a (nil A) = a

Prove head_cons : @A:*s. @a,b:A. @l:List A. head a (b;l) = b

-------------------------------------------
-- nil and cons are different injections --
-------------------------------------------

Prove nil_is_cons_ : @A:*s. @l:List A. @a:A. Not (nil A = a;l)

Prove cons_is_nil_ : @A:*s. @l:List A. @a:A. Not (a;l = nil A)

Prove cons_is_cons_ : @A:*s. @l1,l2:List A. @a1,a2:A. 
                             a1;l1 = a2;l2 -> a1 = a2 /\ l1=l2



------------
-- concat --
------------

-- Name in lemmas: concat
Def (++) := \A:*s. \as,as' : List A. iterlist as' (
                  \hd:A. \concat_tail : List A. hd;concat_tail) as :
            @A:*s. List A -> List A -> List A
Implicit 1 (++)

Prove nil_concat : @A:*s. @as:List A. (nil A)++as = as

Prove cons_concat : @A:*s. @a:A. @as,as': List A. 
                    (a;as) ++ as' = a ; (as++as')

Prove concat_assoc : @A:*s. @bs,cs,as : List A. (as++bs)++cs = as++(bs++cs)

Prove concat_nil : @A:*s. @as:List A. as ++ (nil A) = as

---------------
-- singleton --
---------------
                                          
Def singleton := \A:*s. \a:A. a ; (nil A) : @A:*s. A -> List A
Implicit 1 singleton

-------------------
-- RELATION Elem --
-------------------

Def Elem := \A:*s.\a:A.\l:List A. 
                 @P:List A -> *p. (@m:List A. P (a;m)) ->
                                  (@m:List A.@b:A. P m -> P (b;m)) ->
                                  P l :
            @A:*s. A -> List A -> *p
Implicit 1 Elem

Prove Elem_a_a_cons : @A:*s.@a:A.@l:List A. Elem a (a;l)

Prove Elem_a_b_cons : @A:*s.@a,b:A.@l:List A. Elem a l -> Elem a (b;l)

Prove Elem_strong_ind : @A:*s.@a:A.@l:List A. Elem a l ->
                           @P:List A -> *p.
                           (@m:List A. P (a;m)) ->
                           (@m:List A. @b:A. Elem a m -> P m -> P (b;m)) ->
                           P l

Prove Elem_exh : @A:*s.@a:A.@l:List A. 
                     Elem a l -> 
                     (Ex m:List A. l = a;m) \/
                     (Ex m:List A. Ex b:A. l = b;m /\ Elem a m) 

Prove Elem_nil_ : @A:*s. @a:A. Not (Elem a (nil A))

Prove Elem_cons_ : @A:*s.@a,b:A. @l:List A. Elem a (b;l) -> a=b \/ Elem a l