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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run (denoteOpArgs Δ ((name, ty) :: args)) env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[run_denoteOpArgs_cons_]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run
      (do
        let x ← TopM.get ty name
        let xs ← denoteOpArgs Δ args
        pure ({ fst := ty, snd := x } :: xs))
      env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ run
      (do
        let x ← TopM.get ty name
        let xs ← denoteOpArgs Δ args
        pure ({ fst := ty, snd := x } :: xs))
      env =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp [run_bind]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (TopM.get ty name) env with
    | Except.ok (a, env') =>
      match run (denoteOpArgs Δ args) env' with
      | Except.ok (a_1, env') => run (pure ({ fst := ty, snd := a } :: a_1)) env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (TopM.get ty name) env with
    | Except.ok (a, env') =>
      match run (denoteOpArgs Δ args) env' with
      | Except.ok (a_1, env') => run (pure ({ fst := ty, snd := a } :: a_1)) env'
      | Except.error e => Except.error e
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[run_TopM_get_success (ENV := ENV)]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (denoteOpArgs Δ args) env with
    | Except.ok (a, env') => run (pure ({ fst := ty, snd := v } :: a)) env'
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match run (denoteOpArgs Δ args) env with
    | Except.ok (a, env') => run (pure ({ fst := ty, snd := v } :: a)) env'
    | Except.error e => Except.error e) =
    match run (denoteOpArgs Δ args) env with
    | Except.ok (xs, env') => Except.ok ({ fst := ty, snd := v } :: xs, env')
    | Except.error e => Except.error e
Tactic:
simp[pure, StateT.pure, run, StateT.run, Except.pure]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e) =
    match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
env : SSAEnv Δ
ty : MLIRType Δ
v : MLIRType.eval ty
name : SSAVal
ENV : SSAEnv.get name ty env = some v
args : List (TypedSSAVal Δ)
⊢ (match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e) =
    match denoteOpArgs Δ args env with
    | Except.ok (a, env') => Except.ok ({ fst := ty, snd := v } :: a, env')
    | Except.error e => Except.error e
Tactic:
cases denoteOpArgs Δ args env <;> simp
State after:
no goals