`agda`：如何指定方程推理中的步骤是通过函数的定义来实现的？

Question

我是 agda 的新手。当我进行等式推理时，如何指定特定步骤是通过函数的定义来实现的？

例如，采用以下自然数的定义：

open import Relation.Binary.PropositionalEquality
open ≡-Reasoning

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

add : Nat -> Nat -> Nat
add zero    x = x
add (suc x) y = suc (add x y)

我现在可以证明 2 + 3 等于 5：

_ : add 2 3 ≡ 5
_ =
  begin
     add 2 3
     
  ≡⟨⟩  -- replace notation
     add (suc (suc zero)) (suc (suc (suc zero)))
     
  ≡⟨⟩  -- inductive case of add
     suc (add (suc zero) (suc (suc (suc zero))))
     
  ≡⟨⟩  -- inductive case of add
     suc (suc (add zero (suc (suc (suc zero)))))
     
  ≡⟨⟩  -- base case of add
     suc (suc (suc (suc (suc zero))))
     
  ≡⟨⟩  -- replace notation
     5
  ∎

Agda 对此非常满意，但我想让它也检查我在某些步骤中的推理是否正确。有没有办法让我更换：

     suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨⟩  -- base case of add
     suc (suc (suc (suc (suc zero))))

与：

     suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨ ?put something here? ⟩
     suc (suc (suc (suc (suc zero))))

“？放东西在这里？”在哪里？但特指

add

定义中的基本情况，以便 agda 可以检查是否正是通过应用

add

可以减少我所说的表达式？

Answer 1

（不包括重写规则），Agda 减少表达式的唯一方法是诉诸定义。因此，尝试让 Agda“检查是否通过应用 add 可以精确地减少表达式”并没有多大意义。这是 Agda 能做到的唯一方法！

如果你真的想明确你正在使用基本情况的事实，你可以证明引理：

rightIdentity : forall x -> 0 + x ≡ x
rightIdentity x = refl

然后写：

suc (suc (add zero (suc (suc (suc zero)))))

  ≡⟨ cong (\a -> suc (suc a)) (rightIdentity (suc (suc (suc zero)))) ⟩

suc (suc (suc (suc (suc zero))))