在 Agda 中使用 rewrite 需要重新编写定义吗？

Question

锻炼

*-assoc

（推荐）{#times-assoc}

显示乘法是结合律的，即

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

适合所有天然

m

、

n

和

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

我需要在这里重写乘法的定义。真烦人。

我尝试在where中添加乘法的定义。如何避免？

Answer 1

我不确定我是否真的理解你在问什么，也不确定为什么这可能是“烦人的”（不是真正的技术问题，除非你认为乘法的定义在某种程度上是不正确的。或者有一个“更好的”定义？），但它可能会帮助您了解，对于

suc-*-comm m n = refl

块中

where

的定义，主要证明的第一步，

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

减少到

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

因此

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

因此，类似于最后一步，最终

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

因此，您将不再需要

where

块...