Checked rearrangement equivalence #
Extensional comparison, executable decisions, counterexamples, and compact row-major certificates for checked rearrangement plans.
Extensional equivalence of two checked rearrangements with equal physical input and output shapes.
The shape equalities transport the second plan's coordinates into the first plan's coordinate types. Requiring equality at every output coordinate makes the definition independent of axis spelling, ellipsis use, and grouping.
Instances For
Decide whether two checked rearrangements have equal shapes and the same coordinate map.
Unlike comparison of parsed syntax, this accepts patterns that use different axis names or ellipsis spellings but denote the same tensor transformation.
Instances For
Return an output coordinate where two equal-shaped rearrangements select different input coordinates.
A shape mismatch returns none: the unequal shapes themselves are already a
complete reason for inequivalence. When the physical shapes agree, none
means the coordinate maps are equivalent.
Instances For
The Boolean comparison is exact once the common shapes are fixed.
The Boolean comparison succeeds exactly when common input and output shapes and an extensional coordinate proof exist.
With common shapes, absence of a counterexample is equivalent to extensional equivalence.
Every returned counterexample is sound: at that output coordinate, the two plans select different input coordinates after shape transport.
Extensional rearrange equivalence is symmetric.
Extensional rearrange equivalence is transitive.
Linearizing the general checked output-to-input coordinate projection gives the compact row-major index calculation.
Unlike rearrangeCoordinateEquiv_linearize, this theorem requires only that
every input axis occurs in the output. It therefore covers both permutations
and repeats that introduce arbitrarily many new axes.
Linearize the general checked output-to-input projection at an arbitrary output coordinate.
Compute the checked source flat index selected by an output flat index.
The value is the compact list-and-arithmetic program used by native lowering; its bound follows from the independent coordinate semantics.
Instances For
The executable checked flat-index projection equals linearization of the independent coordinate projection.
Linearizing the checked rearrangement coordinate map gives the compact
natural-number calculation rearrangeLinearIndex.
This theorem is the trust boundary for proof automation: the tactic may reduce the compact calculation, while the kernel checks here that it denotes the independent coordinate semantics.
Linearize a checked rearrangement at an arbitrary output coordinate.
This coordinate form composes directly: repeated rewriting turns a chain of
checked equivalences into nested rearrangeLinearIndex calculations.
The explicit function projection of a rearrangement equivalence has the same compact row-major index semantics as its coercion to a function.
Generated fusion terms retain .toFun so their executable composition is
unambiguous; this form lets proof automation normalize that representation
without unfolding the checked coordinate map.
Linearizing a checked rearrangement is insensitive to transport of its output coordinate across an equal physical shape.
This is the composition form used by proof-producing fusion. It absorbs the dependent cast introduced when independently checked stages share a physical shape, then exposes the same compact row-major index calculation as the uncast coordinate theorem.