Theorem: SCF.FOR_PEELING.equivalent
Proof 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_]
Proof 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"