Zulip Chat Archive

Stream: general

Topic: matching on vectors


Floris van Doorn (Oct 19 2018 at 21:29):

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 (Oct 19 2018 at 21:31):

(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 (Oct 19 2018 at 21:39):

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

Floris van Doorn (Oct 19 2018 at 21:51):

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 (Oct 19 2018 at 22:00):

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

Reid Barton (Oct 19 2018 at 22:03):

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

Reid Barton (Oct 19 2018 at 22:07):

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

Reid Barton (Oct 19 2018 at 22:07):

I wonder whether there is some option to disable that?

Reid Barton (Oct 19 2018 at 22:08):

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

Mario Carneiro (Oct 19 2018 at 22:52):

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

Mario Carneiro (Oct 19 2018 at 22:52):

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

Reid Barton (Oct 19 2018 at 23:23):

But can you use that with the equation compiler?

Johan Commelin (Oct 20 2018 at 03:39):

@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 (Oct 20 2018 at 22:26):

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

Floris van Doorn (Oct 20 2018 at 22:28):

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 (Oct 20 2018 at 22:30):

@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 (Oct 20 2018 at 22:37):

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

Mario Carneiro (Oct 20 2018 at 22:38):

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 (Oct 20 2018 at 22:39):

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

Mario Carneiro (Oct 20 2018 at 22:39):

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

Floris van Doorn (Oct 20 2018 at 22:45):

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

Mario Carneiro (Oct 21 2018 at 00:01):

oh, I thought I renamed it

Mario Carneiro (Oct 21 2018 at 00:02):

vector2 used to be just fin n -> A

Mario Carneiro (Oct 21 2018 at 00:02):

or maybe it was fin2 n -> A


Last updated: Dec 20 2023 at 11:08 UTC