vector types

Stream: general

[awalterschulze]

Currently there are two Vector types that I am aware of

Vector from std lib, which has no definition of induction, which makes proofs hard:

/-- `Vector α n` is an `Array α` with size `n`. -/
structure Vector (α : Type u) (n : Nat) where
  /-- The underlying array. -/
  toArray : Array α
  /-- Array size. -/
  size_toArray : toArray.size = n
deriving Repr, DecidableEq

List.Vector from mathlib4 which includes a custom definition of induction, so proofs work:

def List.Vector (α : Type u) (n : ℕ) :=
  { l : List α // l.length = n }

But why do both differ from the definitions in Rocq/Agda/The Little Typer:

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

Why was there decided to diverge from this Lean definition:

inductive Vec (α: Type): Nat -> Type where
  | nil : Vec α 0
  | cons (n: Nat) (x: α) (xs: Vec α n): Vec α (n + 1)

Before I start redefining this, has this been done somewhere else?
Or was there some reason that I shouldn't go down this path?

[Arthur Paulino]

My thinking is that Vector can sit on top of the efficiency characteristics of Array and List.Vector can profit from all the existing API from List.

[Henrik Böving]

Vector is defined as it is so it can use the good properties of Array in the runtime.

List.Vector is defined as is because it can reuse all the List API for free. Furthermore the inductively defined vectors have to carry around the n that tells the length of the tail in every cons node when compiled. So this is not a data structure you would ever want to use for executable code compared to { l : List α // l.length = n }

[awalterschulze]

Ah okay interesting. In Lean, unlike Coq, Agda and The Little Typer, execution is important and for execution speed the definition of Vec is not efficient. I don't quite understand why that is the case, why n would need to be carried around in compiled code after type checking, but that is okay, I can understand that Array is more efficient. I do also get that converting from a Subtype to a List vs running a toList function on Vec is more efficient.

Currently I do find that List.Vector in mathlib4 is more convenient for proofs, since it at least has a defined induction macro. I do hope Vector in the std lib gets one soon too.

I do still wonder if Vec would still be more convenient, just for proofs.

[Arthur Paulino]

"convenient" is a broad and subjective term. I, particularly, find it hard to beat the convenience of reusing all the definitions and theorems from List. If you define a completely new type, you'll have to bootstrap everything, which is quite the opposite of "convenient" IMO.

[awalterschulze]

All very true

[Mukesh Tiwari]

awalterschulze said:

Ah okay interesting. In Lean, unlike Coq, Agda and The Little Typer, execution is important and for execution speed the definition of Vec is not efficient. I don't quite understand why that is the case, why n would need to be carried around in compiled code after type checking, but that is okay, I can understand that Array is more efficient.

I do still wonder if Vec would still be more convenient, just for proofs.

Because n is of sort Nat and Nat is of sort Type. Anything that lives in Type remains the part of computations and anything that lives in Prop never participates in computations. Since n is of type Nat, you can do pattern match (eliminate) n then vector itself so n survives and becomes a part of computation. (This answer is based on Rocq experience but I think it’s true for Lean as well. I however wonder what would happen if the n of Vec Type n lives in Prop?)

[Shreyas Srinivas]

awalterschulze said:

Currently there are two Vector types that I am aware of

Vector from std lib, which has no definition of induction, which makes proofs hard:

/-- `Vector α n` is an `Array α` with size `n`. -/
structure Vector (α : Type u) (n : Nat) where
  /-- The underlying array. -/
  toArray : Array α
  /-- Array size. -/
  size_toArray : toArray.size = n
deriving Repr, DecidableEq

List.Vector from mathlib4 which includes a custom definition of induction, so proofs work:

def List.Vector (α : Type u) (n : ℕ) :=
  { l : List α // l.length = n }

But why do both differ from the definitions in Rocq/Agda/The Little Typer:

Inductive t A : nat -> Type :=
  |nil : t A 0
  |cons : forall (h:A) (n:nat), t A n -> t A (S n).

Why was there decided to diverge from this Lean definition:

inductive Vec (α: Type): Nat -> Type where
  | nil : Vec α 0
  | cons (n: Nat) (x: α) (xs: Vec α n): Vec α (n + 1)

Before I start redefining this, has this been done somewhere else?
Or was there some reason that I shouldn't go down this path?

you can still get induction on Vector. You can take a vector v and call v.toArray.toList

[awalterschulze]

Shreyas Srinivas said:

you can still get induction on Vector. You can take a vector v and call v.toArray.toList

Yes, but that doesn't work in all contexts.

xs = ys

can be transformed into

xs.toList = ys.toList

But when it is lower down in the equality, things are a bitter tougher

(map xs f).get i = f (xs.get i)

Maybe this is not the best example or maybe you know a trick I do not know about

[Shreyas Srinivas]

You prove the lifted version of list lemmas for arrays and vector. Fortunately the vector library already has quite a bit of this api.

[Mirek Olšák]

Note that there is also another typical way of representing vectors, and that is Fin n -> α. This is used for example for matrices, and denoted with ![1,2,3].

[awalterschulze]

Shreyas Srinivas said:

You prove the lifted version of list lemmas for arrays and vector. Fortunately the vector library already has quite a bit of this api.

Ok , but once you define your own functions on vectors, you also have to create lifted versions for each lemma you want to define on those functions?

[Mirek Olšák]

By the way, I can see one fundamental advantage of having List.Vector defined as a restricted List: Then the conversions to List and vice versa are definitionally equal.

example (v : List.Vector ℕ 20) : v = ⟨v.val, v.2⟩ := rfl
example (l : List ℕ) (h : l.length = 20) : (⟨l, h⟩ : List.Vector ℕ 20).val = l := rfl

besides this, it would not matter of course how we define List.Vector as long as we have the two conversions. Of course the advantage is that we can easily detach the proving part from manipulation, and therefore the manipulation is more flexible.

To me, the definition of Rocq / Agda / ... is a bit of show-off what a cool dependent type can be built in the system without caring much about consequences, and Lean's List.Vector is a reasonable decision to minimize dependent type hell, and realize that Vector is for most people just a List of fixed length... I have heard that Rocq defines even Fin with some DTT trick which is cool but not very practical (for Lean, Fin is just a restricted Nat).