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