internlm/Lean-Github huggingface dataset:
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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]
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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
Proof 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"
Theorem: SCF.FOR_PEELING.equivalent
Proof 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
Proof state after:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Theorem: SCF.FOR_PEELING.equivalent
Proof state before:
case a
n : ℕ
r : Region scf
⊢ SSAVal.SSAVal "cn" ≠ SSAVal.SSAVal "c0"
Tactic:
simp
Proof state after:
no goals
Theorem: List.all_one
Proof state before:
α : Type u_1
P : α → Bool
a : α
⊢ all [a] P = true ↔ P a = true
Tactic:
simp [all, foldr]
Proof state after:
no goals
Theorem: List.ne_mem_cons
Proof state before:
α : Type u_1
x a : α
as : List α
⊢ ¬x ∈ a :: as → x ≠ a ∧ ¬x ∈ as
Tactic:
intros Hne
Proof state after:
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
⊢ x ≠ a ∧ ¬x ∈ as
Theorem: List.ne_mem_cons
Proof state before:
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
⊢ x ≠ a ∧ ¬x ∈ as
Tactic:
apply And.intro <;> intros _ <;> apply Hne
Proof state after:
case left
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x = a
⊢ x ∈ a :: as

case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Theorem: List.ne_mem_cons
Proof state before:
case left
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x = a
⊢ x ∈ a :: as

case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Tactic:
. subst x; constructor
Proof state after:
case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Theorem: List.ne_mem_cons
Proof state before:
case right
α : Type u_1
x a : α
as : List α
Hne : ¬x ∈ a :: as
a✝ : x ∈ as
⊢ x ∈ a :: as
Tactic:
. constructor; assumption
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
⊢ ∀ {α : Type} (xs : List α) (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
Tactic:
intros α xs
Proof state after:
α : Type
xs : List α
⊢ ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
xs : List α
⊢ ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
Tactic:
induction xs
Proof state after:
case nil
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []

case cons
α : Type
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (i : ℕ) (INBOUND : i < length tail✝), Mem (getF tail✝ i INBOUND) tail✝
⊢ ∀ (i : ℕ) (INBOUND : i < length (head✝ :: tail✝)), Mem (getF (head✝ :: tail✝) i INBOUND) (head✝ :: tail✝)
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []
Tactic:
case nil => {
  intros i INBOUND; simp at INBOUND;
}
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
⊢ ∀ (i : ℕ) (INBOUND : i < length (x' :: xs)), Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
case cons x' xs IH => {
  intros i INBOUND;
  cases i;
  case zero => {
     simp [List.getF];
     constructor;
  }
  case succ i' => {
   simp [List.getF];
   constructor;
   apply IH;
 }
}
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
⊢ ∀ (i : ℕ) (INBOUND : i < length []), Mem (getF [] i INBOUND) []
Tactic:
intros i INBOUND
Proof state after:
α : Type
i : ℕ
INBOUND : i < length []
⊢ Mem (getF [] i INBOUND) []
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
i : ℕ
INBOUND : i < length []
⊢ Mem (getF [] i INBOUND) []
Tactic:
simp at INBOUND
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
⊢ ∀ (i : ℕ) (INBOUND : i < length (x' :: xs)), Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
intros i INBOUND
Proof state after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i : ℕ
INBOUND : i < length (x' :: xs)
⊢ Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i : ℕ
INBOUND : i < length (x' :: xs)
⊢ Mem (getF (x' :: xs) i INBOUND) (x' :: xs)
Tactic:
cases i
Proof state after:
case zero
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)

case succ
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
n✝ : ℕ
INBOUND : Nat.succ n✝ < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ n✝) INBOUND) (x' :: xs)
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)
Tactic:
case zero => {
   simp [List.getF];
   constructor;
}
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
i' : ℕ
INBOUND : Nat.succ i' < length (x' :: xs)
⊢ Mem (getF (x' :: xs) (Nat.succ i') INBOUND) (x' :: xs)
Tactic:
case succ i' => {
 simp [List.getF];
 constructor;
 apply IH;
}
Proof state after:
no goals
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem (getF (x' :: xs) Nat.zero INBOUND) (x' :: xs)
Tactic:
simp [List.getF]
Proof state after:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem x' (x' :: xs)
Theorem: List.List.getF_implies_mem
Proof state before:
α : Type
x' : α
xs : List α
IH : ∀ (i : ℕ) (INBOUND : i < length xs), Mem (getF xs i INBOUND) xs
INBOUND : Nat.zero < length (x' :: xs)
⊢ Mem x' (x' :: xs)
Tactic:
constructor
Proof state after:
no goals