Stream: new members

Topic: Adding vectors elementwise

Martin C. Martin (Apr 26 2023 at 20:35):

I'm defining a type for vector of length n, and a function to add them element wise. I've taken it mostly from section 8.7 in TPIL. However, I get an error I don't understand.

type mismatch at application
term
2::3::nil
has type
vector ?m_1 1.succ : Type ?
but is expected to have type
Type ? : Type (?+1)


what am I doing wrong?

import algebra.field.basic

universe u
inductive vector (α : Type u) : ℕ → Type u
| nil {}                              : vector 0
| cons {n : ℕ} (a : α) (v : vector n) : vector (nat.succ n)

namespace vector
local notation (name := cons) h :: t := cons h t

variables (F : Type*) [field F]

def myadd : Π { n : ℕ }, (vector F n) → (vector F n) → (vector F n)
| .(0)     nil           nil         := nil
| .(n + 1) (@cons .(F) n a₁ v₁) (cons a₂ v₂) := cons (a₁ + a₂) (myadd v₁ v₂)

example : myadd (2 :: 3 :: nil) (5 :: 7 :: nil) = 7 :: 10 :: nil := sorry

end vector


Ruben Van de Velde (Apr 26 2023 at 20:38):

First explicit argument to myadd is F, not a vector

Martin C. Martin (Apr 26 2023 at 20:41):

Oh, I thought it would be implicit since it's a variable imported from the context. Is there a good description somewhere for what things are implicit or explicit? Or the def syntax?

Ruben Van de Velde (Apr 26 2023 at 20:42):

(F) is explicit, {F} is implicit (and [field F] is another kind of implicit)

Martin C. Martin (Apr 26 2023 at 20:43):

Ah, in the variables statement! Thanks.

Martin C. Martin (Apr 26 2023 at 21:05):

So now I've ditched the Field altogether, since ℕ isn't a field, and have defined myadd as:

variable {α : Type u}
def myadd [has_add α] : Π { n : ℕ}, (vector α n) → (vector α n) → (vector α n)


However, when I try to enable infix + notation like this:

variable {n : ℕ}
instance : has_add (vector α n) := ⟨myadd⟩


It fails because I'm not restricting it only to places where α  has has_add α . How do I do that?

Eric Wieser (Apr 26 2023 at 21:08):

instance [has_add α] : has_add (vector α n) := ⟨myadd⟩

Last updated: Dec 20 2023 at 11:08 UTC