Sorting in Twelf

sorting.elf

int: type.
z: int.
s: int -> int.

<: int -> int -> type.
%infix right 1 <.
less/0: X < s X.
less/1: X < s Y
    <- X < Y.

==: int -> int -> type.
%infix right 1 ==.
equal/0: X == X.

<=: int -> int -> type.
%infix right 1 <=.
less_equal/0: X <= Y
    <- X < Y.
less_equal/1: X <= Y
    <- X == Y.

!=: int -> int -> type.
%infix right 1 !=.
not_equal/0: X != Y
    <- X < Y.
not_equal/1: X != Y
    <- Y < X.

0 = z.
1 = s 0.
2 = s 1.
3 = s 2.
4 = s 3.
5 = s 4.
6 = s 5.
7 = s 6.
8 = s 7.
9 = s 8.
10 = s 9.


list: type.
*: list.
;: int -> list -> list.
%infix right 1 ;.

find_lowest: list -> int -> type.
find_lowest/0: find_lowest (X ; *) X.
find_lowest/1: find_lowest (X ; Xs) Y
    <- find_lowest Xs Y
    <- Y < X.
find_lowest/2: find_lowest (X ; Xs) X
    <- find_lowest Xs Y
    <- X < Y.
find_lowest/3: find_lowest (X ; Xs) X
    <- find_lowest Xs Y
    <- X == Y.

delete_item: list -> int -> list -> type.
delete_item/0: delete_item * X *.
delete_item/1: delete_item (X ; Xs) Y (X ; As)
    <- X != Y
    <- delete_item Xs Y As.
delete_item/2: delete_item (X ; Xs) Y Xs
    <- X == Y.

sort: list -> list -> type.
sort/0: sort * *.
sort/1: sort Xs (X ; Ys)
    <- find_lowest Xs X
    <- delete_item Xs X X1s
    <- sort X1s Ys.

The worst case scenario in this sorting algorithm is an already sorted list.