Index casts — relabelling a graph's index along a proved Nat equality #
Nat multiplication is not definitionally associative, so the network's left-associated
c·h·w (and N·(c·h·w)) and the BatchNorm / channel-LayerNorm ops' c·(h·w) are different
types for the same tensor. castIdx h e is the same graph typed at the other index; the emitted
text does not change (h : n = m, so after subst the skel is the same; not stated as a lemma
here), and den_castIdx says the denotation is read through Fin.cast. la_assoc is the
batched seam N·(c·h·w) = N·(c·(h·w)).
The same reshuffle on plain vectors is BackLinks.reassocB (batched, Batched.BackLinks) and
reassocFwd / reassocBack (per example, PerChannelBN); den_reassocS / den_unassocS
(ConvNeXtChannelLN) identify the graph casts reassoc / unassoc with those.
Relabel an AST value's index along a proved equality. h ▸ e: the same graph, typed at
m instead of n. The emitted text does not change: n = m, so skel is unchanged (by
subst; skel itself keeps the index).
Equations
- Proofs.StableHLO.castIdx h e = h ▸ e
Instances For
c·h·w → c·(h·w): the Nat.mul_assoc relabelling a channel-last transpose needs.