beweisen einen Satz in Agda. Fehler: sollte ein Funktionstyp sein, ist aber nicht

Question

Hier ist der Satz, den ich beweisen möchte.

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

ist, was ich

schrieb

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

ich einen neuen Satz prob4a geschaffen, um die Ausgabe in einer richtigen Reihenfolge anzuordnen. Und es ist in der Lage, Sätze in nat.thms.agda zu benutzen, um es zu beweisen.

und der Fehler ist

x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y) ein Funktion Typ sein sollte, aber es ist nicht bei der Überprüfung, dass (w * z) auf eine Funktion von Typ x + y + z + w * x + w * y ≡ x + y + z + (w * x + w * y)

so ein gültiges Argument ist Was bedeutet das? und wie kann ich es korrigieren, damit der Beweis funktioniert?

Answer 1

+-assoc braucht nur 3 Argumente, aber Sie haben 4 Argumente übergeben.

Agda klagt, dass ein Gleichheitstyp kein Funktionstyp ist, weil das Ergebnis von +-assoc auf 3 Argumente angewendet wird, ist ein Gleichheitstyp, aber ein 4. Argument bedeutet, dass es eine Funktion sein soll.