-- File: sort

-- This file contains the example of sorting of records, as in Section 8.4.

Path "../lol"
Path "../lolplus"
Load "lambdaLsubplus"
Load "sort"  -- so we have Perm

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

Def OrderedId := \B<:{|id:Nat|}.
                 \l:List B. 
                 @P:List B -> *p.
                 P (nil B) ->
                 (@a:B.@m:List B. P m -> (@b:B. Elem b m -> a`id<=b`id) -> 
                                  P (a;m)) ->
                 P l :
                 @B<:{|id:Nat|}. List B -> *p

Implicit 1 OrderedId

Prove OrderedId_nil : @B<:{|id:Nat|}. OrderedId (nil B)

Prove OrderedId_cons : @B<:{|id:Nat|}.@a:B.@m:List B. OrderedId m -> 
                                        (@b:B. Elem b m -> a`id<=b`id) -> 
                                        OrderedId (a;m)

Prove OrderedId_singleton : @B<:{|id:Nat|}. @m:B. OrderedId (singleton m)

Prove OrderedId_exh : @B<:{|id:Nat|}. @l:List B. OrderedId l -> 
                       l = nil B \/
                       Ex a:B. Ex m:List B. l = a;m /\
                                              (@b:B. Elem b m -> a`id<=b`id) /\
                                              OrderedId m

Prove OrderedId_cons_ : @B<:{|id:Nat|}. @a:B.@m:List B. OrderedId (a;m) -> 
                                          (@b:B. Elem b m -> a`id<=b`id) /\
                                          OrderedId m


-----------------------
-- FUNCTION insertId --
-----------------------

Def insertId := \B<:{|id:Nat|}. \n:B. primreclist (singleton n) (
                      \head:B. \tail:List B. \insert_tail:List B. 
                         if (leq n`id head`id) 
                            (n;head;tail)
                            (head;insert_tail)) : 
              @B<:{|id:Nat|}. B -> List B -> List B
implicit 1 insertId

Prove insertId_nil : @B<:{|id:Nat|}. @m:B. insertId m (nil B) = singleton m

Prove Le__insertId : @B<:{|id:Nat|}. @m,n:B.@l:List B. m`id<=n`id -> 
                                     insertId m (n;l) = m;n;l

Prove Gt__insertId : @B<:{|id:Nat|}. @m,n:B.@l:List B. n`id<m`id -> 
                                     insertId m (n;l) = n;(insertId m l)

Prove Elem_insertId_ : @B<:{|id:Nat|}. @m,n:B.@ns:List B.
                                           Elem m (insertId n ns) -> 
                                           m=n \/ Elem m ns

Prove OrderedId_insertId  : @B<:{|id:Nat|}. @m:B. @l:List B. OrderedId l ->
                                             OrderedId (insertId m l)

Prove Perm_insertId : @B<:{|id:Nat|}. @m:B. @l:List B.
                               Perm (insertId m l) (m;l)

------------
-- sortId --
------------

Def sortId := \B<:{|id:Nat|}.
              primreclist (nil B) (\head:B. \tail:List B. 
                             \sort_tail:List B. insertId head sort_tail) :
            @B<:{|id:Nat|}. List B -> List B
Implicit 1 sortId

Prove sortId_nil : @B<:{|id:Nat|}. sortId (nil B) = nil B

Prove sortId_cons : @B<:{|id:Nat|}. @m:B.@l:List B. sortId (m;l) = insertId m (sortId l)

Prove OrderedId_sortId : @B<:{|id:Nat|}. @l:List B. OrderedId (sortId l)

Prove Perm_sortId : @B<:{|id:Nat|}. @l:List B. Perm (sortId l) l