-- File: sort

-- This file contains the example of sorting, as in Section 4.7

Load "nat"
Load "list"

-----------------------
-- PREDICATE Ordered --
-----------------------

-- Ordered is the smallest predicate with
--  * Ordered nil
--  * Ordered l -> (@b:Nat. Elem b l -> a<=b) -> Ordered (a;l)
-- This is a nice definition, since there are only two clauses, that follow
-- the structure of lists.

Def Ordered := \l:List Nat. 
               @P:List Nat -> *p.
               P (nil Nat) ->
               (@a:Nat.@m:List Nat. P m -> (@b:Nat. Elem b m -> a<=b) -> 
                                    P (a;m)) ->
               P l :
               List Nat -> *p

Prove Ordered_nil : Ordered (nil Nat)

Prove Ordered_cons : @a:Nat.@m:List Nat. Ordered m -> 
                                        (@b:Nat. Elem b m -> a<=b) -> 
                                        Ordered (a;m)

Prove Ordered_singleton : @m:Nat. Ordered (singleton m)

Prove Ordered_exh : @l:List Nat. Ordered l -> 
                     l = nil Nat \/
                     Ex a:Nat. Ex m:List Nat. l = a;m /\
                                              (@b:Nat. Elem b m -> a<=b) /\
                                              Ordered m

Prove Ordered_cons_ : @a:Nat.@m:List Nat. Ordered (a;m) -> 
                                          (@b:Nat. Elem b m -> a<=b) /\
                                          Ordered m


----------
-- Perm --
----------

Def Perm := \A:*s. \as,bs: List A.
                  @P : List A -> List A -> *p.
                  (@xs:List A. P xs xs) ->
                  (@xs,ys,zs:List A. P xs ys -> P ys zs -> P xs zs) ->
                  (@xs,ys:List A.@x,y:A. P (xs++(x;y;ys)) (xs++(y;x;ys))) ->
                  P as bs :
            @A:*s. List A -> List A -> *p
Implicit 1 Perm

-- An alternative definition of Perm is with clauses
-- - @xs:List A. Perm xs xs
-- - @xs,ys,zs:List A. Perm xs ys -> Perm ys zs -> Perm xs zs
-- - @xs:List A. @x,y:A. Perm (x;y;bs) (y;x;bs)
-- - @xs,ys:List A. @x:A. Perm xs ys -> Perm (x;xs) (Perm x;ys)
-- Advantage: no concatenation necessary.
-- Disadvantage: less intuitive.

Prove Perm_refl : @A:*s. @xs:List A. Perm xs xs

Prove Perm_trans : @A:*s. @xs,ys,zs:List A. Perm xs ys -> Perm ys zs -> 
                                            Perm xs zs

Prove Perm_swap : @A:*s. @xs,ys:List A.@x,y:A. 
                                     Perm (xs++(x;y;ys)) (xs++(y;x;ys))
                                                                 
Prove Perm_cons : @A:*s. @a:A. @l,m:List A. Perm l m -> Perm (a;l) (a;m)

Prove Perm_sym : @A:*s. @xs,ys:List A. Perm xs ys -> Perm ys xs


---------------------
-- FUNCTION insert --
---------------------

Def insert := \n:Nat. primreclist (singleton n) (
                      \head:Nat. \tail:List Nat. \insert_tail:List Nat. 
                         if (leq n head) (n;head;tail) (head;insert_tail)) : 
              Nat -> List Nat -> List Nat

Prove insert_nil : @m:Nat. insert m (nil Nat) = singleton m

Prove Le__insert : @m,n:Nat.@l:List Nat. m<=n -> insert m (n;l) = m;n;l

Prove Gt__insert : @m,n:Nat.@l:List Nat. n<m -> insert m (n;l) = n;(insert m l)

Prove Elem_insert_ : @m,n:Nat.@ns:List Nat. Elem m (insert n ns) -> 
                                            m=n \/ Elem m ns

Prove Ordered_insert  : @m:Nat. @l:List Nat. Ordered l ->
                                             Ordered (insert m l)

Prove Perm_insert : @m:Nat. @l:List Nat. Perm (insert m l) (m;l)

----------
-- sort --
----------

-- sort [] = sort
-- sort (x:xs) = insert x (sort xs)

Def sort := primreclist (nil Nat) (\head:Nat. \tail:List Nat. 
                                \sort_tail:List Nat. insert head sort_tail) :
            List Nat -> List Nat
-- bdRed sort (S O ; O ; nil Nat)
-- 255 reductions!

Prove sort_nil : sort (nil Nat) = nil Nat

Prove sort_cons : @m:Nat.@l:List Nat. sort (m;l) = insert m (sort l)

Prove Ordered_sort : @l:List Nat. Ordered (sort l)

Prove Perm_sort : @l:List Nat. Perm (sort l) l