Theorem: double_transpose_correct
Proof 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]
Proof 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 })])