在Agda中证明*-assoc时，如何避免重复编写乘法定义？

背景说明 #

练习*-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块中添加乘法定义，希望找到避免重复编写乘法定义的方法。

解决方法 #

1. 直接导入Agda标准库的自然数模块 #

Agda的Data.Nat标准库已经内置了自然数乘法的定义，以及你用到的suc-*-comm（对应标准库中的*ˡ-suc）、*-distrib-+等基础引理。只需在代码开头添加导入语句，就能直接复用这些内容，无需自己重复定义：

open import Data.Nat using (ℕ; zero; suc; _*_; *-distrib-+; *ˡ-suc)

导入后，你可以直接用*ˡ-suc替代自己写的suc-*-comm，完全省去重复定义的步骤。

2. 自定义公共引理模块 #

如果不想依赖标准库，或者需要自定义一些项目专属的基础引理，可以把这些通用性质单独放到一个独立模块中，比如创建NatLemmas.agda：

module NatLemmas where
open import Data.Nat using (ℕ; zero; suc; _*_; _+_)

suc-*-comm : ∀ (m n : ℕ) → (suc m) * n ≡ n + m * n
suc-*-comm m n = refl

*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
-- 这里补充该引理的证明

之后在需要的证明文件中导入这个模块即可：

open import NatLemmas using (suc-*-comm; *-distrib-+)

所有需要用到这些引理的地方都能直接调用，不用每次在where块里重复编写。

3. 利用rewrite关键字简化推导 #

不需要手动展开乘法定义，直接用rewrite关键字调用已有的等式引理，可以大幅简化证明代码，完全避免手动重写的繁琐：

*-assoc : ∀ (m n p : ℕ) → (m * n) * p ≡ m * (n * p)
*-assoc zero n p = refl
*-assoc (suc m) n p rewrite *ˡ-suc m n | *-distrib-+ n (m * n) p | *-assoc m n p = refl

内容的提问来源于stack exchange，提问作者IvoryESeagull