Tensor Coordinates

This module connects the public Spec.Shape API to row-major coordinate geometry. Both the specification and buffer layers use the same list of dimensions; their size functions are connected explicitly so that each layer retains its own simplification API. Shape.Coord supplies the finite coordinate space used by verified tensor lowering.

@[reducible, inline]

abbrev Spec.Shape.Coord (shape : Shape) : Type

The finite multidimensional coordinate type of a TorchLean shape.

theorem Spec.Shape.internalSize_eq (shape : Shape) : TorchLean.Tensor.Internal.Shape.size shape = shape.size

The buffer-level element count agrees with the spec-level one.

Not a simp lemma. Spec.Shape.size and Tensor.Internal.Shape.size are two definitions of the same function on the same type, one for each layer, and rewriting every buffer-level count into a spec-level one would strand the buffer lemmas that Rep proofs rely on. Bridge explicitly where a spec-level fact has to meet a buffer-level obligation.

theorem Spec.Shape.internalSize_congr {source target : Shape} (hSize : source.size = target.size) : TorchLean.Tensor.Internal.Shape.size source = TorchLean.Tensor.Internal.Shape.size target

Transport a spec-level size equality down to the buffer level.

The companion of internalSize_eq for the common case where a definition demands the buffer-level equality and the caller has the spec-level one.

def Spec.Shape.Coord.linearize {shape : Shape} (coordinate : shape.Coord) : Fin shape.size

Convert a multidimensional coordinate to its row-major flat index.

def Spec.Shape.Coord.unlinearize {shape : Shape} (index : Fin shape.size) : shape.Coord

Recover a multidimensional coordinate from a row-major flat index.

def Spec.Shape.Coord.toList (shape : Shape) : shape.Coord → List ℕ

Expose a statically valid coordinate as outermost-first natural indices.

def Spec.Shape.Coord.ofList? (shape : Shape) : List ℕ → Option shape.Coord

Validate a runtime coordinate list against a static tensor shape.

The list is outermost-first and must contain exactly one in-bounds index per axis. Successful validation returns the ordinary proof-carrying coordinate.

def Spec.Shape.Coord.ofArray? (shape : Shape) (coordinates : Array ℕ) : Option shape.Coord

Validate runtime array coordinates against a static tensor shape.

@[simp]

theorem Spec.Shape.Coord.ofList?_toList (shape : Shape) (coordinate : shape.Coord) : ofList? shape (toList shape coordinate) = some coordinate

A statically valid coordinate validates when converted to runtime indices.

@[simp]

theorem Spec.Shape.Coord.linearize_unlinearize {shape : Shape} (index : Fin shape.size) : (unlinearize index).linearize = index

Unlinearizing and then linearizing recovers the flat index.

@[simp]

theorem Spec.Shape.Coord.unlinearize_linearize {shape : Shape} (coordinate : shape.Coord) : unlinearize coordinate.linearize = coordinate

Linearizing and then unlinearizing recovers the multidimensional coordinate.