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

State before:
n : ℕ
r : Region scf
⊢ run ⟦ LHS r ⟧ (INPUT n) = run ⟦ RHS r ⟧ (INPUT n)
Tactic:
simp[LHS, RHS]
State after:
n : ℕ
r : Region scf
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        [])
      (INPUT n) =
    run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
            Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        [])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        [])
      (INPUT n) =
    run
      (denoteRegion scf
        (Region.mk "entry" []
          [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
            Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        [])
      (INPUT n)
Tactic:
simp[run_denoteRegion]
State after:
n : ℕ
r : Region scf
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
                (AttrDict.mk [])])
      (INPUT n) =
    run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
              Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
                [r] (AttrDict.mk [])])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
                (AttrDict.mk [])])
      (INPUT n) =
    run
      (do
        denoteTypedArgs [] []
        denoteOps scf
            [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
              Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
                [r] (AttrDict.mk [])])
      (INPUT n)
Tactic:
simp[run_bind]
State after:
n : ℕ
r : Region scf
⊢ (match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
            Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e

State before:
n : ℕ
r : Region scf
⊢ (match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    match run (denoteTypedArgs [] []) (INPUT n) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
            Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e
Tactic:
simp[run_denoteTypedArgs_nil]
State after:
n : ℕ
r : Region scf
⊢ run
      (denoteOps scf
        [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ run
      (denoteOps scf
        [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)
Tactic:
simp[run_denoteOps_singleton]
State after:
n : ℕ
r : Region scf
⊢ run
      (denoteOp scf
        (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
          (AttrDict.mk [])))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ run
      (denoteOp scf
        (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
          (AttrDict.mk [])))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)
Tactic:
simp[run_denoteOp]
State after:
n : ℕ
r : Region scf
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ run
      (do
        let args ← denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
        OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (INPUT n) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)
Tactic:
simp[run_bind]
State after:
n : ℕ
r : Region scf
⊢ (match
      run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
        (INPUT n) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)

State before:
n : ℕ
r : Region scf
⊢ (match
      run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
        (INPUT n) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (INPUT n)
Tactic:
simp[INPUT]
State after:
n : ℕ
r : Region scf
⊢ (match
      run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

State before:
n : ℕ
r : Region scf
⊢ (match
      run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))
Tactic:
simp[run_denoteOpArgs_cons_]
State after:
n : ℕ
r : Region scf
⊢ (match
      run
        (do
          let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c0")
          let xs ← denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
          pure ({ fst := MLIRType.index, snd := x } :: xs))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

State before:
n : ℕ
r : Region scf
⊢ (match
      run
        (do
          let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c0")
          let xs ← denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
          pure ({ fst := MLIRType.index, snd := x } :: xs))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))
Tactic:
simp[run_bind]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        run (TopM.get MLIRType.index (SSAVal.SSAVal "c0"))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        run (TopM.get MLIRType.index (SSAVal.SSAVal "c0"))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))
Tactic:
rw[run_TopM_get_]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))
Tactic:
rw[SSAEnv.get_set_ne_val]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_ne_val]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        Except.ok
          (match
              SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)) with
            | some v => v
            | none => default,
            SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
        | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_eq_val] <;> simp
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOpArgs_cons_]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "cn_plus_1")
            let xs ← denoteOpArgs scf []
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "cn_plus_1")
            let xs ← denoteOpArgs scf []
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_bind]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (TopM.get MLIRType.index (SSAVal.SSAVal "cn_plus_1"))
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (TopM.get MLIRType.index (SSAVal.SSAVal "cn_plus_1"))
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[run_TopM_get_]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "cn_plus_1") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                    (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                      (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                        (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "cn_plus_1") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                    (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                      (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                        (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_ne_val]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "cn_plus_1") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "cn_plus_1") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, snd := a } :: a_1)) env'
          | Except.error e => Except.error e
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_eq_val] <;> simp
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (denoteOpArgs scf [])
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := ↑n + 1 } :: a)) env'
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (denoteOpArgs scf [])
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := ↑n + 1 } :: a)) env'
        | Except.error e => Except.error e with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOpArgs_nil]
State after:
n : ℕ
r : Region scf
⊢ (match
      match
        run (pure [{ fst := MLIRType.index, snd := ↑n + 1 }])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ (match
      match
        run (pure [{ fst := MLIRType.index, snd := ↑n + 1 }])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_pure]
State after:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r])
        (Semantics.semantics_op
          (IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM (TopM.mapDenoteRegion scf [r])
        (Semantics.semantics_op
          (IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[TopM.mapDenoteRegion]
State after:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (Semantics.semantics_op
          (IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (Semantics.semantics_op
          (IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[Semantics.semantics_op, scf_semantics_op]
State after:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (match
          IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []) with
        | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
          ite (b = 1) rthen relse []
        |
        IOp.mk "scf.for" resTy
            [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
              { fst := MLIRType.index, snd := step }]
            [body] attrs =>
          do
          let _ ←
            run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                body [{ fst := MLIRType.index, snd := i }]
          pure []
        |
        IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
            attrs =>
          run_loop_bounded (Int.toNat (hi - lo)) lo [] body
        | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
        | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
          if arg = 0 then
            OpM.Error
              (toString "" ++
                      toString
                        (match AttrDict.find attrs "msg" with
                        | some (AttrValue.str str) => str
                        | x => "") ++
                    toString ": " ++
                  toString arg ++
                toString " <assert failed>")
          else pure []
        | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
        | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (match
          IOp.mk "scf.for'" [] [{ fst := MLIRType.index, snd := 0 }, { fst := MLIRType.index, snd := ↑n + 1 }]
            (OpM.denoteRegions [r] 0) (AttrDict.mk []) with
        | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
          ite (b = 1) rthen relse []
        |
        IOp.mk "scf.for" resTy
            [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
              { fst := MLIRType.index, snd := step }]
            [body] attrs =>
          do
          let _ ←
            run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                body [{ fst := MLIRType.index, snd := i }]
          pure []
        |
        IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
            attrs =>
          run_loop_bounded (Int.toNat (hi - lo)) lo [] body
        | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
        | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
          if arg = 0 then
            OpM.Error
              (toString "" ++
                      toString
                        (match AttrDict.find attrs "msg" with
                        | some (AttrValue.str str) => str
                        | x => "") ++
                    toString ": " ++
                  toString arg ++
                toString " <assert failed>")
          else pure []
        | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
        | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[OpM.denoteRegions]
State after:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
n : ℕ
r : Region scf
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
apply Eq.symm
State after:
case h
n : ℕ
r : Region scf
⊢ run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ run
      (denoteOps scf
        [Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []),
          Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOps_cons]
State after:
case h
n : ℕ
r : Region scf
⊢ run
      (do
        let _ ← denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []))
        denoteOps scf
            [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
                (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ run
      (do
        let _ ← denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk []))
        denoteOps scf
            [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
                (AttrDict.mk [])])
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_bind]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run (denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk [])))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run (denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk [])))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (denoteOps scf
          [Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
              (AttrDict.mk [])])
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOps_singleton]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run (denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk [])))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (denoteOp scf
          (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])))
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run (denoteOp scf (Op.mk "scf.execute_region" [] [(SSAVal.SSAVal "c0", MLIRType.index)] [r] (AttrDict.mk [])))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (denoteOp scf
          (Op.mk "scf.for'" [] [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)] [r]
            (AttrDict.mk [])))
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOp]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (do
          let args ← denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index)]
          OpM.toTopM (TopM.mapDenoteRegion scf [r])
              (Semantics.semantics_op (IOp.mk "scf.execute_region" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (do
          let args ←
            denoteOpArgs scf [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
          OpM.toTopM (TopM.mapDenoteRegion scf [r])
              (Semantics.semantics_op (IOp.mk "scf.for'" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (do
          let args ← denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index)]
          OpM.toTopM (TopM.mapDenoteRegion scf [r])
              (Semantics.semantics_op (IOp.mk "scf.execute_region" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      run
        (do
          let args ←
            denoteOpArgs scf [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
          OpM.toTopM (TopM.mapDenoteRegion scf [r])
              (Semantics.semantics_op (IOp.mk "scf.for'" [] args (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
        env'
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_bind]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index)])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
          env' with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "c0", MLIRType.index)])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        run (denoteOpArgs scf [(SSAVal.SSAVal "c1", MLIRType.index), (SSAVal.SSAVal "cn_plus_1", MLIRType.index)])
          env' with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOpArgs_cons_]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c0")
            let xs ← denoteOpArgs scf []
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c1")
            let xs ← denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          env' with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c0")
            let xs ← denoteOpArgs scf []
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        run
          (do
            let x ← TopM.get MLIRType.index (SSAVal.SSAVal "c1")
            let xs ← denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]
            pure ({ fst := MLIRType.index, snd := x } :: xs))
          env' with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_bind]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (TopM.get MLIRType.index (SSAVal.SSAVal "c0"))
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (TopM.get MLIRType.index (SSAVal.SSAVal "c0"))
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[run_TopM_get_]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                    (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                      (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                        (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                    (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                      (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                        (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_ne_val]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                    (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                      (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_ne_val]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                SSAEnv.get (SSAVal.SSAVal "c0") MLIRType.index
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)) with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
rw[SSAEnv.get_set_eq_val]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                if H' : MLIRType.index = MLIRType.index then
                  some
                    (cast
                      (_ :
                        (match MLIRType.index with
                          | MLIRType.float a => Float
                          | MLIRType.int signedness sz => FinInt sz
                          | MLIRType.tensor1d => Tensor1D
                          | MLIRType.tensor2d => Tensor2D
                          | MLIRType.tensor4d => Tensor4D
                          | MLIRType.index => ℤ
                          | MLIRType.undefined a => Unit
                          | MLIRType.extended σ => Unit
                          | MLIRType.erased => Unit) =
                          match MLIRType.index with
                          | MLIRType.float a => Float
                          | MLIRType.int signedness sz => FinInt sz
                          | MLIRType.tensor1d => Tensor1D
                          | MLIRType.tensor2d => Tensor2D
                          | MLIRType.tensor4d => Tensor4D
                          | MLIRType.index => ℤ
                          | MLIRType.undefined a => Unit
                          | MLIRType.extended σ => Unit
                          | MLIRType.erased => Unit)
                      0)
                else none with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          Except.ok
            (match
                if H' : MLIRType.index = MLIRType.index then
                  some
                    (cast
                      (_ :
                        (match MLIRType.index with
                          | MLIRType.float a => Float
                          | MLIRType.int signedness sz => FinInt sz
                          | MLIRType.tensor1d => Tensor1D
                          | MLIRType.tensor2d => Tensor2D
                          | MLIRType.tensor4d => Tensor4D
                          | MLIRType.index => ℤ
                          | MLIRType.undefined a => Unit
                          | MLIRType.extended σ => Unit
                          | MLIRType.erased => Unit) =
                          match MLIRType.index with
                          | MLIRType.float a => Float
                          | MLIRType.int signedness sz => FinInt sz
                          | MLIRType.tensor1d => Tensor1D
                          | MLIRType.tensor2d => Tensor2D
                          | MLIRType.tensor4d => Tensor4D
                          | MLIRType.index => ℤ
                          | MLIRType.undefined a => Unit
                          | MLIRType.extended σ => Unit
                          | MLIRType.erased => Unit)
                      0)
                else none with
              | some v => v
              | none => default,
              SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
                (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                  (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                    (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf []) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (denoteOpArgs scf [])
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
        | Except.error e => Except.error e with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        match
          run (denoteOpArgs scf [])
            (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
              (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
                (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                  (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
        | Except.ok (a, env') => run (pure ({ fst := MLIRType.index, snd := 0 } :: a)) env'
        | Except.error e => Except.error e with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_denoteOpArgs_nil]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run (pure [{ fst := MLIRType.index, snd := 0 }])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      match
        run (pure [{ fst := MLIRType.index, snd := 0 }])
          (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
            (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
              (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
                (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
      | Except.ok (a, env') =>
        run
          (OpM.toTopM (TopM.mapDenoteRegion scf [r])
            (Semantics.semantics_op (IOp.mk "scf.execute_region" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => run (pure ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_pure]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM (TopM.mapDenoteRegion scf [r])
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[TopM_mapDenoteRegion_cons]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM (TopM.scoped ∘ denoteRegion scf r :: TopM.mapDenoteRegion scf [])
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r :: TopM.mapDenoteRegion scf [])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM (TopM.scoped ∘ denoteRegion scf r :: TopM.mapDenoteRegion scf [])
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r :: TopM.mapDenoteRegion scf [])
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[TopM_mapDenoteRegion_nil]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (Semantics.semantics_op
            (IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []))))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (Semantics.semantics_op (IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []))))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[Semantics.semantics_op, scf_semantics_op]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (match
            IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []) with
          | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
            ite (b = 1) rthen relse []
          |
          IOp.mk "scf.for" resTy
              [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                { fst := MLIRType.index, snd := step }]
              [body] attrs =>
            do
            let _ ←
              run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                  body [{ fst := MLIRType.index, snd := i }]
            pure []
          |
          IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
              attrs =>
            run_loop_bounded (Int.toNat (hi - lo)) lo [] body
          | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
          | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
            if arg = 0 then
              OpM.Error
                (toString "" ++
                        toString
                          (match AttrDict.find attrs "msg" with
                          | some (AttrValue.str str) => str
                          | x => "") ++
                      toString ": " ++
                    toString arg ++
                  toString " <assert failed>")
            else pure []
          | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
          | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (match
            IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }] (OpM.denoteRegions [r] 0)
              (AttrDict.mk []) with
          | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
            ite (b = 1) rthen relse []
          |
          IOp.mk "scf.for" resTy
              [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                { fst := MLIRType.index, snd := step }]
              [body] attrs =>
            do
            let _ ←
              run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                  body [{ fst := MLIRType.index, snd := i }]
            pure []
          |
          IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
              attrs =>
            run_loop_bounded (Int.toNat (hi - lo)) lo [] body
          | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
          | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
            if arg = 0 then
              OpM.Error
                (toString "" ++
                        toString
                          (match AttrDict.find attrs "msg" with
                          | some (AttrValue.str str) => str
                          | x => "") ++
                      toString ": " ++
                    toString arg ++
                  toString " <assert failed>")
            else pure []
          | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
          | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a (OpM.denoteRegions [r] 0) (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[OpM_denoteRegions_cons]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (match
            IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }]
              (OpM.denoteRegion r 0 :: OpM.denoteRegions [] 1) (AttrDict.mk []) with
          | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
            ite (b = 1) rthen relse []
          |
          IOp.mk "scf.for" resTy
              [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                { fst := MLIRType.index, snd := step }]
              [body] attrs =>
            do
            let _ ←
              run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                  body [{ fst := MLIRType.index, snd := i }]
            pure []
          |
          IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
              attrs =>
            run_loop_bounded (Int.toNat (hi - lo)) lo [] body
          | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
          | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
            if arg = 0 then
              OpM.Error
                (toString "" ++
                        toString
                          (match AttrDict.find attrs "msg" with
                          | some (AttrValue.str str) => str
                          | x => "") ++
                      toString ": " ++
                    toString arg ++
                  toString " <assert failed>")
            else pure []
          | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
          | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a (OpM.denoteRegion r 0 :: OpM.denoteRegions [] 1) (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run
        (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
          (match
            IOp.mk "scf.execute_region" [] [{ fst := MLIRType.index, snd := 0 }]
              (OpM.denoteRegion r 0 :: OpM.denoteRegions [] 1) (AttrDict.mk []) with
          | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
            ite (b = 1) rthen relse []
          |
          IOp.mk "scf.for" resTy
              [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                { fst := MLIRType.index, snd := step }]
              [body] attrs =>
            do
            let _ ←
              run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                  body [{ fst := MLIRType.index, snd := i }]
            pure []
          |
          IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
              attrs =>
            run_loop_bounded (Int.toNat (hi - lo)) lo [] body
          | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
          | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
            if arg = 0 then
              OpM.Error
                (toString "" ++
                        toString
                          (match AttrDict.find attrs "msg" with
                          | some (AttrValue.str str) => str
                          | x => "") ++
                      toString ": " ++
                    toString arg ++
                  toString " <assert failed>")
            else pure []
          | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
          | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a (OpM.denoteRegion r 0 :: OpM.denoteRegions [] 1) (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[OpM_denoteRegions_nil]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r] (OpM.denoteRegion r 0 [{ fst := MLIRType.index, snd := 0 }]))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r] (OpM.denoteRegion r 0 [{ fst := MLIRType.index, snd := 0 }]))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_OpM_toTopM_denoteRegion]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r] 0 [{ fst := MLIRType.index, snd := 0 }])
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r] 0 [{ fst := MLIRType.index, snd := 0 }])
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp[run_TopM_denoteRegionsByIx_cons]
State after:
case h
n : ℕ
r : Region scf
⊢ (match
      run (TopM.scoped (denoteRegion scf r [{ fst := MLIRType.index, snd := 0 }]))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h
n : ℕ
r : Region scf
⊢ (match
      run (TopM.scoped (denoteRegion scf r [{ fst := MLIRType.index, snd := 0 }]))
        (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
          (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
            (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
              (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty)))) with
    | Except.ok (a, env') =>
      match
        match run (TopM.get MLIRType.index (SSAVal.SSAVal "c1")) env' with
        | Except.ok (a, env') =>
          match run (denoteOpArgs scf [(SSAVal.SSAVal "cn_plus_1", MLIRType.index)]) env' with
          | Except.ok (a_1, env') => Except.ok ({ fst := MLIRType.index, 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.scoped ∘ denoteRegion scf r]
            (match IOp.mk "scf.for'" [] a [OpM.denoteRegion r 0] (AttrDict.mk []) with
            | IOp.mk "scf.if" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := b }] [rthen, relse] attrs =>
              ite (b = 1) rthen relse []
            |
            IOp.mk "scf.for" resTy
                [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi },
                  { fst := MLIRType.index, snd := step }]
                [body] attrs =>
              do
              let _ ←
                run_loop_bounded_stepped (Int.toNat ((hi - lo) / step)) lo step default fun i x =>
                    body [{ fst := MLIRType.index, snd := i }]
              pure []
            |
            IOp.mk "scf.for'" resTy [{ fst := MLIRType.index, snd := lo }, { fst := MLIRType.index, snd := hi }] [body]
                attrs =>
              run_loop_bounded (Int.toNat (hi - lo)) lo [] body
            | IOp.mk "scf.yield" resTy vs [] attrs => pure vs
            | IOp.mk "scf.assert" resTy [{ fst := MLIRType.int Signedness.Signless 1, snd := arg }] [] attrs =>
              if arg = 0 then
                OpM.Error
                  (toString "" ++
                          toString
                            (match AttrDict.find attrs "msg" with
                            | some (AttrValue.str str) => str
                            | x => "") ++
                        toString ": " ++
                      toString arg ++
                    toString " <assert failed>")
              else pure []
            | IOp.mk "scf.execute_region" resTy args [rgn] attrs => rgn args
            | IOp.mk name resTy args regions attrs => OpM.Unhandled ("scf unhandled: " ++ name)))
          env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r]
        (run_loop_bounded (Int.toNat (↑n + 1)) 0 [] (OpM.denoteRegion r 0)))
      (SSAEnv.set (SSAVal.SSAVal "cn") MLIRType.index (↑n)
        (SSAEnv.set (SSAVal.SSAVal "cn_plus_1") MLIRType.index (↑n + 1)
          (SSAEnv.set (SSAVal.SSAVal "c0") MLIRType.index 0
            (SSAEnv.set (SSAVal.SSAVal "c1") MLIRType.index 1 SSAEnv.empty))))

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
sorry
State after:
case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
sorry
State after:
case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case h.a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
State after:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "cn_plus_1"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
State after:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn_plus_1" ≠ SSAVal.SSAVal "c0"

case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
State after:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"

State before:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
State after:
no goals