Theorem: transpose_involutive (MLIR/Dialects/ToyModel.lean)

State before:
α n : ℕ
m : MLIR.AST.MLIRTy
⊢ ∀ (t : Matrix α n m), transpose (transpose t) = t
Tactic:
intro t
State after:
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ transpose (transpose t) = t

State before:
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ transpose (transpose t) = t
Tactic:
simp [transpose]
State after:
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ {
      toTensor :=
        { shape := [α, n],
          data :=
            List.remap
              (List.remap t.toTensor.data (transpose_remap α n)
                (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
              (transpose_remap n α)
              (_ :
                ∀ (n_1 : ℕ),
                  n_1 <
                      List.length
                        (List.remap t.toTensor.data (transpose_remap α n)
                          (_ :
                            ∀ (i : ℕ),
                              i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
                    transpose_remap n α n_1 <
                      List.length
                        (List.remap t.toTensor.data (transpose_remap α n)
                          (_ :
                            ∀ (i : ℕ),
                              i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))),
          h_data_size :=
            (_ :
              List.length
                  (List.remap
                    (List.remap t.toTensor.data (transpose_remap α n)
                      (_ :
                        ∀ (i : ℕ),
                          i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
                    (transpose_remap n α)
                    (_ :
                      ∀ (n_1 : ℕ),
                        n_1 <
                            List.length
                              (List.remap t.toTensor.data (transpose_remap α n)
                                (_ :
                                  ∀ (i : ℕ),
                                    i < List.length t.toTensor.data →
                                      transpose_remap α n i < List.length t.toTensor.data)) →
                          transpose_remap n α n_1 <
                            List.length
                              (List.remap t.toTensor.data (transpose_remap α n)
                                (_ :
                                  ∀ (i : ℕ),
                                    i < List.length t.toTensor.data →
                                      transpose_remap α n i < List.length t.toTensor.data)))) =
                shapeProd [α, n]) },
      h_refines :=
        (_ :
          shapeRefines
              { shape := [α, n],
                  data :=
                    List.remap
                      (List.remap t.toTensor.data (transpose_remap α n)
                        (_ :
                          ∀ (i : ℕ),
                            i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
                      (transpose_remap n α)
                      (_ :
                        ∀ (n_1 : ℕ),
                          n_1 <
                              List.length
                                (List.remap t.toTensor.data (transpose_remap α n)
                                  (_ :
                                    ∀ (i : ℕ),
                                      i < List.length t.toTensor.data →
                                        transpose_remap α n i < List.length t.toTensor.data)) →
                            transpose_remap n α n_1 <
                              List.length
                                (List.remap t.toTensor.data (transpose_remap α n)
                                  (_ :
                                    ∀ (i : ℕ),
                                      i < List.length t.toTensor.data →
                                        transpose_remap α n i < List.length t.toTensor.data))),
                  h_data_size :=
                    (_ :
                      List.length
                          (List.remap
                            (List.remap t.toTensor.data (transpose_remap α n)
                              (_ :
                                ∀ (i : ℕ),
                                  i < List.length t.toTensor.data →
                                    transpose_remap α n i < List.length t.toTensor.data))
                            (transpose_remap n α)
                            (_ :
                              ∀ (n_1 : ℕ),
                                n_1 <
                                    List.length
                                      (List.remap t.toTensor.data (transpose_remap α n)
                                        (_ :
                                          ∀ (i : ℕ),
                                            i < List.length t.toTensor.data →
                                              transpose_remap α n i < List.length t.toTensor.data)) →
                                  transpose_remap n α n_1 <
                                    List.length
                                      (List.remap t.toTensor.data (transpose_remap α n)
                                        (_ :
                                          ∀ (i : ℕ),
                                            i < List.length t.toTensor.data →
                                              transpose_remap α n i < List.length t.toTensor.data)))) =
                        shapeProd [α, n]) }.shape
              [MLIR.AST.Dimension.Known α, MLIR.AST.Dimension.Known n] =
            true) } =
    t

State before:
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ {
      toTensor :=
        { shape := [α, n],
          data :=
            List.remap
              (List.remap t.toTensor.data (transpose_remap α n)
                (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
              (transpose_remap n α)
              (_ :
                ∀ (n_1 : ℕ),
                  n_1 <
                      List.length
                        (List.remap t.toTensor.data (transpose_remap α n)
                          (_ :
                            ∀ (i : ℕ),
                              i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
                    transpose_remap n α n_1 <
                      List.length
                        (List.remap t.toTensor.data (transpose_remap α n)
                          (_ :
                            ∀ (i : ℕ),
                              i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))),
          h_data_size :=
            (_ :
              List.length
                  (List.remap
                    (List.remap t.toTensor.data (transpose_remap α n)
                      (_ :
                        ∀ (i : ℕ),
                          i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
                    (transpose_remap n α)
                    (_ :
                      ∀ (n_1 : ℕ),
                        n_1 <
                            List.length
                              (List.remap t.toTensor.data (transpose_remap α n)
                                (_ :
                                  ∀ (i : ℕ),
                                    i < List.length t.toTensor.data →
                                      transpose_remap α n i < List.length t.toTensor.data)) →
                          transpose_remap n α n_1 <
                            List.length
                              (List.remap t.toTensor.data (transpose_remap α n)
                                (_ :
                                  ∀ (i : ℕ),
                                    i < List.length t.toTensor.data →
                                      transpose_remap α n i < List.length t.toTensor.data)))) =
                shapeProd [α, n]) },
      h_refines :=
        (_ :
          shapeRefines
              { shape := [α, n],
                  data :=
                    List.remap
                      (List.remap t.toTensor.data (transpose_remap α n)
                        (_ :
                          ∀ (i : ℕ),
                            i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
                      (transpose_remap n α)
                      (_ :
                        ∀ (n_1 : ℕ),
                          n_1 <
                              List.length
                                (List.remap t.toTensor.data (transpose_remap α n)
                                  (_ :
                                    ∀ (i : ℕ),
                                      i < List.length t.toTensor.data →
                                        transpose_remap α n i < List.length t.toTensor.data)) →
                            transpose_remap n α n_1 <
                              List.length
                                (List.remap t.toTensor.data (transpose_remap α n)
                                  (_ :
                                    ∀ (i : ℕ),
                                      i < List.length t.toTensor.data →
                                        transpose_remap α n i < List.length t.toTensor.data))),
                  h_data_size :=
                    (_ :
                      List.length
                          (List.remap
                            (List.remap t.toTensor.data (transpose_remap α n)
                              (_ :
                                ∀ (i : ℕ),
                                  i < List.length t.toTensor.data →
                                    transpose_remap α n i < List.length t.toTensor.data))
                            (transpose_remap n α)
                            (_ :
                              ∀ (n_1 : ℕ),
                                n_1 <
                                    List.length
                                      (List.remap t.toTensor.data (transpose_remap α n)
                                        (_ :
                                          ∀ (i : ℕ),
                                            i < List.length t.toTensor.data →
                                              transpose_remap α n i < List.length t.toTensor.data)) →
                                  transpose_remap n α n_1 <
                                    List.length
                                      (List.remap t.toTensor.data (transpose_remap α n)
                                        (_ :
                                          ∀ (i : ℕ),
                                            i < List.length t.toTensor.data →
                                              transpose_remap α n i < List.length t.toTensor.data)))) =
                        shapeProd [α, n]) }.shape
              [MLIR.AST.Dimension.Known α, MLIR.AST.Dimension.Known n] =
            true) } =
    t
Tactic:
apply RankedTensor.eq_of_fields_eq <;> simp
State after:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ [α, n] = t.toTensor.shape

case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data

State before:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ [α, n] = t.toTensor.shape

case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
Tactic:
. rw [←dim_known_project_eq _ t.h_refines] <;> simp
State after:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data

State before:
case a
α n : ℕ
m : MLIR.AST.MLIRTy
t : Matrix α n m
⊢ List.remap
      (List.remap t.toTensor.data (transpose_remap α n)
        (_ : ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))
      (transpose_remap n α)
      (_ :
        ∀ (n_1 : ℕ),
          n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ), i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data)) →
            transpose_remap n α n_1 <
              List.length
                (List.remap t.toTensor.data (transpose_remap α n)
                  (_ :
                    ∀ (i : ℕ),
                      i < List.length t.toTensor.data → transpose_remap α n i < List.length t.toTensor.data))) =
    t.toTensor.data
Tactic:
. simp [List.remap_remap]
  apply List.extF <;> simp
  simp [transpose_remap_involutive]
State after:
no goals