如何在Agda的等式推理中指定步骤为函数定义应用？

你作为Agda新手，希望在等式推理里显式标注某一步是应用函数定义（比如add的基例），同时让Agda验证该步骤的正确性，而非使用空的≡⟨⟩。以下是两种可行方案：

方法1：定义对应引理并引用 #

先把add的基例单独抽成一个语义明确的可复用引理，Agda会自动确认其正确性：

add-zero : ∀ x → add zero x ≡ x
add-zero x = refl

这个引理完全对应add定义里的add zero x = x规则。

在等式推理的目标步骤中，使用cong（同余函数）将引理应用到嵌套表达式上——因为你的目标表达式是suc (suc (add zero ...))，需要对add zero ... ≡ ...的两边同时应用两次suc，所以用cong (suc ∘ suc)：

_ : add 2 3 ≡ 5
_ =
  begin
     add 2 3
  ≡⟨⟩  -- 展开自然数字面量
     add (suc (suc zero)) (suc (suc (suc zero)))
  ≡⟨⟩  -- 应用add的归纳case
     suc (add (suc zero) (suc (suc (suc zero))))
  ≡⟨⟩  -- 再次应用add的归纳case
     suc (suc (add zero (suc (suc (suc zero)))))
  ≡⟨ cong (suc ∘ suc) (add-zero (suc (suc (suc zero)))) ⟩
     suc (suc (suc (suc (suc zero))))
  ≡⟨⟩  -- 转换为自然数字面量
     5
  ∎

Agda会分两步验证：

1. add-zero (suc (suc (suc zero)))确实满足add zero (suc (suc (suc zero))) ≡ suc (suc (suc zero))
2. cong (suc ∘ suc)确保对等式两边同时应用suc ∘ suc后，等式仍然成立，完全匹配你要的推导逻辑。

方法2：直接使用refl（简洁但可读性稍弱） #

如果不想单独定义引理，也可以直接用refl，Agda会自动推导这一步是应用add的基例：

_ : add 2 3 ≡ 5
_ =
  begin
     add 2 3
  ≡⟨⟩
     add (suc (suc zero)) (suc (suc (suc zero)))
  ≡⟨⟩
     suc (add (suc zero) (suc (suc (suc zero))))
  ≡⟨⟩
     suc (suc (add zero (suc (suc (suc zero)))))
  ≡⟨ refl ⟩  -- Agda自动验证此步骤符合add的基例定义
     suc (suc (suc (suc (suc zero))))
  ≡⟨⟩
     5
  ∎

这种方式虽然能通过验证，但可读性不如定义引理——其他阅读代码的人需要自行识别这一步的逻辑，而add-zero这类引理名称能直接点明意图。

补充：归纳步骤的显式验证 #

同理，你也可以把add的归纳步骤做成引理，进一步强化证明的严谨性：

add-suc : ∀ x y → add (suc x) y ≡ suc (add x y)
add-suc x y = refl

之后把原来的空归纳步骤替换为：

≡⟨ add-suc (suc zero) (suc (suc (suc zero))) ⟩

这样整个证明的每一步都有显式的规则引用，逻辑更清晰。

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