Theorem: OpM.toTopM_regions_equiv (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ denoteRegionsEquivInvariant regions →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      toTopM regions opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions opM env₂ = Except.ok (res, env₂')
Tactic:
intros Hregs opM
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
opM : OpM Δ (TypedArgs Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions opM env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions opM env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
opM : OpM Δ (TypedArgs Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions opM env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions opM env₂ = Except.ok (res, env₂')
Tactic:
induction opM <;> intros env res env' H env₂ Henv₂ <;> try contradiction
State after:
case Ret
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
a✝ : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret a✝) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (Ret a✝) env₂ = Except.ok (res, env₂')

case RunRegion
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
a✝² : ℕ
a✝¹ : TypedArgs Δ
a✝ : TypedArgs Δ → OpM Δ (TypedArgs Δ)
a_ih✝ :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (a✝ a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (a✝ a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (RunRegion a✝² a✝¹ a✝) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (RunRegion a✝² a✝¹ a✝) env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret ret) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (Ret ret) env₂ = Except.ok (res, env₂')
Tactic:
case Ret ret =>
  unfold OpM.toTopM; unfold OpM.toTopM at H
  cases H <;> simp
  exists env₂
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (RunRegion idx args continuation) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (RunRegion idx args continuation) env₂ = Except.ok (res, env₂')
Tactic:
case RunRegion idx args continuation HInd =>
  unfold OpM.toTopM; unfold OpM.toTopM at H
  have ⟨⟨resReg, envReg⟩, HReg⟩ := ExceptMonad.split H
  simp_monad at *
  rw [HReg] at H; simp at H
  have ⟨env₂', Henv₂', HIx⟩ := denoteRegionByIx_equiv regions Hregs HReg Henv₂
  specialize (HInd resReg (by assumption) (by assumption))
  rw [HIx]; simp
  assumption
State after:
no goals

State before:
case Error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
a✝ : String
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Error a✝) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (Error a✝) env₂ = Except.ok (res, env₂')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret ret) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (Ret ret) env₂ = Except.ok (res, env₂')
Tactic:
unfold OpM.toTopM
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret ret) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure ret env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (Ret ret) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure ret env₂ = Except.ok (res, env₂')
Tactic:
unfold OpM.toTopM at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : pure ret env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure ret env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : pure ret env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ pure ret env₂ = Except.ok (res, env₂')
Tactic:
cases H <;> simp
State after:
case refl
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env env₂' ∧ pure ret env₂ = Except.ok (ret, env₂')

State before:
case refl
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
ret : TypedArgs Δ
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env env₂' ∧ pure ret env₂ = Except.ok (ret, env₂')
Tactic:
exists env₂
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (RunRegion idx args continuation) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (RunRegion idx args continuation) env₂ = Except.ok (res, env₂')
Tactic:
unfold OpM.toTopM
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (RunRegion idx args continuation) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : toTopM regions (RunRegion idx args continuation) env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')
Tactic:
unfold OpM.toTopM at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env =
    Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env =
    Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')
Tactic:
have ⟨⟨resReg, envReg⟩, HReg⟩ := ExceptMonad.split H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env =
    Except.ok (res, env')
resReg : TypedArgs Δ
envReg : SSAEnv Δ
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env =
    Except.ok (res, env')
resReg : TypedArgs Δ
envReg : SSAEnv Δ
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      Bind.bind (TopM.denoteRegionsByIx regions idx args) (fun ret => toTopM regions (continuation ret)) env₂ =
        Except.ok (res, env₂')
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match TopM.denoteRegionsByIx regions idx args env with
    | Except.error err => Except.error err
    | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
    Except.ok (res, env')
resReg : TypedArgs Δ
envReg : SSAEnv Δ
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H :
  (match TopM.denoteRegionsByIx regions idx args env with
    | Except.error err => Except.error err
    | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
    Except.ok (res, env')
resReg : TypedArgs Δ
envReg : SSAEnv Δ
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
rw [HReg] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H :
  (match Except.ok (resReg, envReg) with
    | Except.error err => Except.error err
    | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
    Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H :
  (match Except.ok (resReg, envReg) with
    | Except.error err => Except.error err
    | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
    Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
simp at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨env₂', Henv₂', HIx⟩ := denoteRegionByIx_equiv regions Hregs HReg Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
specialize (HInd resReg (by assumption) (by assumption))
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
rw [HIx]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1,
    SSAEnv.equiv env' env₂'_1 ∧
      (match Except.ok (resReg, env₂') with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂'_1)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1,
    SSAEnv.equiv env' env₂'_1 ∧
      (match Except.ok (resReg, env₂') with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂'_1)
Tactic:
simp
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ toTopM regions (continuation resReg) ?m.1084400 = Except.ok (?m.1084401, ?m.1084402)
Tactic:
assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ SSAEnv.equiv envReg ?m.1084404
Tactic:
assumption
State after:
no goals