subtraction in types in vector.tail

Stream: general

[Yakov Pechersky]

In core:

def head : vector α (nat.succ n) → α
| ⟨ [],    h ⟩ := by contradiction
| ⟨ a :: v, h ⟩ := a

[...]

def tail : vector α n → vector α (n - 1)
| ⟨ [],     h ⟩ := ⟨ [], congr_arg pred h ⟩
| ⟨ a :: v, h ⟩ := ⟨ v, congr_arg pred h ⟩

I don't understand why head requires a non-empty vector, but tail doesn't. And tail creates a nasty n - 1 dep-type. Why not:

def tail : vector α (nat.succ n) → vector α n
| ⟨ [],    h ⟩ := by contradiction
| ⟨ a :: v, h ⟩ := ⟨ v, sorry⟩

[Adam Topaz]

Because $0 - 1= 0$.

[Mario Carneiro]

and nat.succ n - 1 = n

[Mario Carneiro]

that definition of tail also accords with list.tail, which is not partial but returns the empty list on an empty input

[Yakov Pechersky]

If I do tail on a vector (n + 1) -- that is defeq to vector n?

[Mario Carneiro]

yes

[Yakov Pechersky]

Great.