(SWI-PL) I can't figure out how to create a prolog rule to match this particular type of input

So I've a homework assignment where I given the following code:

numeral(0).
numeral(succ(X)) :- numeral(X).
numeral(X+Y) :- numeral(X), numeral(Y).

add(0,X,X).
add(succ(X),Y,succ(Z)) :- add(X,Y,Z).

And I am to define a prolog predicate add2(X,Y,Z) which will produce, for example, the following outputs

% Exercise 1 Test Cases (for copy-paste to the REPL
%% 1. add2(succ(0)+succ(succ(0)), succ(succ(0)), Z).
%%    >>>> Z = succ(succ(succ(succ(succ(0)))))
%%
%% 2. add2(0, succ(0)+succ(succ(0)), Z).
%%    >>>> Z = succ(succ(succ(0)))
%%
%% 3. add2(succ(succ(0)), succ(0)+succ(succ(0)), Z).
%%    >>>> Z = succ(succ(succ(succ(succ(0)))).
%%
%% 4. add2(succ(0)+succ(0), succ(0+succ(succ(0))), Z).
%%    >>>> Z = succ(succ(succ(succ(succ(0))))).

So I've been working on this for the last few days, and have made a reasonable attempt at the solution. Here's what I have been trying so far:

% Exercise 1 Solution
add2(X,Y,Z):- add(X,Y,Z).
add2(A+B,Y,Z):- add2(A,B,X), add2(X,Y,Z).
add2(X,A+B,Z):- add2(A,B,Y), add2(X,Y,Z).

Now, this above code works quite nicely for the first 3 inputs provided. I am having difficulty trying to think about how prolog might interpret the last, and how I can take advantage of it.

Here's what I was thinking might work.

add2(X, succ(A+B), Z):- add2(A,B,Y), add2(X, succ(Y), Z).

What was I thinking was that, the interpreter would recognise an input such as succ(0+succ(...)) to be succ(A+B), and then the above rules would be able to resolve 0+succ(...) into succ(...) . The output I receive from the SWI-PL REPL is simply:

Z = succ(succ(succ(0+succ(succ(0)))))

Another attempt I made was the following:

add2(X,succ(0+succ(Y), Z)):- add2(X,succ(Y),Z).

However, this yields the same output as before. I am unsure why the above two attempts do not seem to work for me, and while I have made other guesses, there were more or less random variations of the above two or of the other predicates and if I had succeeded by that approach I would likely have achieved the right answer without understanding what I was doing.

I am using SWI-PL as my prolog distribution.

Solution

I think it might help to solve the problem by using a helper predicate here. The helper function will convert a number represented with a cascade of succ(…) and … + … into a uniform style (so only succ(…)).

We thus can implement such function as:

normsucc(0, 0).
normsucc(succ(X), succ(NX)) :-
    normsucc(X, NX).
normsucc(X+Y, NXY) :-
    normsucc(X, NX),
    normsucc(Y, NY),
    add(NX, NY, NXY).

So then we can make use of normsucc to calculate the sum:

add2(X, Y, Z) :-
    normsucc(X, NX),
    normsucc(Y, NY),
    add(NX, NY, Z).

or simpler, like @false suggests:

add2(X, Y, Z) :-
    normsucc(X+Y, Z).