Agda rewrite does not change goal in _*_ commutativity proof

Question

SOLVED: I have a solution after following white-wolf's advice. If you are interested in my solution feel free to message me.

I am trying to write a proof in Agda for commutativity for multiplication:

lem3 : (x y : ℕ) → (x * y) ≡ (y * x)
lem3 0 y rewrite pr3a y = refl
lem3 (suc x) y rewrite lem3 x y | pr3b x y = refl

where we have:

pr3a : (x : ℕ) → (x * 0) ≡ 0
pr3a 0 = refl
pr3a (suc x) with (x * 0) | pr3a x
... | .0 | refl = refl

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y = {!!}

I am having trouble filing this final goal. The expected type is y + y * suc x ≡ y * suc (suc x), and I had expected that using rewrite would give me y * suc (suc x) ≡ y * suc (suc x) as a goal. However:

pr3b (suc x) y rewrite pr3b x y = {!!}

expects the same goal as before: y + y * suc x ≡ y * suc (suc x).

It is my understanding that rewrite would effectively substitute the RHS into the LHS for x = x, giving y * suc x ≡ y * suc x, and then use x = suc x to give y * suc (suc x) ≡ y * suc (suc x). Am I mis-understanding how rewrite works or have I made some other error?

white_wolf white_wolf · Accepted Answer · 2018-08-06T17:37:58

Your goal is y + y * suc x ≡ y * suc (suc x). Your induction hypothesis is y + y * x ≡ y * suc x. I can check that by putting pr3b x y inside the goal and typing C-c C-.

Goal: y + y * suc x ≡ y * suc (suc x)
Have: y + y * x ≡ y * suc x

This means that with a rewrite you should be able to replace y * suc x with y * x. However, you see that the two sides are switched, so you have to rewrite with symmetry like so

pr3b : (x y : ℕ) →  y + y * x ≡ y * suc x
pr3b 0 0 = refl
pr3b 0 (suc y) rewrite pr3b 0 y = refl
pr3b (suc x) y rewrite sym $ pr3b x y = {!!}

This promotes the goal to y + (y + y * x) ≡ y * suc (suc x). This particular proof requires associativity and commutativity of addition to be completed.

Edit

I think you should try to prove this by induction on y instead of x.

Agda rewrite does not change goal in _*_ commutativity proof

1 Answers