Theorem: TopM.set_unfold (MLIR/Semantics/Semantics.lean)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ set τ name v env =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)
Tactic:
simp [TopM.set]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)
Tactic:
simp_monad
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
v : MLIRType.eval τ
⊢ (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    match SSAEnv.get name τ env with
    | some val => Except.error ("setting to SSA value twice!", env)
    | none => Except.ok ((), SSAEnv.set name τ v env)
Tactic:
cases (env.get name τ) <;> rfl
State after:
no goals