```-- File: sort

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

-----------------------
-- 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)

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) (
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
```