Theorem: double_transpose_correct (MLIR/Dialects/ToySemantics.lean)

State before:
⊢ ∀ (t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
    run_toy (toy_semantics_region double_transpose)
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
      Fitree.ret
        ((),
          SSAEnv.One
            [(SSAVal.SSAVal "t1",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
              (SSAVal.SSAVal "t2",
                { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
              (SSAVal.SSAVal "t3",
                { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])
Tactic:
intros t1
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ run_toy (toy_semantics_region double_transpose)
      (SSAEnv.One
        [(SSAVal.SSAVal "t1",
            { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ run_toy (toy_semantics_region double_transpose)
      (SSAEnv.One
        [(SSAVal.SSAVal "t1",
            { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })]) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := builtin.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32, snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := builtin.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32, snd := t1 })])
Tactic:
simp [double_transpose, toy_semantics_region, toy_semantics_op]
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (interpUB'!
          (Fitree.bind
            (match
              Op.mk "toy.transpose"
                [(SSAVal.SSAVal "t2",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))]
                [(SSAVal.SSAVal "t1",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))]
                [] (AttrDict.mk []) with
            | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
              match AttrDict.find attrs "value" with
              | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                | none =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t1",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")
                | some t_lit =>
                  Fitree.bind (Fitree.trigger (ToyOp.Constant D₁ τ₁ t_lit)) fun t =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) (some res) t
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
              match D with
              | [Dimension.Known n, Dimension.Known m] =>
                Fitree.bind
                  (Fitree.trigger
                    (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                      t_name))
                  fun t =>
                  Fitree.bind (Fitree.trigger (ToyOp.Transpose τ n m t)) fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ))
                      (some res) t'
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            |
            Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
              if h : τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                Fitree.bind (Fitree.trigger (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)) fun t =>
                  Fitree.bind
                    (Fitree.trigger
                      (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                        (_ : DimList.prod D' = DimList.prod D) t))
                    fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D' τ₂)) (some res)
                      (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) t')
              else
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | x =>
              raiseUB
                (toString "" ++
                    toString
                      (Op.mk "toy.transpose"
                        [(SSAVal.SSAVal "t2",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                (MLIRType.int Signedness.Signless 32)))]
                        [(SSAVal.SSAVal "t1",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                (MLIRType.int Signedness.Signless 32)))]
                        [] (AttrDict.mk [])) ++
                  toString ""))
            fun x =>
            match
              Op.mk "toy.transpose"
                [(SSAVal.SSAVal "t3",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))]
                [(SSAVal.SSAVal "t2",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))]
                [] (AttrDict.mk []) with
            | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
              match AttrDict.find attrs "value" with
              | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                | none =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")
                | some t_lit =>
                  Fitree.bind (Fitree.trigger (ToyOp.Constant D₁ τ₁ t_lit)) fun t =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) (some res) t
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
              match D with
              | [Dimension.Known n, Dimension.Known m] =>
                Fitree.bind
                  (Fitree.trigger
                    (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                      t_name))
                  fun t =>
                  Fitree.bind (Fitree.trigger (ToyOp.Transpose τ n m t)) fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ))
                      (some res) t'
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            |
            Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
              if h : τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                Fitree.bind (Fitree.trigger (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)) fun t =>
                  Fitree.bind
                    (Fitree.trigger
                      (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                        (_ : DimList.prod D' = DimList.prod D) t))
                    fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D' τ₂)) (some res)
                      (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) t')
              else
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | x =>
              raiseUB
                (toString "" ++
                    toString
                      (Op.mk "toy.transpose"
                        [(SSAVal.SSAVal "t3",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                (MLIRType.int Signedness.Signless 32)))]
                        [(SSAVal.SSAVal "t2",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                (MLIRType.int Signedness.Signless 32)))]
                        [] (AttrDict.mk [])) ++
                  toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (interpUB'!
          (Fitree.bind
            (match
              Op.mk "toy.transpose"
                [(SSAVal.SSAVal "t2",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))]
                [(SSAVal.SSAVal "t1",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))]
                [] (AttrDict.mk []) with
            | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
              match AttrDict.find attrs "value" with
              | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                | none =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t1",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")
                | some t_lit =>
                  Fitree.bind (Fitree.trigger (ToyOp.Constant D₁ τ₁ t_lit)) fun t =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) (some res) t
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
              match D with
              | [Dimension.Known n, Dimension.Known m] =>
                Fitree.bind
                  (Fitree.trigger
                    (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                      t_name))
                  fun t =>
                  Fitree.bind (Fitree.trigger (ToyOp.Transpose τ n m t)) fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ))
                      (some res) t'
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            |
            Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
              if h : τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                Fitree.bind (Fitree.trigger (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)) fun t =>
                  Fitree.bind
                    (Fitree.trigger
                      (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                        (_ : DimList.prod D' = DimList.prod D) t))
                    fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D' τ₂)) (some res)
                      (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) t')
              else
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t1",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | x =>
              raiseUB
                (toString "" ++
                    toString
                      (Op.mk "toy.transpose"
                        [(SSAVal.SSAVal "t2",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                (MLIRType.int Signedness.Signless 32)))]
                        [(SSAVal.SSAVal "t1",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                (MLIRType.int Signedness.Signless 32)))]
                        [] (AttrDict.mk [])) ++
                  toString ""))
            fun x =>
            match
              Op.mk "toy.transpose"
                [(SSAVal.SSAVal "t3",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))]
                [(SSAVal.SSAVal "t2",
                    MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))]
                [] (AttrDict.mk []) with
            | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
              match AttrDict.find attrs "value" with
              | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                | none =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")
                | some t_lit =>
                  Fitree.bind (Fitree.trigger (ToyOp.Constant D₁ τ₁ t_lit)) fun t =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) (some res) t
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
              match D with
              | [Dimension.Known n, Dimension.Known m] =>
                Fitree.bind
                  (Fitree.trigger
                    (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                      t_name))
                  fun t =>
                  Fitree.bind (Fitree.trigger (ToyOp.Transpose τ n m t)) fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ))
                      (some res) t'
              | x =>
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            |
            Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
              if h : τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                Fitree.bind (Fitree.trigger (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)) fun t =>
                  Fitree.bind
                    (Fitree.trigger
                      (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                        (_ : DimList.prod D' = DimList.prod D) t))
                    fun t' =>
                    SSAEnv.set? (MLIRType.extended (builtin.σ.tensor D' τ₂)) (some res)
                      (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) t')
              else
                raiseUB
                  (toString "" ++
                      toString
                        (Op.mk "toy.transpose"
                          [(SSAVal.SSAVal "t3",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [(SSAVal.SSAVal "t2",
                              MLIRType.extended
                                (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                  (MLIRType.int Signedness.Signless 32)))]
                          [] (AttrDict.mk [])) ++
                    toString "")
            | x =>
              raiseUB
                (toString "" ++
                    toString
                      (Op.mk "toy.transpose"
                        [(SSAVal.SSAVal "t3",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                (MLIRType.int Signedness.Signless 32)))]
                        [(SSAVal.SSAVal "t2",
                            MLIRType.extended
                              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                (MLIRType.int Signedness.Signless 32)))]
                        [] (AttrDict.mk [])) ++
                  toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp_itree
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (interpUB'!
          (Fitree.Vis
            (Sum.inr
              (Sum.inl
                (SSAEnvE.Get
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  (SSAVal.SSAVal "t1"))))
            fun r =>
            Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 r))) fun r =>
              Fitree.Vis
                (Sum.inr
                  (Sum.inl
                    (SSAEnvE.Set
                      (MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                      (SSAVal.SSAVal "t2") r)))
                fun r =>
                match
                  Op.mk "toy.transpose"
                    [(SSAVal.SSAVal "t3",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                            (MLIRType.int Signedness.Signless 32)))]
                    [(SSAVal.SSAVal "t2",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                            (MLIRType.int Signedness.Signless 32)))]
                    [] (AttrDict.mk []) with
                | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
                  match AttrDict.find attrs "value" with
                  | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                    match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                    | none =>
                      raiseUB
                        (toString "" ++
                            toString
                              (Op.mk "toy.transpose"
                                [(SSAVal.SSAVal "t3",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [(SSAVal.SSAVal "t2",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [] (AttrDict.mk [])) ++
                          toString "")
                    | some t_lit =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Constant D₁ τ₁ t_lit))) fun r =>
                        Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
                  match D with
                  | [Dimension.Known n, Dimension.Known m] =>
                    Fitree.Vis
                      (Sum.inr
                        (Sum.inl
                          (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                            t_name)))
                      fun r =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose τ n m r))) fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set
                                (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                |
                Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                    [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
                  if h :
                      τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                    Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)))
                      fun r =>
                      Fitree.Vis
                        (Sum.inr
                          (Sum.inr
                            (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                              (_ : DimList.prod D' = DimList.prod D) r)))
                        fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D' τ₂)) res
                                (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) r))))
                          Fitree.Ret
                  else
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | x =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (interpUB'!
          (Fitree.Vis
            (Sum.inr
              (Sum.inl
                (SSAEnvE.Get
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  (SSAVal.SSAVal "t1"))))
            fun r =>
            Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 r))) fun r =>
              Fitree.Vis
                (Sum.inr
                  (Sum.inl
                    (SSAEnvE.Set
                      (MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                      (SSAVal.SSAVal "t2") r)))
                fun r =>
                match
                  Op.mk "toy.transpose"
                    [(SSAVal.SSAVal "t3",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                            (MLIRType.int Signedness.Signless 32)))]
                    [(SSAVal.SSAVal "t2",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                            (MLIRType.int Signedness.Signless 32)))]
                    [] (AttrDict.mk []) with
                | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
                  match AttrDict.find attrs "value" with
                  | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                    match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                    | none =>
                      raiseUB
                        (toString "" ++
                            toString
                              (Op.mk "toy.transpose"
                                [(SSAVal.SSAVal "t3",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [(SSAVal.SSAVal "t2",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [] (AttrDict.mk [])) ++
                          toString "")
                    | some t_lit =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Constant D₁ τ₁ t_lit))) fun r =>
                        Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
                  match D with
                  | [Dimension.Known n, Dimension.Known m] =>
                    Fitree.Vis
                      (Sum.inr
                        (Sum.inl
                          (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                            t_name)))
                      fun r =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose τ n m r))) fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set
                                (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                |
                Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                    [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
                  if h :
                      τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                    Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)))
                      fun r =>
                      Fitree.Vis
                        (Sum.inr
                          (Sum.inr
                            (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                              (_ : DimList.prod D' = DimList.prod D) r)))
                        fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D' τ₂)) res
                                (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) r))))
                          Fitree.Ret
                  else
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | x =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp [interpUB'!]
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (Fitree.bind
          (Fitree.trigger
            (Sum.inl
              (SSAEnvE.Get
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                (SSAVal.SSAVal "t1"))))
          fun x =>
          Fitree.bind (Fitree.trigger (Sum.inr (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x))) fun x =>
            Fitree.bind
              (Fitree.trigger
                (Sum.inl
                  (SSAEnvE.Set
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    (SSAVal.SSAVal "t2") x)))
              fun x =>
              Fitree.interp (Fitree.case UBE.handle! fun T => Fitree.trigger)
                (match
                  Op.mk "toy.transpose"
                    [(SSAVal.SSAVal "t3",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                            (MLIRType.int Signedness.Signless 32)))]
                    [(SSAVal.SSAVal "t2",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                            (MLIRType.int Signedness.Signless 32)))]
                    [] (AttrDict.mk []) with
                | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
                  match AttrDict.find attrs "value" with
                  | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                    match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                    | none =>
                      raiseUB
                        (toString "" ++
                            toString
                              (Op.mk "toy.transpose"
                                [(SSAVal.SSAVal "t3",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [(SSAVal.SSAVal "t2",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [] (AttrDict.mk [])) ++
                          toString "")
                    | some t_lit =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Constant D₁ τ₁ t_lit))) fun r =>
                        Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
                  match D with
                  | [Dimension.Known n, Dimension.Known m] =>
                    Fitree.Vis
                      (Sum.inr
                        (Sum.inl
                          (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                            t_name)))
                      fun r =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose τ n m r))) fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set
                                (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                |
                Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                    [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
                  if h :
                      τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                    Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)))
                      fun r =>
                      Fitree.Vis
                        (Sum.inr
                          (Sum.inr
                            (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                              (_ : DimList.prod D' = DimList.prod D) r)))
                        fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D' τ₂)) res
                                (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) r))))
                          Fitree.Ret
                  else
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | x =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (interpSSA'
        (Fitree.bind
          (Fitree.trigger
            (Sum.inl
              (SSAEnvE.Get
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                (SSAVal.SSAVal "t1"))))
          fun x =>
          Fitree.bind (Fitree.trigger (Sum.inr (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x))) fun x =>
            Fitree.bind
              (Fitree.trigger
                (Sum.inl
                  (SSAEnvE.Set
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    (SSAVal.SSAVal "t2") x)))
              fun x =>
              Fitree.interp (Fitree.case UBE.handle! fun T => Fitree.trigger)
                (match
                  Op.mk "toy.transpose"
                    [(SSAVal.SSAVal "t3",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                            (MLIRType.int Signedness.Signless 32)))]
                    [(SSAVal.SSAVal "t2",
                        MLIRType.extended
                          (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                            (MLIRType.int Signedness.Signless 32)))]
                    [] (AttrDict.mk []) with
                | Op.mk "toy.constant" [(res, MLIRType.extended (Sum.inl (Sum.inl (D₁, τ₁))))] [] [] attrs =>
                  match AttrDict.find attrs "value" with
                  | some (AttrValue.extended { elem := elem, τ_sig := Sum.inl (Sum.inl (D₂, τ₂)) }) =>
                    match TensorLiteral.ofTensorElem elem D₁ τ₁ with
                    | none =>
                      raiseUB
                        (toString "" ++
                            toString
                              (Op.mk "toy.transpose"
                                [(SSAVal.SSAVal "t3",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [(SSAVal.SSAVal "t2",
                                    MLIRType.extended
                                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                        (MLIRType.int Signedness.Signless 32)))]
                                [] (AttrDict.mk [])) ++
                          toString "")
                    | some t_lit =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Constant D₁ τ₁ t_lit))) fun r =>
                        Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D₁ τ₁)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | Op.mk "toy.transpose" [(res, τ₂)] [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ))))] [] attrs =>
                  match D with
                  | [Dimension.Known n, Dimension.Known m] =>
                    Fitree.Vis
                      (Sum.inr
                        (Sum.inl
                          (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor [Dimension.Known n, Dimension.Known m] τ))
                            t_name)))
                      fun r =>
                      Fitree.Vis (Sum.inr (Sum.inr (ToyOp.Transpose τ n m r))) fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set
                                (MLIRType.extended (builtin.σ.tensor [Dimension.Known m, Dimension.Known n] τ)) res r)))
                          Fitree.Ret
                  | x =>
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                |
                Op.mk "toy.reshape" [(res, MLIRType.extended (Sum.inl (Sum.inl (D', τ₂))))]
                    [(t_name, MLIRType.extended (Sum.inl (Sum.inl (D, τ₁))))] [] attrs =>
                  if h :
                      τ₁ = τ₂ ∧ DimList.known D = true ∧ DimList.known D' = true ∧ DimList.prod D' = DimList.prod D then
                    Fitree.Vis (Sum.inr (Sum.inl (SSAEnvE.Get (MLIRType.extended (builtin.σ.tensor D τ₁)) t_name)))
                      fun r =>
                      Fitree.Vis
                        (Sum.inr
                          (Sum.inr
                            (ToyOp.Reshape τ₁ D D' (_ : DimList.known D = true) (_ : DimList.known D' = true)
                              (_ : DimList.prod D' = DimList.prod D) r)))
                        fun r =>
                        Fitree.Vis
                          (Sum.inr
                            (Sum.inl
                              (SSAEnvE.Set (MLIRType.extended (builtin.σ.tensor D' τ₂)) res
                                (cast (_ : RankedTensor D' τ₁ = RankedTensor D' τ₂) r))))
                          Fitree.Ret
                  else
                    raiseUB
                      (toString "" ++
                          toString
                            (Op.mk "toy.transpose"
                              [(SSAVal.SSAVal "t3",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [(SSAVal.SSAVal "t2",
                                  MLIRType.extended
                                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                      (MLIRType.int Signedness.Signless 32)))]
                              [] (AttrDict.mk [])) ++
                        toString "")
                | x =>
                  raiseUB
                    (toString "" ++
                        toString
                          (Op.mk "toy.transpose"
                            [(SSAVal.SSAVal "t3",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [(SSAVal.SSAVal "t2",
                                MLIRType.extended
                                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2]
                                    (MLIRType.int Signedness.Signless 32)))]
                            [] (AttrDict.mk [])) ++
                      toString "")))
        (SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp_itree
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              interpSSA' (Fitree.Ret ())
                (SSAEnv.set (SSAVal.SSAVal "t3")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              interpSSA' (Fitree.Ret ())
                (SSAEnv.set (SSAVal.SSAVal "t3")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp [interpSSA', Fitree.interpState, SSAEnvE.handle]
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              Fitree.interp
                (Fitree.case
                  (fun x e env =>
                    match x, e with
                    | .(MLIRType.eval τ), SSAEnvE.Get τ name =>
                      match SSAEnv.get name τ env with
                      | some v => Fitree.ret (v, env)
                      | none => Fitree.ret (default, env)
                    | .(Unit), SSAEnvE.Set τ name v => Fitree.ret ((), SSAEnv.set name τ v env))
                  Fitree.liftHandler)
                (Fitree.Ret ())
                (SSAEnv.set (SSAVal.SSAVal "t3")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              Fitree.interp
                (Fitree.case
                  (fun x e env =>
                    match x, e with
                    | .(MLIRType.eval τ), SSAEnvE.Get τ name =>
                      match SSAEnv.get name τ env with
                      | some v => Fitree.ret (v, env)
                      | none => Fitree.ret (default, env)
                    | .(Unit), SSAEnvE.Set τ name v => Fitree.ret ((), SSAEnv.set name τ v env))
                  Fitree.liftHandler)
                (Fitree.Ret ())
                (SSAEnv.set (SSAVal.SSAVal "t3")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                  x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp_itree
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              Fitree.Ret
                ((),
                  SSAEnv.set (SSAVal.SSAVal "t3")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                    x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ Fitree.interp ToyOp.handle
      (Fitree.bind
        (match
          SSAEnv.get (SSAVal.SSAVal "t1")
            (MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
            (SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 })]) with
        | some v =>
          Fitree.Ret
            (v,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })])
        | none =>
          Fitree.Ret
            (default,
              SSAEnv.One
                [(SSAVal.SSAVal "t1",
                    { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                      snd := t1 })]))
        fun x =>
        Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 x.fst) fun x_1 =>
          Fitree.bind
            (match
              SSAEnv.get (SSAVal.SSAVal "t2")
                (MLIRType.extended
                  (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                (SSAEnv.set (SSAVal.SSAVal "t2")
                  (MLIRType.extended
                    (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                  x_1 x.snd) with
            | some v =>
              Fitree.Ret
                (v,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd)
            | none =>
              Fitree.Ret
                (default,
                  SSAEnv.set (SSAVal.SSAVal "t2")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)))
                    x_1 x.snd))
            fun x =>
            Fitree.Vis (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x.fst) fun x_2 =>
              Fitree.Ret
                ((),
                  SSAEnv.set (SSAVal.SSAVal "t3")
                    (MLIRType.extended
                      (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)))
                    x_2 x.snd)) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp [SSAEnv.get, SSAEnv.getT, SSAEnv.set]
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ (Fitree.bind
      (ToyOp.handle (RankedTensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32))
        (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 t1))
      fun x =>
      Fitree.bind
        (ToyOp.handle (RankedTensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32))
          (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x))
        fun x_1 =>
        Fitree.ret
          ((),
            SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 }),
                (SSAVal.SSAVal "t2",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
                    snd := x }),
                (SSAVal.SSAVal "t3",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
                    snd := x_1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ (Fitree.bind
      (ToyOp.handle (RankedTensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32))
        (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 2 4 t1))
      fun x =>
      Fitree.bind
        (ToyOp.handle (RankedTensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32))
          (ToyOp.Transpose (MLIRType.int Signedness.Signless 32) 4 2 x))
        fun x_1 =>
        Fitree.ret
          ((),
            SSAEnv.One
              [(SSAVal.SSAVal "t1",
                  { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                    snd := t1 }),
                (SSAVal.SSAVal "t2",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
                    snd := x }),
                (SSAVal.SSAVal "t3",
                  {
                    fst :=
                      MLIRType.extended
                        (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
                    snd := x_1 })])) =
    Fitree.Ret
      ((),
        SSAEnv.One
          [(SSAVal.SSAVal "t1",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 }),
            (SSAVal.SSAVal "t2",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
                snd := transpose t1 }),
            (SSAVal.SSAVal "t3",
              { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32),
                snd := t1 })])
Tactic:
simp_itree
State after:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
          snd := transpose (transpose t1) })] =
    [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 })]

State before:
t1 : RankedTensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32
⊢ [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] (MLIRType.int Signedness.Signless 32)),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        {
          fst :=
            MLIRType.extended
              (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] (MLIRType.int Signedness.Signless 32)),
          snd := transpose (transpose t1) })] =
    [(SSAVal.SSAVal "t1",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 }),
      (SSAVal.SSAVal "t2",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 4, Dimension.Known 2] MLIRType.i32),
          snd := transpose t1 }),
      (SSAVal.SSAVal "t3",
        { fst := MLIRType.extended (builtin.σ.tensor [Dimension.Known 2, Dimension.Known 4] MLIRType.i32), snd := t1 })]
Tactic:
rw [transpose_involutive]
State after:
no goals