Agda中多rewrite语句如何展开为with？对应等式链证明怎么写？

多rewrite的展开规则 #

你对多rewrite的猜测完全正确：rewrite eq1 | eq2和rewrite eq1 rewrite eq2语义完全等价，执行顺序是从左到右，后一个rewrite会在前一个rewrite修改后的目标和上下文基础上执行。

它对应的with展开是嵌套结构，而非你尝试的并列多参数with，标准展开形式如下：

-- 原写法
f params rewrite eq1 | eq2 = rhs

-- 等价展开为嵌套with
f params with LHS(eq1) | eq1
...        | _ | refl with LHS(eq2) | eq2
...               | _ | refl = rhs

其中LHS(eq)指等式eq的左项，rewrite的本质就是用等式的右项替换所有出现的左项。

你之前替换第一个rewrite时的报错原因有两个：

1. 你错误使用了并列双参数的with，而非嵌套结构
2. 自然数加法是左结合的，你写的dot pattern里的n + m + p等价于(n + m) + p，和推断得到的n + (m + p)在未应用加法结合律时不属于同一规范形式，自然匹配失败。

正确的等式链推导 #

你之前的等式链第一步就不符合加法定义，所以推导不成立。suc m + (n + p)根据加法的定义（suc a + b = suc (a + b)），第一步应该展开为suc (m + (n + p))，而非直接跳到n + suc (m + p)。

完整的正确等式链如下：

+-swap (suc m) n p =
  begin
    (suc m) + (n + p)
  ≡⟨⟩ -- 直接展开加法定义
    suc (m + (n + p))
  ≡⟨ cong suc (+-swap m n p) ⟩ -- 应用归纳假设替换括号内的子项
    suc (n + (m + p))
  ≡⟨ sym (+-suc' n (m + p)) ⟩ -- 反转+-suc'的方向，把suc移到加号里面
    n + suc (m + p)
  ≡⟨⟩ -- 展开suc m + p的定义
    n + ((suc m) + p)
  ∎

你的原rewrite版证明正确的原因刚好和这个推导顺序反过来：

1. 初始目标是(suc m) + (n + p) ≡ n + (suc m + p)，右项展开后为n + suc (m + p)
2. 首先用+-suc' n (m + p)把右项的n + suc (m + p)替换为suc (n + (m + p))，目标变为suc (m + (n + p)) ≡ suc (n + (m + p))
3. 再用归纳假设+-swap m n p把左项里的m + (n + p)替换为n + (m + p)，两边完全相等，直接用refl得证。

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