Prolog function count and member by using natural numbers and it succesor

Question

I need to program in Prolog a function that count the number of elements in a list an other that verify if an element is in the list but by using natural numbers "zero" and his succesor (s(zero)).

For example, i managed to program the analogues "take" and "drop" by using the previous restriction:

natural(zero). %we consider "zero" as a natural number
natural(s(X)) :- natural(X). %if X is a natural number, then s(X) is a natural number too


take(zero,_,[]).
take(s(_),[],[]).
take(s(N),[X|Xs],[X|Ys]) :- take(N,Xs,Ys).


drop(zero,Xs,Xs).
drop(s(_),[],[]).
drop(s(N),[_|Ys],Zs):-drop(N,Ys,Zs).

But i can't program the analogues "count" and "member" in Prolog using natural numbers, i only managed to program this functions in the usual way:

isList([]).
isList([_|Xs]) :- isList(Xs).

isInList(X, [X|_]).
isInList(X,[_|Xs]) :- isInList(X,Xs).

countElem([],0).
countElem([X|L],N) :- countElem(L,N2), N is N2 + 1.

I don't have too much experience in Prolog. Any help would be appreciated.

Answer 1

Example: count using peano. This avoids slow non-tail-end recursion:

length_peano(Lst, Len) :-
    % Start at zero
    length_peano_(Lst, zero, Len).

length_peano_([], Len, Len).
length_peano_([_|T], Upto, Len) :-
    % Increment
    Upto1 = s(Upto),
    length_peano_(T, Upto1, Len).

Alternatively, the more elegant (credit to slago):

length_peano([], zero).
length_peano([_|T], s(N)) :-
    length_peano(T, N).

Results in swi-prolog for both:

?- length_peano([a,b,c], Len).
Len = s(s(s(zero))).

?- length_peano(Lst, Len).
Lst = [],
Len = zero ;
Lst = [_],
Len = s(zero) ;
Lst = [_,_],
Len = s(s(zero)) ;
Lst = [_,_,_],
Len = s(s(s(zero))) ;
Lst = [_,_,_,_],
Len = s(s(s(s(zero)))) ;