matching on vectors

Stream: general

[Floris van Doorn]

Is there a library of vectors, defined inductively?

inductive dvector (α : Type u) : ℕ → Type u
| nil {} : dvector 0
| cons : ∀{n}, α → dvector n → dvector (n+1)

Alternatively, can I use the equation compiler to pattern match on vector in the library in a nice way? I want something resembling the definitions in the following code:

universe variables u v w
inductive dvector (α : Type u) : ℕ → Type u
| nil {} : dvector 0
| cons : ∀{n}, α → dvector n → dvector (n+1)

local notation h :: t  := dvector.cons h t
local notation `[` l:(foldr `, ` (h t, dvector.cons h t) dvector.nil `]`) := l

namespace dvector
variables {α : Type u} {β : Type v} {γ : Type w} {n : ℕ}

@[simp] protected def map (f : α → β) : ∀{n : ℕ}, dvector α n → dvector β n
| _ []      := []
| _ (x::xs) := f x :: map xs

@[simp] protected def map_id : ∀{n : ℕ} (xs : dvector α n), xs.map (λx, x) = xs
| _ []      := rfl
| _ (x::xs) := by dsimp; simp*

@[simp] protected def map_congr {f g : α → β} (h : ∀x, f x = g x) :
  ∀{n : ℕ} (xs : dvector α n), xs.map f = xs.map g
| _ []      := rfl
| _ (x::xs) := by dsimp; simp*

@[simp] protected def map_map (g : β → γ) (f : α → β): ∀{n : ℕ} (xs : dvector α n),
  (xs.map f).map g = xs.map (λx, g (f x))
  | _ []      := rfl
  | _ (x::xs) := by dsimp; simp*

end dvector

[Floris van Doorn]

(and yes, these operations are probably already defined for vector, but I want to define new operations on vectors using pattern matching, and I kind-of don't want to do it on lists first)

[Reid Barton]

vector.cons already has the pattern attribute; have you tried using it in the equation compiler?

[Floris van Doorn]

What does the pattern attribute do?
Yes, I tried matching on vectors using vector.nil and vector.cons, but something like this doesn't work:

protected def vector.my_map {α : Type u} {β : Type v} {γ : Type w} (f : α → β) :
 ∀{n : ℕ}, vector α n → vector β n
| _ vector.nil         := vector.nil
| _ (vector.cons x xs) := vector.cons (f x) (vector.my_map xs)

[Reid Barton]

It lets you use the definition in a pattern context, I'm not too sure of the details of how it works

[Reid Barton]

Yeah, it seems not to work, unfortunate...

[Reid Barton]

It seems like maybe the problem is the way that Lean moved the proof field of vector.nil into a theorem

[Reid Barton]

I wonder whether there is some option to disable that?

[Reid Barton]

though one would like it to not matter, since it is a Prop anyways

[Mario Carneiro]

@Floris van Doorn There should be a custom recursor for this

[Mario Carneiro]

that's usually the way we show alternate inductive patterns for types

[Reid Barton]

But can you use that with the equation compiler?

[Johan Commelin]

@Floris van Doorn In kbb we experimented with code like this:

def vector.mk {α : Type*} {n : ℕ} (l : list α) (pr : l.length = n) :
  vector α n := ⟨l, pr⟩

notation `![` l:(foldr `, ` (h t, list.cons h t) list.nil `]`) :=
  vector.mk l rfl

def {u} fast_matrix (m n : ℕ) (α : Type u) : Type u := vector (vector α n) m

example : fast_matrix 2 3 ℤ :=
![![ 1 , 1,  5 ],
  ![ 0 , 1, -2 ]]

It is not exactly what you want, but maybe a bit related.

[Floris van Doorn]

Yes, a custom recursor for vector would be nice. That doesn't affect pattern matching though, right?

[Floris van Doorn]

What is the reason to define vectors (and fin) this way, instead of the inductive family with the nicer pattern matching? Is it because the virtual machine can then use its representation of lists (and nat) for efficient computation?

[Floris van Doorn]

@Johan Commelin that is indeed nice notation. You can get the same effect if you define the notation using vector.nil and vector.cons, right?

[Mario Carneiro]

Yes, both of these types are implemented this way for efficient computation

[Mario Carneiro]

The downside of custom recursors is of course that they don't hook in to the equation compiler, so you don't get the nice pattern matching

[Mario Carneiro]

An alternative is to define the alternate inductive structure as vector2 or something, and prove an equiv

[Mario Carneiro]

If you want these, fin2 and vector2 are defined in dioph.lean

[Floris van Doorn]

Oh, so they do exist, just not in the data folder. In dioph I only find vector3 though. Where is vector2?

[Mario Carneiro]

oh, I thought I renamed it

[Mario Carneiro]

vector2 used to be just fin n -> A

[Mario Carneiro]

or maybe it was fin2 n -> A