使用Agda rewrite时为何需要sym？基于Peano自然数的证明分析

首先我们先给出Peano自然数在Agda中的定义，包括加法运算：

data ℕ : Set where
  zero : ℕ
  suc : ℕ → ℕ

_+_ : ℕ → ℕ → ℕ
zero + n = n
(suc m) + n = suc (m + n)

我们要证明的性质是：对于任意自然数m，zero + m ≡ m + zero，也就是零与任何数相加，交换顺序后结果相等。下面我们来看几种证明方式，以及你提出的rewrite相关疑问。

几种证明方式 #

1. 详细的等式推理写法 #

这种写法用begin/∎展开每一步的等式变换，清晰展示证明过程：

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) = 
  begin
    zero + suc n ≡⟨⟩
    zero + suc (zero + n) ≡⟨⟩
    suc (zero + n) ≡⟨ cong suc (comm-+₀ n) ⟩
    suc (n + zero) ≡⟨⟩
    suc n + zero
  ∎

2. 简洁的cong写法 #

利用cong函数（同态性：若a ≡ b则f a ≡ f b），直接基于归纳假设推导：

comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) = cong suc (comm-+₀ n)

3. 尝试用rewrite的写法（最初失败版） #

你尝试用rewrite替代cong，但最初的写法无法通过类型检查：

-- 无法通过类型检查的版本
comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) rewrite comm-+₀ n = refl

而使用sym (comm-+₀ n)就能通过：

-- 可通过的版本
comm-+₀ : ∀ (m : ℕ) → zero + m ≡ m + zero
comm-+₀ zero = refl
comm-+₀ (suc n) rewrite sym (comm-+₀ n) = refl

为什么rewrite场景需要用sym？ #

这核心在于Agda中rewrite的工作机制：
rewrite是基于语法形式，从左到右替换目标中的子项，它不会自动处理等式的双向替换，也不会自动化简未被证明的等式（比如n + zero ≡ n正是我们要通过归纳证明的内容）。

我们拆解归纳步骤的细节：
当处理suc n时，目标会先通过加法定义自动化简：

• 左边zero + suc n根据加法第一条规则，直接化简为suc n
• 右边suc n + zero根据加法第二条规则，化简为suc (n + zero)

所以此时我们的目标变成了：suc n ≡ suc (n + zero)

而我们的归纳假设comm-+₀ n的语法类型是zero + n ≡ n + zero，虽然zero + n定义上等于n，但rewrite只会看语法上的子项——目标里根本没有zero + n这个子结构，所以直接rewritecomm-+₀ n不会产生任何替换效果，目标还是suc n ≡ suc (n + zero)，这时候refl无法通过（因为语法上两者不相等，Agda不会自动推导n + zero ≡ n，除非我们提供证明）。

而sym (comm-+₀ n)的作用是翻转等式的左右两边，把zero + n ≡ n + zero变成n + zero ≡ zero + n。结合zero + n ≡ n的定义，这个翻转后的等式等价于n + zero ≡ n。此时rewrite这个等式，Agda会把目标中的n + zero替换成n，目标就变成了suc n ≡ suc n，这时候refl自然就成立了。

反观另外两种方法：

• cong写法是直接利用同态性，把归纳假设的等式两边都应用suc函数，直接得到我们需要的目标等式，不需要考虑替换方向。
• 详细的等式推理写法则是手动调整子项（把suc n写成suc (zero + n)），让归纳假设的等式能够匹配上需要替换的部分，所以也不需要sym。

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