Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
cases idx
Proof state after:
case zero
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) Nat.zero args (SSAEnv.set name τ v env) = Except.ok (res, env₂')

case succ
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
n✝ : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args (SSAEnv.set name τ v env) = Except.ok (res, env₂')