在AGDA中证明一个定理。错误：应该是函数类型，但不是

Question

这是我想要证明的定理。

prob4 : ∀(w x y z : ℕ) → w * (x + y + z) ≡ z * w + x * w + w * y
prob 4 = {!!}

这是我写的

open import Data.Nat
open import Data.Nat.Properties.Simple
open import Relation.Binary.PropositionalEquality
prob4a : ∀ (w x y z : ℕ) → w * (x + y + z) ≡ w * x + w * y + w * z
prob4a 0 x y z = refl
prob4a (suc w) x y z rewrite prob4a w x y z
            | +-assoc (x + y + z) (w * x) (w * y) (w * z) = ?

我创建了一个新的定理prob4a，以便以正确的顺序排列输出。它能够使用nat.thms.agda中的定理来证明它。

错误是

x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y)应该是 函数类型，但不是 当检查(w * z)是 类型 x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y)

那么这意味着什么？我怎样才能纠正它才能让证明工作？

Answer 1

+-assoc只需要 3 个参数，但您已经向其传递了 4 个参数。

Agda 抱怨说，相等类型不是函数类型，因为应用于 3 个参数的+-assoc的结果是相等类型，但传递第 4 个参数意味着您希望它成为函数。