Semantic rearrangement equivalence

Coordinate-equivalent checked rearrangements have equal tensor denotations. The converse is witnessed by natural-number coordinate tensors.

theorem TorchLean.Tensor.Internal.Semantics.denoteRearrange_eq_of_equivalent {α : Type u} [Storage α] (first second : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hInputShape : first.value.normalized.input = second.value.normalized.input) (hOutputShape : first.value.output = second.value.output) (hEquivalent : first.RearrangeEquivalent second hFirstKind hSecondKind hInputShape hOutputShape) (inputTensor : first.InputTensor α) : denoteRearrange first hFirstKind inputTensor = cast ⋯ (denoteRearrange second hSecondKind (cast ⋯ inputTensor))

Equivalent rearrange coordinate maps produce equal tensors over every scalar type. The casts only transport tensors across the supplied physical-shape equalities.

theorem TorchLean.Tensor.Internal.Semantics.rearrangeEquivalent_of_denoteRearrange_nat_eq (first second : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hInputShape : first.value.normalized.input = second.value.normalized.input) (hOutputShape : first.value.output = second.value.output) (hDenotations : ∀ (inputTensor : first.InputTensor ℕ), denoteRearrange first hFirstKind inputTensor = cast ⋯ (denoteRearrange second hSecondKind (cast ⋯ inputTensor))) : first.RearrangeEquivalent second hFirstKind hSecondKind hInputShape hOutputShape

Natural-number coordinate tensors separate rearrange maps. Thus equality on all Nat tensors is not merely sufficient but also necessary for extensional pattern equivalence.

theorem TorchLean.Tensor.Internal.Semantics.rearrangeEquivalent_iff_denoteRearrange_nat_eq {first second : Check.CheckedTransform} {hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange} {hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange} {hInputShape : first.value.normalized.input = second.value.normalized.input} {hOutputShape : first.value.output = second.value.output} : first.RearrangeEquivalent second hFirstKind hSecondKind hInputShape hOutputShape ↔ ∀ (inputTensor : first.InputTensor ℕ), denoteRearrange first hFirstKind inputTensor = cast ⋯ (denoteRearrange second hSecondKind (cast ⋯ inputTensor))

For fixed shapes, coordinate equivalence is exactly equality of rearrange denotations on all natural-number tensors.

@[simp]

theorem TorchLean.Tensor.Internal.Semantics.denoteRearrange_inverse {α : Type u} [Storage α] (checked : Check.CheckedTransform) (hKind : checked.value.normalized.kind = Check.TransformKind.rearrange) (outputTensor : checked.OutputTensor α) : denoteRearrange checked hKind (Rep.reindex (checked.rearrangeCoordinateEquiv hKind).symm outputTensor) = outputTensor

Applying a rearrangement after reindexing by its inverse coordinate map recovers the output tensor. Together with inverse_denoteRearrange, this states both inverse laws at the semantic level.

theorem TorchLean.Tensor.Internal.Semantics.denoteRearrange_comp {α : Type u} [Storage α] (first second : Check.CheckedTransform) (hFirstKind : first.value.normalized.kind = Check.TransformKind.rearrange) (hSecondKind : second.value.normalized.kind = Check.TransformKind.rearrange) (hMiddleShape : first.value.output = second.value.normalized.input) (inputTensor : first.InputTensor α) : denoteRearrange second hSecondKind (cast ⋯ (denoteRearrange first hFirstKind inputTensor)) = Rep.reindex ((second.rearrangeCoordinateEquiv hSecondKind).trans ((Equiv.cast ⋯).trans (first.rearrangeCoordinateEquiv hFirstKind))) inputTensor

Two successive checked rearrangements equal one reindexing by the composite coordinate equivalence. The middle-shape cast is explicit because checked plans store, rather than index over, their physical shapes.