internlm/Lean-Github huggingface dataset:
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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₂
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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₂
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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 *
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')
Theorem: OpM.toTopM_regions_equiv
Proof 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
Proof 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₂')