Recursively defining zero vector

Stream: new members

[Martin C. Martin]

I have a standard definition of vector of length n, and want to define the zero vector for each n. Presumably this should be done recursively, but I can't figure out the syntax. How can I define it?

import algebra.field.basic

universe u
-- A vector of length n
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]
variable {n : ℕ}

instance : has_zero (vector F 0) := ⟨ nil ⟩

-- Error on the recursive 0 here:
instance : has_zero (vector F n.succ) := ⟨ (0 : F) :: (0 : (vector F n)) ⟩

end vector

[Mario Carneiro]

You should make just one definition

instance : has_zero (vector F n) := ⟨vector.zero n⟩

and define

def vector.zero : ∀ n : ℕ, vector F n

by recursion

[Martin C. Martin]

Thanks! I usually try to avoid an extra def like that, since it's not automatically expanded during proofs. But I guess a quick dsimp [vector.zero] is all that's needed?