Fixed-length vector and array interoperability

Lean's Vector α n is an Array α together with a proof that the array has exactly n entries. This module identifies that executable one-dimensional storage with the row-major entries of a tensor of any finite shape.

The equivalence is not restricted to rank one. A scalar tensor corresponds to a vector of length one, a matrix corresponds to a vector whose length is the product of its two dimensions, and a shape containing a zero-length axis corresponds to the empty vector.

def TorchLean.Tensor.Internal.Rep.vectorEquiv (α : Type u) [storage : Storage α] (shape : Shape) : Rep α shape ≃ Vector α shape.size

The equivalence between a tensor and its fixed-length row-major storage.

The vector contains one entry for every coordinate in shape. Converting back uses row-major linearization to recover the original multidimensional coordinate semantics.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.vectorEquiv_apply {α : Type u} [Storage α] {shape : Shape} (tensor : Rep α shape) (flatIndex : Fin shape.size) : ((vectorEquiv α shape) tensor).get flatIndex = tensor.get (Coord.unlinearize flatIndex)

Looking up a vector entry reads the tensor coordinate represented by the same row-major flat index.

@[simp]

theorem TorchLean.Tensor.Internal.Rep.vectorEquiv_symm_apply {α : Type u} [Storage α] {shape : Shape} (values : Vector α shape.size) (coordinate : Coord shape) : ((vectorEquiv α shape).symm values).get coordinate = values.get coordinate.linearize

Converting a vector back to a tensor reads each coordinate at its row-major linear index.

theorem TorchLean.Tensor.Internal.Rep.vectorEquiv_map {α : Type u} {β : Type v} [Storage α] [Storage β] {shape : Shape} (f : α → β) (tensor : Rep α shape) : (vectorEquiv β shape) (map f tensor) = Vector.map f ((vectorEquiv α shape) tensor)

Pointwise tensor maps become ordinary fixed-length vector maps.

theorem TorchLean.Tensor.Internal.Rep.vectorEquiv_reshape {α : Type u} [Storage α] {sourceShape targetShape : Shape} (hSize : sourceShape.size = targetShape.size) (tensor : Rep α sourceShape) : (vectorEquiv α targetShape) (reshape hSize tensor) = Vector.cast hSize ((vectorEquiv α sourceShape) tensor)

Reshape preserves the same row-major vector storage.

Only the proof-indexed vector length changes, so Vector.cast transports the source vector along the equality between the source and target shape sizes.

theorem TorchLean.Tensor.Internal.Rep.vectorEquiv_toArray_size {α : Type u} [Storage α] {shape : Shape} (tensor : Rep α shape) : ((vectorEquiv α shape) tensor).toArray.size = shape.size

The array underlying a tensor's vector view has exactly the tensor's number of entries.