Theorem: SCF.IF.equivalent (MLIR/Dialects/ScfSemantics.lean)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run ⟦ LHS r₁ r₂ ⟧ (INPUT b) = run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[LHS]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        [])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        [])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteRegion]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
rw[run_seq]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteTypedArgs [] []) (INPUT b) with
    | Except.ok (PUnit.unit, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteTypedArgs [] []) (INPUT b) with
    | Except.ok (PUnit.unit, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteTypedArgs_nil]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOps scf
        [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOps scf
        [Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])])
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp [run_denoteOps_singleton]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOp scf
        (Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (denoteOp scf
        (Op.mk "scf.if" [] [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)] [r₁, r₂] (AttrDict.mk [])))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteOp]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
            (Semantics.semantics_op (IOp.mk "scf.if" [] args (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
            (Semantics.semantics_op (IOp.mk "scf.if" [] args (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (INPUT b) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_bind]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]) (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match run (denoteOpArgs scf [(SSAVal.SSAVal "b", MLIRType.int Signedness.Signless 1)]) (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_denoteOpArgs_cons_]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run
        (do
          let x ← TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")
          let xs ← denoteOpArgs scf []
          pure ({ fst := MLIRType.int Signedness.Signless 1, snd := x } :: xs))
        (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run
        (do
          let x ← TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")
          let xs ← denoteOpArgs scf []
          pure ({ fst := MLIRType.int Signedness.Signless 1, snd := x } :: xs))
        (INPUT b) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[run_bind]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")) (INPUT b) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b")) (INPUT b) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) [])) (INPUT b)
Tactic:
simp[INPUT]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b"))
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (TopM.get (MLIRType.int Signedness.Signless 1) (SSAVal.SSAVal "b"))
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
rw[run_TopM_get_]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "b") (MLIRType.int Signedness.Signless 1)
                (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "b") (MLIRType.int Signedness.Signless 1)
                (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf []) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := a } :: a_1)) env'
        | Except.error e => Except.error e
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[SSAEnv.get_set_eq]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (denoteOpArgs scf [])
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      match
        run (denoteOpArgs scf [])
          (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
      | Except.ok (a, env') =>
        run (pure ({ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[run_denoteOpArgs_nil]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run (pure [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }])
        (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ (match
      run (pure [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }])
        (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
          (Semantics.semantics_op (IOp.mk "scf.if" [] a (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[run_pure]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r₁, r₂])
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[TopM.mapDenoteRegion]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            (OpM.denoteRegions [r₁, r₂] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[OpM.denoteRegions]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (Semantics.semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[Semantics.semantics_op]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (scf_semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (scf_semantics_op
          (IOp.mk "scf.if" [] [{ fst := MLIRType.int Signedness.Signless 1, snd := if b = true then 1 else 0 }]
            [OpM.denoteRegion r₁ 0, OpM.denoteRegion r₂ 1] (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
simp[scf_semantics_op]
State after:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (ite (b = false → False) (OpM.denoteRegion r₁ 0) (OpM.denoteRegion r₂ 1) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)

State before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (ite (b = false → False) (OpM.denoteRegion r₁ 0) (OpM.denoteRegion r₂ 1) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
cases b <;> simp
State after:
case false
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)

case true
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)

State before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
case false => {
  rw[OpM_toTopM_denoteRegion]; simp[TopM.denoteRegionsByIx]; }
State after:
no goals

State before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)
Tactic:
case true => {
  sorry
  
}
State after:
no goals

State before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
rw[OpM_toTopM_denoteRegion]
State after:
r₁ r₂ : Region scf
⊢ run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] 1 [])
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)

State before:
r₁ r₂ : Region scf
⊢ run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] 1 [])
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
simp[TopM.denoteRegionsByIx]
State after:
no goals

State before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)
Tactic:
sorry
State after:
no goals