Tensor API Implementation

User-facing tensor API for TorchLean.

This is the implementation leaf behind the public NN.Tensor umbrella. It is the ergonomic layer that sits on top of the spec-first tensor semantics in NN.Spec.*. It does not introduce new math; it provides constructors and syntax intended for examples, tests, compact models, and introductory examples.

Typical responsibilities here:

• arbitrary-rank shapes represented by Spec.Shape,
• friendly constructors from lists and literals,
• small syntax helpers for examples/tests,
• and printing support for runtime-friendly dtypes.

Notation policy:

• keep compact literal constructors (shape!, tensor!, tensorOfList!, tensorF!, tensor32!, fin!) in this module so they are easy to find and do not leak into unrelated imports,
• keep more semantic glyphs scoped when possible (as in NN.IR and NN.Floats.IEEEExec),
• and prefer namespace-local aliases over reusing the same unscoped token in multiple layers.

Lean is statically typed, so the element type usually plays the role of “dtype”:

let x := NN.Tensor.vector (α := Float) [0.1, 0.2] let q := NN.Tensor.vector (α := ℚ) [1, 2]

If you ever see Tensor Float _ in code: the _ is just “let Lean infer the shape from the RHS”. In examples we prefer to omit the type annotation entirely unless it helps readability.

For convenience, this module also provides constructors that start from Float literals and cast into common backends such as IEEE32Exec.

Printing: for Tensor ℝ we intentionally refuse to pretty-print, since that backend is meant for proof-oriented mathematics rather than runtime IO. Use Float, IEEE32Exec, ℚ, etc. for values you actually want to display.

@[reducible, inline]

abbrev NN.Tensor.Shape : Type

Local alias for the canonical spec shape type.

Scalar extraction

def NN.Tensor.scalarOf {α : Type} (t : Spec.Tensor α Spec.Shape.scalar) : α

Extract the scalar value from a scalar-shaped tensor.

PyTorch comparison: like t.item() for a 0-dim tensor.

@[reducible, inline]

abbrev Spec.Tensor.item {α : Type} (t : Tensor α Shape.scalar) : α

Dot-notation sugar for scalar tensors: t.item.

This is defined at the Spec.Tensor namespace so that it works with the canonical tensor type.

@[simp]

theorem Spec.Tensor.item_scalar {α : Type} (x : α) : (scalar x).item = x

Tensor.scalar x round-trips through Spec.Tensor.item.

Construction

@[reducible]

def NN.Tensor.shapeOfDims : List ℕ → Shape

Convert a runtime list of dimensions like [2, 3, 4] into a nested Shape.

Why this exists:

• In the spec layer we usually carry the shape in the type (great for safety).
• In “API land” we often start from lists (CLI args, JSON, compact examples, …).

shapeOfDims is the bridge between those representations.

@[simp]

theorem NN.Tensor.shapeOfDims_toList (s : Spec.Shape) : shapeOfDims s.toList = s

shapeOfDims round-trips through Spec.Shape.toList.

def NN.Tensor.numelDims (dims : List ℕ) : ℕ

Number of scalar elements (“numel”) implied by a runtime dims list.

def NN.Tensor.vector (α : Type := Float) (xs : List α) : Spec.Tensor α (Spec.Shape.dim xs.length Spec.Shape.scalar)

Create a 1-D tensor from a Lean List.

Notes:

• The shape is computed from xs.length, so the type remembers the length.
• This is total and does not perform any runtime checks.

PyTorch analogy: torch.tensor(xs) producing a 1D tensor.

One-hot vectors

def NN.Tensor.oneHot {α : Type} [Zero α] [One α] (n : ℕ) (k : Fin n) : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)

One-hot vector of length n, with a single 1 at index k.

def NN.Tensor.oneHotNat {α : Type} [Zero α] [One α] (n k : ℕ) : Spec.Tensor α (Spec.Shape.dim n Spec.Shape.scalar)

One-hot vector using a raw Nat index.

If $k\ge n$, we return the all-zeros vector instead of failing. This is convenient in data-conversion code where carrying a Fin n would obscure the caller.

def NN.Tensor.matrix? (α : Type := Float) [Inhabited α] (xss : List (List α)) : Option (Spec.Tensor α (Spec.Shape.dim xss.length (Spec.Shape.dim (if xss.isEmpty = true then 0 else xss.head!.length) Spec.Shape.scalar)))

2-D tensor from nested lists, returning none for empty/ragged inputs.

This delegates to Spec.from_list_2d, which refuses:

• an empty outer list,
• any empty row,
• or rows with mismatched lengths.

PyTorch analogy: torch.tensor(xss) also refuses ragged inputs.

def NN.Tensor.matrix (α : Type := Float) [Inhabited α] (xss : List (List α)) : Except String (Spec.Tensor α (Spec.Shape.dim xss.length (Spec.Shape.dim (if xss.isEmpty = true then 0 else xss.head!.length) Spec.Shape.scalar)))

2-D tensor from nested lists, with a clear error message on failure.

Ragged-friendly 2D constructors

def NN.Tensor.matrixPadTo (α : Type := Float) [Inhabited α] (nCols : ℕ) (xss : List (List α)) : Spec.Tensor α (Spec.Shape.dim xss.length (Spec.Shape.dim nCols Spec.Shape.scalar))

2-D tensor from nested lists, padding/truncating each row to nCols.

This is the permissive sibling of matrix: it never fails, but it will silently pad with default (and drop extra entries beyond nCols). This is useful when you intend ragged inputs (e.g. batching variable-length sequences after padding).

PyTorch analogy: closer to pad_sequence(..., batch_first=True) followed by torch.tensor.

def NN.Tensor.matrixPadRight (α : Type := Float) [Inhabited α] (xss : List (List α)) : Spec.Tensor α (Spec.Shape.dim xss.length (Spec.Shape.dim (Spec.maxRowLength xss) Spec.Shape.scalar))

2-D tensor from nested lists, padding to the maximum row length (0 if empty).

This is convenient when you just want a rectangular tensor without precomputing nCols.

General N-D tensors from a flat list

The “real” spec constructors are shape-indexed, i.e. you usually build tensors by recursion on a Shape. In example and data-loading code, though, it’s common to have:

• a runtime dims list (List Nat), and
• a flat list of scalars.

So we do a small amount of reshaping here.

Implementation note:

• buildFromFlat_ofLenEq consumes the flat list using a proof that lengths match.
• The public APIs (ofListOfLength and ofList) are the ones that establish that proof.

def NN.Tensor.buildFromFlatOfLenEq {α : Type} (s : Shape) (xs : List α) : xs.length = Spec.Shape.size s → Spec.Tensor α s

Build a shape-indexed tensor from a flat list, given a proof that the lengths match.

This is a helper for ofListOfLength/ofList: users typically want those APIs rather than recursing over Shape directly.

def NN.Tensor.ofListOfLength {α : Type} (dims : List ℕ) (xs : List α) (h : xs.length = numelDims dims) : Spec.Tensor α (shapeOfDims dims)

N-D tensor from a runtime dims list and a flat xs, given a proof of matching length.

This is the “static / proof-carrying” version: if you can prove the length match, you avoid any runtime checks and you keep a precise shape in the type.

def NN.Tensor.ofList {α : Type} (dims : List ℕ) (xs : List α) : Except String (Spec.Tensor α (shapeOfDims dims))

N-D tensor from a runtime dims list and a flat xs, with a runtime length check.

This is the “dynamic / user-friendly” version: it fails with a descriptive message if the number of provided scalars doesn’t match the implied numel.

Fill, zeros, and ones from runtime dimensions

def NN.Tensor.fillOfDims {α : Type} (value : α) (dims : List ℕ) : Spec.Tensor α (shapeOfDims dims)

Fill a tensor from a runtime dimension list.

The OfDims suffix distinguishes this constructor from Spec.fill, whose second argument is an already-typed Shape.

def NN.Tensor.zerosOfDims {α : Type} [Zero α] (dims : List ℕ) : Spec.Tensor α (shapeOfDims dims)

All-zeros tensor, from a runtime dims list.

def NN.Tensor.onesOfDims {α : Type} [One α] (dims : List ℕ) : Spec.Tensor α (shapeOfDims dims)

All-ones tensor, from a runtime dims list.

Tactics

ofListOfLength needs a proof that your flat list has the right length.

For the common “all dimensions and lists are literals/abbrevs” case, this tactic usually closes that goal automatically.

Usage: ofListOfLength ... (by tensor_len)

def NN.Tensor.tacticTensor_len : Lean.ParserDescr

tensorOfList! is the checked literal constructor for constants whose length proof should be solved by tensor_len.

It expands to ofListOfLength ... (by tensor_len), so you usually don’t have to write the proof. If the proof can’t be solved (for example, when dims is computed at runtime), elaboration fails; use ofList in that case.

def NN.Tensor.termTensorOfList!__ : Lean.ParserDescr

def NN.Tensor.«termTensorOfList!(_:=_)__» : Lean.ParserDescr

Typed variant of tensorOfList!.

This is the same constructor as tensorOfList! dims xs, but lets you explicitly specify the element type when numeric literals would otherwise default to an undesired type.

Example: def x : Tensor ℚ (shape![2, 2]) := tensorOfList! (ty := ℚ) [2, 2] [1, 2, 3, 4]

Implementation note: we avoid reserving a common identifier as a syntax keyword (Lean would then treat it as a keyword in downstream files). Instead, we parse an ident and check that it is ty.

shape! is a compact convenience macro for examples: build a Shape from a bracketed dimension list.

It expands through reducible shapeOfDims, so it stays definitionally aligned with tensorOfList! while still unfolding for dependent proofs and shape typeclass search.

Example: def s : Shape := shape![2, 3, 4]

def NN.Tensor.shapeBang : Lean.ParserDescr

tensor! is the "nested brackets" constructor, similar to writing nested Python lists in PyTorch.

Examples:

-- shape (2, 3, 4)
def x :=
  tensor! [
    [ [0,1,2,3],   [4,5,6,7],   [8,9,10,11] ],
    [ [12,13,14,15],[16,17,18,19],[20,21,22,23] ]
  ]

It is fully general over rank: the nesting depth determines the rank. Internally, it computes the dims from list lengths and flattens in row-major order (last dimension changes fastest), then calls tensorOfList!.

If you need runtime/ragged handling, use ofList/dynamicOfList instead.

Typed variant of tensor!.

This is useful when the leaf literals don’t uniquely determine the element type.

Example:

def x : Tensor ℚ (shape![2, 2]) :=
  tensor! (ty := ℚ) [[1, 2], [3, 4]]

def NN.Tensor.«termTensor!(_:=_)_» : Lean.ParserDescr

def NN.Tensor.termTensor!_ : Lean.ParserDescr

Untyped variant of tensor!.

This is the common case: Lean infers the element type from the literal leaves (e.g. Nat, Int, Float, ℚ, ...). If inference picks the wrong type, use the typed form tensor! (ty := α) ... instead.

Small index helpers

Writing ⟨0, by decide⟩ everywhere is noisy.

These macros are intended for examples/tests where the dimension is a literal or abbreviation, so by decide can close the bounds proof. They are not a replacement for carrying a real Fin n in library code.

Examples: Tensor.vecGet v fin0! Tensor.vecGet v fin1! Tensor.vecGet v (fin! 5 3)

def NN.Tensor.termFin0! : Lean.ParserDescr

def NN.Tensor.termFin1! : Lean.ParserDescr

Convenience index ⟨1, by decide⟩ for example code where the bound proof is decidable.

def NN.Tensor.termFin!__ : Lean.ParserDescr

Convenience index ⟨i, by decide⟩ packaged as Fin n, for examples/tests with literal bounds.

tensorF! is a convenience macro for constants: build from Float literals, then cast into your chosen runtime scalar backend using cast : Float → α.

Example: let w : Tensor α (.dim 3 (.dim 2 .scalar)) := tensorF! cast [3, 2] [0.1, 0.2, 0.3, 0.4, 0.5, 0.6]

This avoids noisy lists like [cast 0.1, cast 0.2, ...].

def NN.Tensor.termTensorF!___ : Lean.ParserDescr

tensor32! is the tensor! macro specialized to the executable IEEE-754 binary32 backend.

It builds a Tensor Float _ from a nested bracket literal, then casts elementwise via IEEE32Exec.ofFloat.

Example:

def w : Tensor TorchLean.Floats.IEEE32Exec (shape![2, 2]) :=
  tensor32! [[0.1, 0.2], [0.3, 0.4]]

def NN.Tensor.termTensor32!_ : Lean.ParserDescr

Dynamic tensor wrapper (shape not in the type)

structure NN.Tensor.DynTensor (α : Type) : Type

A tensor paired with its shape, where the shape is stored as data instead of being in the type.

This is useful when:

• you need to accept arbitrary tensors at runtime (CLI / file formats / interoperability),
• but you still want to carry a Shape around so downstream code can inspect it.

• s : Shape

  Runtime shape tag carried alongside the tensor.

• t : Spec.Tensor α self.s

  Shape-indexed tensor whose type is tied to s.

def NN.Tensor.dynamicOfList {α : Type} (dims : List ℕ) (xs : List α) : Except String (DynTensor α)

Build a DynTensor from runtime dims + flat data, with a runtime length check.

Common dtype helpers (from Float literals)

def NN.Tensor.float32Vector (xs : List Float) : Spec.Tensor TorchLean.Floats.F32 (Spec.Shape.dim xs.length Spec.Shape.scalar)

1-D tensor from Float literals, cast into the executable IEEE-754 FP32 backend.

def NN.Tensor.float32Matrix (xss : List (List Float)) : Except String (Spec.Tensor TorchLean.Floats.F32 (Spec.Shape.dim xss.length (Spec.Shape.dim (if xss.isEmpty = true then 0 else xss.head!.length) Spec.Shape.scalar)))

2-D tensor from Float literals, cast into the executable IEEE-754 FP32 backend.

Printing

class NN.Tensor.DTypeName (α : Type) : Type

A compact “dtype name” class used by NN.Tensor.print.

The class only records the display name needed by human-facing tensor output.

• name : String

@[implicit_reducible]

instance NN.Tensor.instDTypeNameFloat : DTypeName Float

Display name for Float tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameRat : DTypeName ℚ

Display name for rational tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameInt : DTypeName ℤ

Display name for integer tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameFP32 : DTypeName TorchLean.Floats.FP32

Display name for proof-level FP32 rounding-model tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameIEEE32Exec : DTypeName TorchLean.Floats.IEEE32Exec

Display name for executable IEEE-754 FP32 tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameReal : DTypeName ℝ

Display name for proof-level real-valued tensors in NN.Tensor.print.

@[implicit_reducible]

instance NN.Tensor.instDTypeNameComplex {α : Type} [DTypeName α] : DTypeName (TorchLean.Complex α)

Display name for TorchLean complex scalars in NN.Tensor.print.

class NN.Tensor.TensorPrintable (α : Type) : Type

A “pretty-printer with failure”.

We model printing as Except String String because some tensor element types are intentionally non-printable (e.g. ℝ or proof-only floating-point models).

• pretty {s : Shape} : Spec.Tensor α s → Except String String

@[implicit_reducible, instance 10]

instance NN.Tensor.instTensorPrintableOfToString {α : Type} [ToString α] : TensorPrintable α

Default printing for element types that support ToString.

@[implicit_reducible, instance 100]

instance NN.Tensor.instTensorPrintableReal : TensorPrintable ℝ

Printing is disabled by design for proof-level ℝ tensors.

@[implicit_reducible, instance 100]

instance NN.Tensor.instTensorPrintableFP32 : TensorPrintable TorchLean.Floats.FP32

Printing is disabled by design for the proof-only rounding model FP32.

def NN.Tensor.print {α : Type} [DTypeName α] [TensorPrintable α] {s : Shape} (t : Spec.Tensor α s) : IO Unit

Print a tensor with a dtype tag, or throw an IO.userError if the dtype refuses to print.