Cast vector into one with equivalent length

Stream: new members

[Vivek Rajesh Joshi]

I have a function that outputs vectors that are of length z + k + 1, and I have a proof that n = z + k + 1. How do I make it output vectors of length n?

import Mathlib.Data.Matrix.Notation

structure ReducedRow (n : Nat) where
  z : Nat
  k : Nat
  tail : Vector Rat k
  h : n = z + k + 1

def zeroVec (k: Nat) : Vector Rat k := Vector.replicate k 0

def ReducedRow.toVector (row : ReducedRow n): Vector Rat (row.z+row.k+1) :=
  (zeroVec row.z).append (Vector.cons 1 row.tail)

[Anand Rao Tadipatri]

import Mathlib.Data.Matrix.Notation

structure ReducedRow (n : Nat) where
  z : Nat
  k : Nat
  tail : Vector Rat k
  h : n = z + k + 1

def zeroVec (k: Nat) : Vector Rat k := Vector.replicate k 0

def ReducedRow.toVector (row : ReducedRow n): Vector Rat n :=
  row.h ▸ (zeroVec row.z).append (Vector.cons 1 row.tail)

The triangle operator ▸ can be used here to substitute the equality into the term to get a result of the required type (the docstring that shows up when you hover over this symbol mentions references describing this operator in more detail).

[Eric Wieser]

does docs#Vector.cast exist?

[Eric Wieser]

@loogle ?m = ?n -> Vector _ ?m -> Vector _ ?n

[loogle]

:search: Vector.congr

[Eric Wieser]

You should prefer that to @Anand Rao Tadipatri's spelling above, as it is easier to prove things about

[Vivek Rajesh Joshi]

Cool, thanks!