Question about add_succ

Stream: new members

[Kaixin Wang]

image.png
Why is there an error if I execute add_succ succ(succ 0) succ(succ 0) at h but no error if I do add_succ at h

[Mitchell Lee]

add_succ m n proves m + succ n = succ (m + n).

So add_succ (succ (succ 0)) (succ (succ 0)) proves that succ (succ 0) + succ (succ (succ 0)) = succ (succ (succ 0) + succ (succ 0)).

Since succ (succ 0) + succ (succ (succ 0)) doesn't appear anywhere in the goal, the rewriting fails.

[Mitchell Lee]

You might have more success with rw [add_succ (succ (succ 0)) (succ 0)] at h.

[Mitchell Lee]

Also, it is always necessary to put a space between a function and its arguments, so you should write succ (succ 0) instead of succ(succ 0).

[Kaixin Wang]

Thanks for your help!
I have a related question

[Kaixin Wang]

image.png

[Kaixin Wang]

add_zero a proves a + 0 = a

[Kaixin Wang]

when I tried rw[add_zero a * 0]
there is this error:

[Kaixin Wang]

image.png

[Kaixin Wang]

Oh I see, this works!
image.png

[Kaixin Wang]

What is wrong with this:
image.png

[Johan Commelin]

one_mul is for 1 * x = x. But your goal is x = 1 * x

[Johan Commelin]

So you need to take care of the LHS/RHS symmetry.

[Kaixin Wang]

exact <- one_mul x and exact (<- one_mul x) doesn't work either

[Johan Commelin]

@Kaixin Wang hint: try rw instead of exact

[Kaixin Wang]

Yes rw works, I was just wondering if exact works as well.

I think everything that is doable with exact should be doable with rw.

[Kevin Buzzard]

exact (one_mul x).symm would probably work.