internlm/Lean-Github huggingface dataset:
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
b : Bool
⊢ run
      (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂]
        (ite (b = false → False) (OpM.denoteRegion r₁ 0) (OpM.denoteRegion r₂ 1) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf (if b = true then r₁ else r₂) []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 (if b = true then 1 else 0) SSAEnv.empty)
Tactic:
cases b <;> simp
Proof state after:
case false
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)

case true
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
case false => {
  rw[OpM_toTopM_denoteRegion]; simp[TopM.denoteRegionsByIx]; }
Proof state after:
no goals
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)
Tactic:
case true => {
  sorry
  
}
Proof state after:
no goals
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₂ 1 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
rw[OpM_toTopM_denoteRegion]
Proof state after:
r₁ r₂ : Region scf
⊢ run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] 1 [])
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
⊢ run (TopM.denoteRegionsByIx [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] 1 [])
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₂ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 0 SSAEnv.empty)
Tactic:
simp[TopM.denoteRegionsByIx]
Proof state after:
no goals
Theorem: SCF.IF.equivalent
Proof state before:
r₁ r₂ : Region scf
⊢ run (OpM.toTopM [TopM.scoped ∘ denoteRegion scf r₁, TopM.scoped ∘ denoteRegion scf r₂] (OpM.denoteRegion r₁ 0 []))
      (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty) =
    run (TopM.scoped (denoteRegion scf r₁ [])) (SSAEnv.set (SSAVal.SSAVal "b") MLIRType.i1 1 SSAEnv.empty)
Tactic:
sorry
Proof state after:
no goals
Theorem: SCF.FOR_PEELING.CORRECT_r
Proof state before:
n : ℕ
r : Region scf
args : TypedArgs scf
⊢ run (denoteRegion scf r args) (INPUT n) = Except.ok ([], INPUT n)
Tactic:
sorry
Proof state after:
no goals
Theorem: SCF.FOR_PEELING.identity₁
Proof state before:
n : ℕ
⊢ Int.toNat (Int.ofNat n + 1 - 0) = n + 1
Tactic:
sorry
Proof state after:
no goals
Theorem: SCF.FOR_PEELING.equivalent
Proof state before:
n : ℕ
r : Region scf
⊢ run ⟦ LHS r ⟧ (INPUT n) = run ⟦ RHS r ⟧ (INPUT n)
Tactic:
simp[LHS, RHS]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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)
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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))))
Theorem: SCF.FOR_PEELING.equivalent
Proof 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_]
Proof 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))))
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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))))
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"