Trees in twelf

tree.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.


t_node: type.
?: t_node.
node: t_node -> int -> t_node -> t_node.

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

concat: list -> list -> list -> type.
concat/0: concat * Xs Xs.
concat/1: concat (X ; Xs) Ys (X ; Zs)
    <- concat Xs Ys Zs.

depth: t_node -> list -> type.
depth/0: depth ? *.
depth/1: depth (node L V R) Y
    <- depth L Y1
    <- depth R Y2
    <- concat Y1 (V ; Y2) Y.

add_node: t_node -> t_node -> t_node -> type.
add_node/0: add_node X ? X.
add_node/1: add_node ? X X.
add_node/2: add_node (node XL XV XR) (node YL YV YR) (node Z YV YR)
    <- XV < YV
    <- add_node (node XL XV XR) YL Z.
add_node/3: add_node (node XL XV XR) (node YL YV YR) (node YL YV Z)
    <- YV < XV
    <- add_node (node XL XV XR) YR Z.

list_to_tree: list -> t_node -> type.
list_to_tree/0: list_to_tree * ?.
list_to_tree/1: list_to_tree (X ; Xs) Y
    <- list_to_tree Xs Y1
    <- add_node Y1 (node ? X ?) Y.

There's a bit of a bug with add_node ? ? X. which gives 2 solutions that are both X = ? (I would like for it to only give me 1 solution).