Theorem: SCF_SELECT.equivalent (MLIR/Examples/IfStatementOptimization.lean)

State before:
b : FinInt 1
n m : FinInt 32
⊢ run (denoteOp Δ LHS) (INPUT b n m) = run (denoteOp Δ RHS) (INPUT b n m)
Tactic:
simp [LHS, RHS, INPUT]
State after:
b : FinInt 1
n m : FinInt 32
⊢ run
      (denoteOp Δ
        (Op.mk "scf.if" [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)]
          [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
          [Region.mk "entry" []
              [Op.mk "scf.yield" [] [(SSAVal.SSAVal "n", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk [])],
            Region.mk "entry" []
              [Op.mk "scf.yield" [] [(SSAVal.SSAVal "m", MLIRType.int Signedness.Signless 32)] [] (AttrDict.mk [])]]
          (AttrDict.mk [])))
      (SSAEnv.One
        [(SSAVal.SSAVal "b", { fst := MLIRType.i1, snd := b }), (SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })]) =
    run
      (denoteOp Δ
        (Op.mk "arith.select" [(SSAVal.SSAVal "x", MLIRType.int Signedness.Signless 32)]
          [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1),
            (SSAVal.SSAVal "n", MLIRType.int Signedness.Signless 32),
            (SSAVal.SSAVal "m", MLIRType.int Signedness.Signless 32)]
          [] (AttrDict.mk [])))
      (SSAEnv.One
        [(SSAVal.SSAVal "b", { fst := MLIRType.i1, snd := b }), (SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })])