Documentation

LeanMlir.Proofs.Foundation.IndexCast

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 (skel erases indices), and den_castIdx says the denotation is read through Fin.cast. laAssoc is the batched seam N·(c·h·w) = N·(c·(h·w)).

The same reshuffle on plain vectors is EnetTiePoC.reassocB (batched, BatchedBackLinks) and reassocFwd / reassocBack (per example, PerChannelBN); den_reassocS / den_unassocS (ConvNeXtChannelLN) identify the graph cast with those.

source
def Proofs.StableHLO.castIdx {n m : ℕ} (h : n = m) (e : SHlo n) :
SHlo m

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, because skel erases indices.

Equations
Instances For
    source
    theorem Proofs.StableHLO.den_castIdx {n m : ℕ} (h : n = m) (e : SHlo n) :
    den (castIdx h e) = fun (i : Fin m) => den e (Fin.cast ⋯ i)
    source
    theorem Proofs.StableHLO.laAssoc (N oc h w : ℕ) :
    N * (oc * h * w) = N * (oc * (h * w))

    The mul_assoc relabelling under N * · — the seam between the network's left-assoc N·(c·h·w) and the BatchNorm ops' N·(c·(h·w)).