Trying to write a tree-height predicate - do I need Peano-style natural numbers?

As a basic Prolog exercise, I set myself the task of writing a binary tree height predicate that would work forwards and "backwards" - that is, as well as determining the height of a known binary tree, it should be able to find all binary trees (including unbalanced ones) of a known height. This is the best solution I've come up with so far...

tree_eq1([],s).  % Previously had a cut here - removed (see comments for reason)
tree_eq1([_|T],n(L,R)) :- tree_eq1(T,L), tree_eq1(T,R).
tree_eq1([_|T],n(L,R)) :- tree_eq1(T,L), tree_lt1(T,R).
tree_eq1([_|T],n(L,R)) :- tree_lt1(T,L), tree_eq1(T,R).

tree_lt1([_|_],s).
tree_lt1([_,X|T],n(L,R)) :- XX=[X|T], tree_lt1(XX,L), tree_lt1(XX,R).

The first argument is the height, expressed as a list - the elements are irrelevant, the length of the list expresses the height of the tree. So I'm basically abusing lists as Peano-style natural numbers. The reasons this is convenient are...

No concerns about negative numbers.
I can check for > or >= without knowing the exact number - for example, by matching two items on the head of the list, I ensure the list length is >=2 without caring about the length of the tail.

Neither of these properties seem to apply to Prolog numbers, and I can't think of a way so far to adapt the same basic approach to use actual numbers in place of these lists.

I've seen a few examples in Prolog using Peano-style numbers, so my question is - is this normal practice? Or is there some way to avoid the issue that I haven't spotted yet?

Also, is there a way to convert to/from a Peano-style representation that won't break the bidirectionality? The following don't work for fairly obvious reasons...

length(L,N), tree_eq1(L,X).
  % infinite set of lists to explore if N is unknown

tree_eq1(L,X), length(L,N)
  % infinite set of trees to explore if X is unknown

The best I can think of so far is an is-this-variable-instantiated test to choose between implementations, which seems like cheating to me.

BTW - I have some ideas for other methods which I don't want spoilers for - particularly a kind of dynamic programming approach. I'm really focused on fully understanding the lessons from this particular attempt.

Solution

First: +1 for using lists lengths for counting, which sometimes really is quite convenient and a nice alternative for successor notation.

Second: For reversible arithmetic, you typically use constraints instead of successor notation, because constraints allow you to work with actual numbers and come with built-in definitions of the usual mathematical relations among numbers.

For example, with SICStus Prolog or SWI:

:- use_module(library(clpfd)).

tree_height(s, 0).
tree_height(n(Left,Right), Height) :-
        Height #>= 0,
        Height #= max(HLeft,HRight) + 1,
        tree_height(Left, HLeft),
        tree_height(Right, HRight).

Example query:

?- tree_height(Tree, 2).
Tree = n(s, n(s, s)) ;
Tree = n(n(s, s), s) ;
Tree = n(n(s, s), n(s, s)) ;
false.

Third, notice that the most general query, ?- tree_eq1(X, Y)., does not work satisfactorily with your version. With the snippet above, at least it gives an infinite number of solutions (as it should):

?- tree_height(T, H).
T = s,
H = 0 ;
T = n(s, s),
H = 1 ;
T = n(s, n(s, s)),
H = 2 .

I leave their fair enumeration as an exercise.