通过列出所有情况来定义函数（例如 add ）是否有任何缺点？

Question

Add 通常定义为：

add : ℕ -> ℕ -> ℕ
add zero    m = m
add (suc n) m = suc (add n m)

这个定义很短，但使得 add-comm 之类的证明相当复杂，需要两个归纳函数并调用 subst、cong 和 sym。相反，如果我们将添加定义为：

add : ℕ -> ℕ -> ℕ
add zero    zero     = zero
add (suc n) zero     = suc n
add zero    (suc m)  = suc m
add (suc n) (suc m)  = suc (suc (add n m))

然后交换性的证明变得几乎微不足道：

add-comm : forall a b -> add a b ≡ add b a
add-comm zero    zero    = refl
add-comm zero    (suc b) = refl
add-comm (suc a) zero    = refl
add-comm (suc a) (suc b) = cong suc (cong suc (add-comm a b))

像 add 这样通过列出所有情况而不是经济地定义函数是否有任何负面影响？

Answer 1

你赢得了一些定义上的平等，但你失去了其他人。在这种情况下，您失去了 add (suc a) b 是任何 b 的 suc (add a b)。简而言之，如果你这里有更多案例，你需要更多案例 and/or 其他地方的证明，例如 Vec 附加：

open import Data.Vec

add-zero : ∀ n → add zero n ≡ n
add-zero zero    = refl
add-zero (suc n) = refl

suc-add : ∀ n m → suc (add n m) ≡ add (suc n) m
suc-add zero zero = refl
suc-add zero (suc m) = cong suc (cong suc (sym (add-zero m)))
suc-add (suc n) zero = refl
suc-add (suc n) (suc m) rewrite suc-add n m = refl

append : ∀ {n m}{A : Set} → Vec A n → Vec A m → Vec A (add n m)
append []       ys = subst (Vec _) (sym (add-zero _)) ys
append (x ∷ xs) ys = subst (Vec _) (suc-add _ _) (x ∷ append xs ys)

（原来的add-comm不需要二次定义）：

add : ℕ -> ℕ -> ℕ
add zero    m = m
add (suc n) m = suc (add n m)

add-comm : ∀ n m → add n m ≡ add m n
add-comm zero    zero    = refl
add-comm zero    (suc m) = cong suc (add-comm zero m)
add-comm (suc n) zero    = cong suc (add-comm n zero)
add-comm (suc n) (suc m)
  rewrite add-comm n (suc m)
        | sym (add-comm (suc n) m)
        | add-comm n m = refl

通过列出所有情况来定义函数（例如 add ）是否有任何缺点？

Is there any cons to defining functions (such as `add`) by listing all cases?

agda