Theorem: run_bind_success (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ run (ma >>= a2mb) env = run (a2mb va) env'
Tactic:
simp[bind, StateT.bind, Except.bind]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ run
      (fun s =>
        match ma s with
        | Except.error err => Except.error err
        | Except.ok v => a2mb v.fst v.snd)
      env =
    run (a2mb va) env'

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ run
      (fun s =>
        match ma s with
        | Except.error err => Except.error err
        | Except.ok v => a2mb v.fst v.snd)
      env =
    run (a2mb va) env'
Tactic:
simp[run, StateT.run] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => a2mb v.fst v.snd) =
    a2mb va env'

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
a b : Type
Δ : Dialect α σ ε
S : Semantics Δ
ma : TopM Δ a
a2mb : a → TopM Δ b
env : SSAEnv Δ
va : a
env' : SSAEnv Δ
MA : ma env = Except.ok (va, env')
⊢ (match ma env with
    | Except.error err => Except.error err
    | Except.ok v => a2mb v.fst v.snd) =
    a2mb va env'
Tactic:
simp[MA]
State after:
no goals