-- File: list2

-- 1. Lemmas concerning existing functions/predicates
--    exhaustion property, and lemmas about Perm, insert, concat, Elem
-- 2. New functions with their properties.
--    elem, null, genCount, count, snoc, length, init, last, reverse

Path "../lol"
Load "logic2"
Load "bool2" 
Load "nat2"  
Load "list"
Load "sort"  


--------------------------------------------------------------------
--------------------------------------------------------------------
--                                                                --
--  1. L E M M A S   F O R   E X I S T I N G   F U N C T I O N S  --
--                                                                --
--------------------------------------------------------------------
--------------------------------------------------------------------

-- exhaustion property --
Prove exh_list: @A:*s. @l:List A. l = nil A \/ Ex hd:A. Ex tl:List A. l=hd;tl

-- Lemma about Perm --
Prove Perm_cons_weak : @A:*s.@a,b:A.@l:List A. Perm (a;b;l) (b;a;l)

-- Two lemmas about insert --
Prove lemma_insert_m_n_is_insert_n_m : @m,n:Nat. m<n -> 
               (@l:List Nat. insert m (insert n l) = insert n (insert m l))

Prove insert_m_n_is_insert_n_m : @m,n:Nat. @l:List Nat. 
                                 insert m (insert n l) = insert n (insert m l)

-- Lemma about concat
Prove concat_is_nil_ : @A:*s. @as,bs:List A. as ++ bs = nil A -> 
                       as = nil A /\ bs = nil A

-- Three lemmas about Elem
Prove Elem_cons : @A:*s. @l:List A. @a,b:A.
                       Elem a (b;l) <=> a=b  \/ Elem a l

Prove Elem_concat : @A:*s. @l,l':List A. @a:A.
                       Elem a (l++l') <=> Elem a l \/ Elem a l'

prove Perm__Elem_eq : @A:*s. @l,l':List A. Perm l l' -> @a:A.
                       Elem a l -> Elem a l'


---------------------------------------------------------------------
---------------------------------------------------------------------
--                                                                 --
--  2.  N E W   F U N C T I O N S   W I T H   P R O P E R T I E S  --
--                                                                 --
---------------------------------------------------------------------
---------------------------------------------------------------------


----------
-- elem --
----------

Def elem := \m:Nat. iterlist false (\hd:Nat. \elem_tail:Bool. 
                                    eq m hd || elem_tail) :
            Nat -> List Nat -> Bool

Prove elem_m_nil : @m:Nat. elem m (nil Nat) = false

Prove elem_m_cons : @m,n:Nat.@ns:List Nat. elem m (n;ns) = eq m n || elem m ns

----------
-- null --
----------


Def null := \A:*s. iterlist true (\hd:A. \null_tail:Bool. false) :
            @A:*s. List A -> Bool
Implicit 1 null

Prove null_nil : @A:*s. null (nil A) = true

Prove null_cons : @A:*s. @a:A. @as:List A. null (a;as) = false


----------------------
-- genCount & count --
----------------------

Def genCount := \A:*s.\p:A->Bool.\l:List A. iterlist O (\hd:A. \countTail:Nat. 
                                        if (p hd) (S countTail) countTail) l :
                @A:*s. (A->Bool) -> List A -> Nat
Implicit 1 genCount

Prove genCount_nil : @A:*s.@p:A->Bool. genCount p (nil A) = O

Prove genCount_cons : @A:*s.@p:A->Bool. @a:A. @l:List A. 
                  genCount p (a;l) = if (p a) (S (genCount p l)) (genCount p l)



Def count := \m:Nat. genCount (eq m) : Nat -> List Nat -> Nat

Prove count_nil : @m:Nat. count m (nil Nat) = O

Prove count_cons : @m,n:Nat. @l:List Nat. 
                   count m (n;l) = if (eq m n) (S (count m l)) (count m l)


Prove eq__count_cons : @m,n:Nat. @l:List Nat. eq m n = true ->
                                              count m (n;l) = S (count m l)

Prove neq__count_cons : @m,n:Nat. @l:List Nat. eq m n = false ->
                                              count m (n;l) = count m l

Prove count_m_m_cons : @m:Nat.@l:List Nat. count m (m;l) = S (count m l)

Prove count_m_n_cons : @m,n:Nat.@l:List Nat. Not (m=n) -> 
                          count m (n;l) = count m l


Prove count_m_insert_m : @m:Nat.@l:List Nat. 
                         count m (insert m l) = S (count m l)

Prove count_m_insert_n : @m,n:Nat.@l:List Nat. Not (m=n) -> 
                         count m (insert n l) = count m l

Prove genCount_concat : @A:*s.@p:A->Bool.@l1,l2:List A.
                        genCount p (l1++l2) = genCount p l1 + genCount p l2

Prove Perm__genCount_equal : @A:*s.@p:A->Bool. @l1,l2:List A.
                             Perm l1 l2 -> genCount p l1 = genCount p l2

Prove Perm__count_equal : @m:Nat.@l1,l2:List Nat. Perm l1 l2 ->
                                                  count m l1 = count m l2

Prove SO_Le_count__Elem : @l:List Nat. @m:Nat. S O <= count m l -> Elem m l


----------
-- snoc --
----------

Def snoc := \A:*s. \a:A. \l:List A. l ++ singleton a :
            @A:*s. A -> List A -> List A
Implicit 1 snoc

Prove Perm_cons_snoc : @A:*s.@a:A.@l:List A. Perm (a;l) (snoc a l)


------------
-- length --
------------

Def length := \A:*s. iterlist O (\hd:A.S) :
              @A:*s. List A -> Nat
implicit 1 length

Prove length_nil : @A:*s. length (nil A) = O

Prove length_cons : @A:*s.@a:A.@l:List A. length (a;l) = S (length l)

Prove length_insert : @m:Nat. @l:List Nat. length (insert m l) = S (length l)


----------
-- init --
----------

-- init [] = []
-- init [x:xs] = if null xs then [] else x : init xs
Def init := \A:*s. primreclist (nil A) (\hd:A.\tl:List A.\init_tail:List A.
                                        if (null tl) (nil A) (hd;init_tail)) :
            @A:*s. List A -> List A
implicit 1 init

Prove init_nil : @A:*s. init (nil A) = nil A

Prove init_singleton : @A:*s.@a:A. init (a;nil A) = nil A

Prove init_cons2 : @A:*s.@a,b:A. @as:List A. init (a;b;as) = a; init (b;as)

Prove Not_nil__init_cons : @A:*s.@a:A. @as:List A. Not (as=nil A) -> 
                           init (a;as) = a; init as

Prove init_concat : @A:*s.@as,bs:List A. Not (bs = nil A) ->
                    init (as++bs) = as ++ init bs

----------
-- last --
----------

-- last d nil = d
-- last d (a;as) = last a as

Def last := \A:*s.\Def:A.\l:List A. 
   iterlist (\Def:A.Def) (\hd:A. \last_tail:A->A. \dummy:A. last_tail hd) l Def
implicit 1 last

Prove last_nil : @A:*s. @a:A. last a (nil A) = a

Prove last_cons : @A:*s. @a,b:A. @as:List A. last a (b;as) = last b as

Prove Not_nil__last : @A:*s.@a1,a2:A.@as:List A. Not (as = nil A) -> 
                      last a1 as = last a2 as

Prove Not_nil__last_cons : @A:*s.@a,b:A.@as:List A. Not (as = nil A) -> 
                           last a (b;as) = last a as

Prove last_concat : @A:*s.@a:A.@as,bs:List A. Not (bs = nil A) -> 
                    last a (as++bs) = last a bs

Prove Elem_last : @A:*s.@l:List A.@a:A. Not (l = nil A) -> Elem (last a l) l

Prove Elem_Le_last : @l:List Nat. @m:Nat. Elem m l -> 
                     @n:Nat. Ordered l -> m <= last n l


-------------
-- reverse --
-------------

Def reverse := \A:*s. iterlist (nil A) (snoc A)
Implicit 1 reverse

Prove reverse_nil : @A:*s. reverse (nil A) = nil A

Prove reverse_cons : @A:*s. @a:A. @as:List A.
                             reverse (a;as) = snoc a (reverse as)

Prove reverse_tail : @A:*s. @as:List A.
                              reverse (tail as) = init (reverse as)

Prove last_reverse : @A:*s.@a:A.@as:List A.
                            last a (reverse as) = head a as