Prove 2+2=2*2 (and similar)

Question

Output a full formal poof of such statements such as 1+2=3, 2+2=2*(1+1) etc.

Introuction

If you know Peano Arithmetic you can probably skip this section.

Here's how we define the Natural Numbers:

(Axiom 1) 0 is a number
(Axiom 2) If `x` is a number, the `S(x)`, the successor of `x`, is a number.

Hence, for example S(S(S(0))) is a number.

You can use any equivalent representation in your code. For example, all of these are valid:

0    ""    0           ()       !
1    "#"   S(0)        (())     !'
2    "##"  S(S(0))     ((()))   !''
3    "###" S(S(S(0)))  (((()))) !'''
...
etc

We can extend the rules to define addition as follows.

(Rule 1) X+0 = X
(Rule 2) X+S(Y)=S(X)+Y

With this we can prove 2+2=4 as follows

         S(S(0)) + S(S(0)) = 2 + 2
[Rule 2 with X=S(S(0)), Y=S(0)]
         S(S(S(0))) + S(0) = 3 + 1
[Rule 2 with X=S(S(S(0))), Y=0]
         S(S(S(S(0)))) + 0 = 4 + 0
[Rule 1 with X=S(S(S(S(0))))
         S(S(S(S(0))))     = 4

We can extend these rules to define multiplication as follows

(Rule 3) X*0 = 0
(Rule 4) X*S(Y) = (X*Y) + X

Although to allow this we need to define the structural role of parentheses.

(Axiom 3) If X is a number, (X) is the same number.

Addition and multiplication operators are strictly binary and parentheses must always be explicit. A+B+C is not well-defined, but (A+B)+C and A+(B+C) are.

Example

Now we have enough to prove a theorem about multiplication: 2+2=2*2

2 + 2
(2) + 2
(0 + 2) + 2
((0*2) + 2) + 2
(1*2) + 2
2*2

Requirements

A proof that A=B is a list expressions such that:

• the first is A,
• the last is B, and
• each expression in the list apart from the first can obtained from the previous by transforming it under one of the rules.

Your program will take two valid expressions as input, each expression contains numbers, addition, multiplication, and parentheses as defined above.

Your program will output a proof, a list as defined above, that the two expressions are equal, if such a proof exists.

If the two expressions are not equal, your program will output nothing.

Proving or disproving is always possible in a finite number of steps, because each expression can be reduced to a single number and these numbers can be trivially tested for equality.

If the input expressions are not valid (e.g. unbalanced parentheses, contains non-numbers, or non-binary operators) then your program should exit with error, throw an exception, print an error, or otherwise produce some observable behaviour which is distinct from the case in which the inputs are valid but non-equal.

In summary, the normal output for admissible inputs is a list of equal numbers, including the inputs, which is produced by the following rules.

(Axiom 1) 0 is a number
(Axiom 2) If `x` is a number, the `S(x)`, the successor of `x`, is a number.
(Axiom 3) If X is a number, (X) is the same number

(Rule 1) X+0 = X
(Rule 2) X+S(Y)=S(X)+Y
(Rule 3) X*0 = 0
(Rule 4) X*S(Y) = (X*Y) + X
(Rule 5) X = (X)              (Axiom 3 expressed as a transformation rule.)

Any suitable representation of the numbers in the input and output is allowed, e.g. 0=""=(), 3="###"=(((()))), etc. Whitespace is irrelevant.

Rules can, of course, be applied in either direction. Your program does not have to output which rule is used, just the expression produced by its action on the previous expression.

Shortest code wins.

Answer 1

Perl, 166 + 1 bytes

Run with -p (1 byte penalty).

$r='\((S*)';(@b,@a)=@a;push@a,$_ while+s/\+S/S+/||s/$r\+\)/$1/||s/$r\*\)//||s/$r\*S(S*)/(($1*$2)+$1/||s/$r\)/$1/;$\.=/[^S]./s;$_=$b[-1]eq$a[-1]?join'',@b,reverse@a:""

More readable:

                           # implicit: read a line of input into $_
                           # we leave the newline on
$r = '\((S*)';             # we use this regex fragment a lot, factor it out
(@b, @a) = @a;             # set @b to @a, @a to empty
push @a, $_ while          # each time round the loop, append $_ to @a
+s/\+S/S+/||               # rule 2: change "+S" to "S+"
s/$r\+\)/$1/||             # rule 1: change "(X+0)" to "X"
s/$r\*\)//||               # rule 3: change "(X*0)" to ""
s/$r\*S(S*)/(($1*$2)+$1/|| # rule 4: change "(X*Y" to "((X*Y)+X"
s/$r\)/$1/;                # rule 5: change "(X) to "X"
$\.=/[^S]./s;              # append a 1 to the newline character if we
                           # see any non-S followed by anything
$_=$b[-1]eq$a[-1]?         # if @b and @a end the same way
  join'',@b,reverse@a      # then $_ becomes @b followed by (@a backwards)
  :""                      # otherwise empty $_
                           # implicit: output $_

The input format expresses numbers in unary as strings of S, and requires the two inputs on separate lines (each followed by a newline, and an EOF after both are seen). I interpreted the question as requiring that parentheses should be literally ( ) and addition/multiplication should be literally + *; I can save a few bytes through less escaping if I'm allowed to make different choices.

The algorithm actually compares the first line of input with an empty line, the second with the first, the third with the second, and so on. This fulfils the requirements of the question. Here's an example run:

My input:

(SS+SS)
(SS*SS)

Program output:

(SSS+S)
(SSSS+)
SSSS
SSSS
(SSSS+)
((SS+)SS+)
(((SS*)SS+)SS+)
(((SS*)S+S)SS+)
(((SS*)+SS)SS+)
((SS*S)SS+)
((SS*S)S+S)
((SS*S)+SS)

The duplicated SSSS in the middle is annoying but I decided it didn't violate the specification, and it's fewer bytes to leave it in.

On invalid input, I append 1 to the newline character, so you get stray 1s sprinkled in at the end of the output.