Should I write the definition again for using rewrite in Agda?

Question

Exercise *-assoc (recommended) {#times-assoc}

Show multiplication is associative, that is,

(m * n) * p ≡ m * (n * p)

for all naturals m, n, and p.

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl

*-assoc (suc m) n p = 
  begin
    ((suc m) * n) * p 
  ≡⟨ cong (_* p) (suc-*-comm m n) ⟩
    (n + (m * n)) * p
  ≡⟨ (*-distrib-+ n (m * n) p) ⟩
    n * p + (m * n) * p
  ≡⟨ cong ((n * p) +_) (*-assoc m n p) ⟩
    n * p + m * (n * p)
  ≡⟨⟩
    (suc m) * (n * p)
  ∎
  where 
  suc-*-comm : ∀ (m n : ℕ) → (suc m) * n ≡ n + m * n
  suc-*-comm m n = refl

I need to rewrite the definition of multiplication here. It is annoying.

I have tried to add the definition of multiplication in the where. How to avoid it?

Answer 1

I'm not sure I really understand what you are asking, nor why this might be "annoying" (not really a technical matter, unless you think the definition of multiplication to be somehow incorrect. or for there to be a 'better' definition?), but it may help you to know that, for your definition of suc-*-comm m n = refl in the where block, the first step in the main proof,

    ((suc m) * n) * p 
  ≡⟨ cong (_* p) (suc-*-comm m n) ⟩
    (n + (m * n)) * p

reduces to

    ((suc m) * n) * p 
  ≡⟨ cong (_* p) refl ⟩
    (n + (m * n)) * p

and hence to

    ((suc m) * n) * p 
  ≡⟨ refl ⟩
    (n + (m * n)) * p

and hence, analogously to the final step, finally to

    ((suc m) * n) * p 
  ≡⟨⟩
    (n + (m * n)) * p

As a consequence of which, you will no longer need the where block...

*-assoc (suc m) n p = 
  begin-equality
    ((suc m) * n) * p 
  ≡⟨⟩
    (n + (m * n)) * p
  ≡⟨ ... ⟩
    n * p + (m * n) * p
  ≡⟨ cong ((n * p) +_) (*-assoc m n p) ⟩
    n * p + m * (n * p)
  ≡⟨⟩
    (suc m) * (n * p)
  ∎

(the ... here is because using stdlib-v2.0, a different proof of distributivity is required in that step)