Idx

Utilities for working with typed context indices (Idx) in tape-style graphs.

Many graph-construction proofs need two basic operations:

• weaken an index when the context is extended by more intermediates; and
• refer to the last element of an appended shape list (Γ ++ ss ++ [τ]).

We centralize them here to avoid repeating the same list-arithmetic boilerplate in every op graph (LayerNorm, BatchNorm, attention, …).

def Proofs.Autograd.Idx.weaken {Γ : List Spec.Shape} {s : Spec.Shape} (idx : Idx Γ s) (rest : List Spec.Shape) : Idx (Γ ++ rest) s

Weaken a typed index when the context is extended by appending more shapes.

If idx : Idx Γ s, then weaken idx rest : Idx (Γ ++ rest) s.

def Proofs.Autograd.Idx.last {Γ ss : List Spec.Shape} {τ : Spec.Shape} : Idx (Γ ++ ss ++ [τ]) τ

Typed index for the last element of an appended shape list.

Idx.last is the canonical index of τ in Γ ++ ss ++ [τ].