Miscellaneous spec utilities

This file collects small helper definitions used across the spec layer.

The contents are intended to be broadly reusable: small constructors, shape-preserving maps, and conversion and pretty-printing helpers used by examples and by higher-level APIs.

Main definitions include:

• map_tensor (change the scalar type of a tensor, preserving shape),
• basic constructors like zeros/ones,
• simple pretty-printing (Spec.pretty) for executable scalar backends,
• list ↔ tensor helpers (from_list_1d, from_list_2d).

User-facing constructors in the tensor API (for example tensorOfList!, tensorF!) live in NN/Tensor/API.lean and are built on top of these utilities.

def Spec.mapTensor {α β : Type} {s : Shape} : (α → β) → Tensor α s → Tensor β s

Map a scalar function across a tensor, changing the element type.

PyTorch analogy: torch.Tensor.to(dtype=...) is implemented as a scalar cast map under the hood. We keep this explicit at the spec layer because it is a common building block.

def Spec.Tensor.Forall {α : Type} (p : α → Prop) {s : Shape} : Tensor α s → Prop

Forall p x means that every scalar entry of x satisfies p.

The definition is rank-generic: domain conditions such as positivity, finite-value assumptions, quantizer code ranges, and interval membership use the same predicate for scalars, vectors, and higher-rank tensors.

@[simp]

theorem Spec.Tensor.forall_scalar {α : Type} {p : α → Prop} {x : α} : Forall p (scalar x) ↔ p x

@[simp]

theorem Spec.Tensor.forall_dim {α : Type} {p : α → Prop} {n : ℕ} {s : Shape} {values : Fin n → Tensor α s} : Forall p (dim values) ↔ ∀ (i : Fin n), Forall p (values i)

theorem Spec.Tensor.forall_true {α : Type} {s : Shape} (x : Tensor α s) : Forall (fun (x : α) => True) x

The predicate that is always true holds at every tensor coordinate.

theorem Spec.Tensor.forall_mapTensor {α β : Type} {p : α → Prop} {q : β → Prop} {f : α → β} {s : Shape} {x : Tensor α s} (hx : Forall p x) (hf : ∀ (a : α), p a → q (f a)) : Forall q (mapTensor f x)

Transport a pointwise property through a shape-preserving scalar map.

theorem Spec.Tensor.forall_replicate {α : Type} {p : α → Prop} {s : Shape} {x : α} (hx : p x) : Forall p (replicate (scalar x))

Replicating a scalar satisfying p produces a tensor satisfying p everywhere.

theorem Spec.Tensor.forall_fill {α : Type} {p : α → Prop} {s : Shape} {x : α} (hx : p x) : Forall p (fill x s)

A constant-filled tensor satisfies any predicate satisfied by the constant.

Small constructors

def Spec.zeros (α : Type) [Zero α] (s : Shape) : Tensor α s

All‑zeros tensor of a given shape.

def Spec.ones (α : Type) [One α] (s : Shape) : Tensor α s

All‑ones tensor of a given shape.

def Spec.fullLike {α : Type} {s : Shape} : α → Tensor α s → Tensor α s

Fill a tensor with a constant, using the shape of an existing tensor.

PyTorch analogy: torch.full_like(t, value). We implement it by structural recursion so that the argument tensor is genuinely used (and so this stays friendly to linters).

def Spec.zerosLike {α : Type} [Zero α] {s : Shape} : Tensor α s → Tensor α s

All‑zeros tensor with the same shape as a given tensor.

PyTorch analogy: torch.zeros_like(t).

def Spec.onesLike {α : Type} [One α] {s : Shape} : Tensor α s → Tensor α s

All‑ones tensor with the same shape as a given tensor.

PyTorch analogy: torch.ones_like(t).

def Spec.zip {α : Type} {s : Shape} : Tensor α s → Tensor α s → Tensor (α × α) s

Zip two tensors pointwise into a tensor of pairs.

Tensor ↔ list utilities

def Spec.toList {α : Type} {s : Shape} : Tensor α s → List α

Convert a tensor into a flat list (row‑major by outermost dimension).

def Spec.pretty {α : Type} [ToString α] {s : Shape} : Tensor α s → String

Pretty‑print a tensor using ToString on scalars.

def Spec.useFin {n : ℕ} {α : Type} (values : Fin n → α) (h : 0 < n) : α

Evaluate a Fin n → α at index 0, given a proof that n > 0.

def Spec.expandLastDim {α : Type} {n : ℕ} (t : Tensor α (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n (Shape.dim 1 Shape.scalar))

Expand a vector into a column vector by inserting a trailing dimension of size 1.

def Spec.vectorFromList {α : Type} (xs : List α) : Tensor α (Shape.dim xs.length Shape.scalar)

Build a vector tensor from a list.

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

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

Build a matrix tensor from a list of rows (strict validation).

This is the "safe by default" constructor used by the user-facing API layer. It refuses empty input and refuses ragged rows, because that usually indicates a bug at the call site (e.g. an accidental missing column in imported weights).

PyTorch analogy: torch.tensor(xss) will also error if xss is ragged.

def Spec.maxRowLength {α : Type} (xss : List (List α)) : ℕ

Compute the maximum row length of a list of rows.

This is used to build a padded rectangular tensor from ragged input.

def Spec.matrixFromRowsPadTo {α : Type} [Inhabited α] (nCols : ℕ) (xss : List (List α)) : Tensor α (Shape.dim xss.length (Shape.dim nCols Shape.scalar))

Build a matrix tensor from a list of rows by padding/truncating to nCols.

This is the "permissive" constructor: it never fails, but it will silently pad missing entries with default (and ignore any extra entries beyond nCols).

This is useful when importing data that is naturally ragged, or when you intentionally want "pad-right with zeros" semantics (common in NLP style batching).

PyTorch analogy: this is closer to a manual pad_sequence + torch.tensor, except we do it directly as a tensor constructor at the spec layer.

def Spec.matrixFromRowsPadRight {α : Type} [Inhabited α] (xss : List (List α)) : Tensor α (Shape.dim xss.length (Shape.dim (maxRowLength xss) Shape.scalar))

Build a matrix tensor from a list of rows by padding to the maximum row length.

If xss = [], this returns a 0 x 0 tensor. Otherwise, the number of columns is max_row_length xss and shorter rows are padded with default.