Normalized transformation patterns

Normalization expands ellipses against a statically known input rank and replaces surface axes by stable elementary-axis identifiers. The result carries the rank and operation-specific well-formedness facts needed by later checking and semantics.

inductive TorchLean.Tensor.Internal.Check.TransformKind : Type

The three transformation modes with distinct axis-set rules.

• rearrange : TransformKind

  Permute and reshape axes without creating or reducing elements.

• repeat : TransformKind

  Insert and replicate axes while preserving every input axis.

• reduce : TransformKind

  Remove input axes with an explicitly chosen reduction.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instReprTransformKind : Repr TransformKind

def TorchLean.Tensor.Internal.Check.instReprTransformKind.repr : TransformKind → ℕ → Std.Format

def TorchLean.Tensor.Internal.Check.instBEqTransformKind.beq : TransformKind → TransformKind → Bool

@[implicit_reducible]

instance TorchLean.Tensor.Internal.Check.instBEqTransformKind : BEq TransformKind

instance TorchLean.Tensor.Internal.Check.instReflBEqTransformKind : ReflBEq TransformKind

instance TorchLean.Tensor.Internal.Check.instLawfulBEqTransformKind : LawfulBEq TransformKind

@[implicit_reducible]

instance TorchLean.Tensor.Internal.Check.instDecidableEqTransformKind : DecidableEq TransformKind

inductive TorchLean.Tensor.Internal.Check.AxisId : Type

Stable identity of an elementary axis after ellipsis expansion.

• named (name : String) : AxisId

  A logical axis identified by its source name.

• anonymous (value occurrence : ℕ) : AxisId

  A numeric axis identified by both its length and source occurrence.

• ellipsis (index : ℕ) : AxisId

  One concrete dimension generated by expanding an ellipsis.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.instReprAxisId : Repr AxisId

def TorchLean.Tensor.Internal.Check.instReprAxisId.repr : AxisId → ℕ → Std.Format

@[implicit_reducible]

instance TorchLean.Tensor.Internal.Check.instBEqAxisId : BEq AxisId

def TorchLean.Tensor.Internal.Check.instBEqAxisId.beq : AxisId → AxisId → Bool

instance TorchLean.Tensor.Internal.Check.instReflBEqAxisId : ReflBEq AxisId

instance TorchLean.Tensor.Internal.Check.instLawfulBEqAxisId : LawfulBEq AxisId

def TorchLean.Tensor.Internal.Check.instDecidableEqAxisId.decEq (x✝ x✝¹ : AxisId) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance TorchLean.Tensor.Internal.Check.instDecidableEqAxisId : DecidableEq AxisId

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.AxisId.isAnonymous : AxisId → Bool

Whether an axis is an anonymous numeric occurrence.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.Impl.expandAxis (ellipsisAxes : List AxisId) (axis : Syntax.Axis) : List AxisId

Expand one parsed axis into its elementary normalized axes.

This helper is exposed only because elaborated transformation certificates reduce expandExpression in downstream modules.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.Impl.isBareEllipsis (axis : Syntax.CompositeAxis) : Bool

Whether a physical axis consists solely of an unparenthesized ellipsis.

The distinction matters because a bare ellipsis contributes several physical dimensions, whereas a parenthesized ellipsis remains one composite dimension.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.expandComposite (ellipsisAxes : List AxisId) (axis : Syntax.CompositeAxis) : List (List AxisId)

Expand one composition, splitting a bare ellipsis into separate dimensions.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.expandExpression (ellipsisAxes : List AxisId) (expression : Syntax.Expression) : List (List AxisId)

Expand every composition in an expression against rank-generated ellipsis axes.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.axesSubset (left right : List AxisId) : Bool

Whether every elementary axis in left also occurs in right.

theorem TorchLean.Tensor.Internal.Check.axesSubset_eq_true_iff {left right : List AxisId} : axesSubset left right = true ↔ ∀ ⦃axis : AxisId⦄, axis ∈ left → axis ∈ right

The Boolean subset test exactly expresses list-element containment.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.Impl.hasAnonymous (axes : List AxisId) : Bool

Whether a normalized axis list contains a numeric anonymous axis.

This helper remains under Internal; its body is visible so generated well-formedness certificates can reduce anonymousAxesAllowed.

structure TorchLean.Tensor.Internal.Check.NormalizedTransform : Type

A transformation pattern after rank-specific ellipsis expansion.

• kind : TransformKind

  Operation whose axis-set rules the normalized pattern must satisfy.

• source : Syntax.TransformPattern

  Original parsed pattern, retained for diagnostics and source conventions.

• input : Shape

  Physical input against which the left side was normalized.

• ellipsisRank : ℕ

  Number of physical dimensions represented by the input ellipsis.

• ellipsisAxes : List AxisId

  Fresh logical axes replacing the ellipsis, in physical order.

• inputGroups : List (List AxisId)

  Elementary input axes grouped by physical input dimension.

• outputGroups : List (List AxisId)

  Elementary output axes grouped by physical output dimension.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.NormalizedTransform.inputAxes (normalized : NormalizedTransform) : List AxisId

Elementary input axes in source order.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.NormalizedTransform.outputAxes (normalized : NormalizedTransform) : List AxisId

Elementary output axes in source order.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.NormalizedTransform.axisRelation (normalized : NormalizedTransform) : Bool

The axis-set condition associated with the selected transformation mode.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.NormalizedTransform.anonymousAxesAllowed (normalized : NormalizedTransform) : Bool

Whether the mode permits all anonymous axes present in the pattern.

@[implicit_reducible]

def TorchLean.Tensor.Internal.Check.NormalizedTransform.ellipsisRankValid (normalized : NormalizedTransform) : Prop

The rank equation determining the number of expanded ellipsis axes.

@[instance_reducible]

instance TorchLean.Tensor.Internal.Check.NormalizedTransform.instDecidableEllipsisRankValid (normalized : NormalizedTransform) : Decidable normalized.ellipsisRankValid

The ellipsis rank equation is constructively decidable from the finite pattern and shape data.

structure TorchLean.Tensor.Internal.Check.NormalizedTransform.Valid (normalized : NormalizedTransform) : Prop

All structural facts established by normalization.

• left_ellipsis_unique : normalized.source.left.ellipsisCount ≤ 1

  The input expression contains at most one ellipsis.

• right_ellipsis_unique : normalized.source.right.ellipsisCount ≤ 1

  The output expression contains at most one ellipsis.

• left_ellipsis_bare : normalized.source.left.hasParenthesizedEllipsis = false

  An input ellipsis occupies a complete physical-axis position.

• right_ellipsis_has_source : normalized.source.right.ellipsisCount = 0 ∨ normalized.source.left.ellipsisCount = 1

  An output ellipsis is present only when the input supplies its axes.

• ellipsis_rank : normalized.ellipsisRankValid

  The expanded ellipsis rank agrees with the physical input rank.

• ellipsis_axes : normalized.ellipsisAxes = List.map AxisId.ellipsis (List.range normalized.ellipsisRank)

  Ellipsis axes are the canonical fresh identifiers in physical order.

• input_expansion : normalized.inputGroups = expandExpression normalized.ellipsisAxes normalized.source.left

  Input groups are exactly the rank-specific expansion of the source syntax.

• output_expansion : normalized.outputGroups = expandExpression normalized.ellipsisAxes normalized.source.right

  Output groups are exactly the rank-specific expansion of the target syntax.

• input_rank : normalized.inputGroups.length = List.length normalized.input

  Expanded input groups correspond one-for-one with physical dimensions.

• input_nodup : normalized.inputAxes.Nodup

  Every elementary input axis has a unique semantic occurrence.

• output_nodup : normalized.outputAxes.Nodup

  Every elementary output axis has a unique semantic occurrence.

• axis_relation : normalized.axisRelation = true

  Input and output axis sets obey the selected operation's rule.

• anonymous_axes : normalized.anonymousAxesAllowed = true

  Anonymous numeric axes occur only in modes where their semantics is defined.

theorem TorchLean.Tensor.Internal.Check.NormalizedTransform.Valid.input_axes_subset_output_of_rearrange {normalized : NormalizedTransform} (valid : normalized.Valid) (hKind : normalized.kind = TransformKind.rearrange) ⦃axis : AxisId⦄ : axis ∈ normalized.inputAxes → axis ∈ normalized.outputAxes

Rearrange preserves every input elementary axis in its output.

theorem TorchLean.Tensor.Internal.Check.NormalizedTransform.Valid.output_axes_subset_input_of_rearrange {normalized : NormalizedTransform} (valid : normalized.Valid) (hKind : normalized.kind = TransformKind.rearrange) ⦃axis : AxisId⦄ : axis ∈ normalized.outputAxes → axis ∈ normalized.inputAxes

Rearrange introduces no output elementary axis absent from its input.

theorem TorchLean.Tensor.Internal.Check.NormalizedTransform.Valid.input_axes_subset_output_of_repeat {normalized : NormalizedTransform} (valid : normalized.Valid) (hKind : normalized.kind = TransformKind.repeat) ⦃axis : AxisId⦄ : axis ∈ normalized.inputAxes → axis ∈ normalized.outputAxes

Repeat retains every input elementary axis and may add new output axes.

theorem TorchLean.Tensor.Internal.Check.NormalizedTransform.Valid.output_axes_subset_input_of_reduce {normalized : NormalizedTransform} (valid : normalized.Valid) (hKind : normalized.kind = TransformKind.reduce) ⦃axis : AxisId⦄ : axis ∈ normalized.outputAxes → axis ∈ normalized.inputAxes

Reduce retains only elementary axes already present in its input.

structure TorchLean.Tensor.Internal.Check.CheckedNormalization : Type

A normalized pattern bundled with its machine-checked invariant.

• value : NormalizedTransform

  Normalized transformation data consumed by shape resolution.

• valid : self.value.Valid

  Proof that normalization established every structural invariant.

def TorchLean.Tensor.Internal.Check.normalize (kind : TransformKind) (pattern : Syntax.TransformPattern) (inputShape : Shape) : Result CheckedNormalization

Expand a parsed transformation pattern against a concrete input rank.

The returned proof records rank agreement, ellipsis expansion, uniqueness of elementary axes, and the mode-specific axis relation.