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

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ set τ name v env = Except.ok r → r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
simp [set]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ 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 =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ 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 =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
simp_monad
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ (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 =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
⊢ (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 =
      Except.ok r →
    r = ((), SSAEnv.set name τ v env) ∧ SSAEnv.get name τ env = none
Tactic:
cases (env.get name τ) <;> simp <;> intros H <;> try contradiction
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
H : (PUnit.unit, SSAEnv.set name τ v env) = r
⊢ r = ((), SSAEnv.set name τ v env)

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
H : (PUnit.unit, SSAEnv.set name τ v env) = r
⊢ r = ((), SSAEnv.set name τ v env)
Tactic:
rw [H]
State after:
no goals

State before:
case some
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit × SSAEnv Δ
val✝ : MLIRType.eval τ
H : raiseUB "setting to SSA value twice!" env = Except.ok r
⊢ False
Tactic:
contradiction
State after:
no goals