CODEWITHSUNDEEP
agda
qwer1234
qwer1234

Reputation: 267

prove a theorem in agda. Error : should be a function type, but isn't

Here is the theorem that I want to prove.

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

This is what I wrote

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) = ?

I created a new theorem prob4a in order to arrange the output in a correct order. And it's able to use theorems in nat.thms.agda to prove it.

and the error is

x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y) should be a function type, but it isn't when checking that (w * z) is a valid argument to a function of type x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y)

so what 's that mean? and how can i correct it in order to let the prove work?

Upvotes: 2

Views: 517

Answers (1)

gallais
gallais

Reputation: 12103

+-assoc only takes 3 arguments but you've passed 4 arguments to it.

Agda complains than an equality type is not a function type because the result of +-assoc applied to 3 arguments is an equality type but passing a 4th argument means you want it to be a function.

Upvotes: 2

Related Questions