General tips and tricks for pattern matching on Vectors?

Stream: general

[AZMCode]

I keep running into issues when pattern matching using Mathlib's ::v constructor, and stright up do not know how to match the empty vector. What are the recommended ways to pattern match Vectors?

[Jason Rute]

#mwe ?

[Jason Rute]

Also, note that, unlike some ITPs, both docs#Vector and docs#List.Vector are not inductively defined. The first is an Array with a fixed length and the second is a List of fixed length. So it may not make sense to write recursive definitions on either, which is what I assume you mean by pattern matching.

[Notification Bot]

AZMCode has marked this topic as resolved.

[AZMCode]

Why would it not make sense to write recursive definitions with List.Vector though? Aren't lists meant to be easily pattern-matchable? There is the proof in the way, but it looks like the ::v constructor takes care of that. What would be the preferred approach?

[Jason Rute]

@AZMCode I think it would be best for you to write a small example of the sort of function you would like to write with vectors. (Make it clear which of the two vector types you are referring to.) If you like, you can write it with the notation you think would be most natural, even if Lean doesn’t accept that, as long as it is clear what your meaning is. Then one of us could show you an idiomatic way which works in Lean.

[AZMCode]

Will do in a moment. My initial issue was with confusing the default Array backed vector for the List backed vector. List backed is probably what im looking for for the indices and dimensions, since they're probably small and meant to go along a recursive structure.

The thing I'm trying to build, as an exercise (I don't know if something similar already exists, probably tho), is an N-Dimensional vector implemented via nested Vectors. Accesed via a Vector index and dimensioned according to another Vector.

I feel a particularly clean way to implement this would be via recursive functions, since the structure itself is recursive. Ive found the issues trying to pattern match on these indices and dimensions.Will post the specific code soon.

[AZMCode]

def nestedVectorTy (t: Type) {d: ℕ} (dim: List.Vector ℕ d): Type :=
    match d, dim with
        | (dp+1), hdim ::ᵥ tdim => nestedVectorTy (Vector t hdim) tdim
        | 0     , _             => t

structure NVector (t: Type) {d: ℕ} (dim: List.Vector ℕ d): Type where
    toNestedVector: (nestedVectorTy t dim)

Currently the compilation error is

invalid patterns, `tdim` is an explicit pattern variable, but it only occurs in positions that are inaccessible to pattern matching
  dp.succ

  ⟨hdim :: .(tdim.1), ⋯⟩

[Kim Morrison]

You might check Mathlib.Data.Holor for related work. (It has not been used since it was written in 2018, to my knowledge.)

[Kim Morrison]

@AZMCode, please check #mwe. e.g. your code block above is missing imports.

[Notification Bot]

Jason Rute has marked this topic as unresolved.

[Jason Rute]

Adding one possible import, you can simply do this by writing your function for List and then using dim.toList (which is O(1)) to extract the list:

import Mathlib

def nestedVectorTy_aux (t: Type) : (dim: List ℕ) -> Type
| hdim :: tdim => nestedVectorTy_aux (Vector t hdim) tdim
| []           => t

def nestedVectorTy (t: Type) {d: ℕ} (dim: List.Vector ℕ d): Type :=
  nestedVectorTy_aux t dim.toList

[Jason Rute]

(Also, why is the return value using Vector, but the input is using List.Vector? Or is this in the imports that you didn't include?)

[Jason Rute]

A more interesting example would be where you write a function from List.Vector to List.Vector. Here are two examples in the Mathlib code:

def reverse (v : Vector α n) : Vector α n :=
  ⟨v.toList.reverse, by simp⟩

def insertIdx (a : α) (i : Fin (n + 1)) (v : Vector α n) : Vector α (n + 1) :=
  ⟨v.1.insertIdx i a, by
    rw [List.length_insertIdx, v.2]
    split <;> omega⟩

Notice, these just work by computing the output on the underlying list and then also including a proof that the output length is as intended. In the first case simp was enough to give the proof. In the second case, one has to give a more manual proof.

[AZMCode]

(Also, why is the return value using Vector, but the input is using List.Vector? Or is this in the imports that you didn't include?)

I assumed it would better optimize if the multidimensional array was in a compact representation rather than a linked list. Not as good as compacting the multiple dimensions in a single array, but close enough for a first prototype.

Yes, i did omit the Mathlib import, my bad. Will make sure not to do that in future questions.

Notice, these just work by computing the output on the underlying list and then also including a proof that the output length is as intended. In the first case simp was enough to give the proof. In the second case, one has to give a more manual proof.

Would these not introduce an additional runtime check on the length of the lists?

You might check Mathlib.Data.Holor for related work. (It has not been used since it was written in 2018, to my knowledge.)

Assuming by the lack of usage, I assume nested Vectors are recommended for small and fixed dimensions? Kind of an unruly notation to carry around for even relatively small numbers of dimensions. Is there another more compact notation?

Also, I appreciate the Math pointers. I come from a Software Engineering perspective, so I have little maths knowledge as of now. Sure seems interesting!

[AZMCode]

BTW, I deeply appreciate the pointers. Just getting started here so the feedback is amazing. Thanks.

[AZMCode]

From this I gather pattern matching on vectors directly is discouraged, so I'll make sure to steer clear, however, in my google searches I haven't found this particular error before, about Inaccessible location in pattern matching. What does that mean precisely? Is it just about visibility protections, or something more interesting?

[Jason Rute]

AZMCode said:

Notice, these just work by computing the output on the underlying list and then also including a proof that the output length is as intended. In the first case simp was enough to give the proof. In the second case, one has to give a more manual proof.

Would these not introduce an additional runtime check on the length of the lists?

No, because at compile time you have already proved what the length of the list is, so you don’t need to compute it at runtime. Yay for proofs!

[Jason Rute]

While it looks like a List.Vector has two parts, the List and the proof, the proof isn’t actually included in the machine code. So it is just a List in machine code.