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

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃env : SSAEnv Δ⦄ ⦃r : MLIRType.eval τ⦄ ⦃env' : SSAEnv Δ⦄,
    get τ name env = Except.ok (r, env') →
      ∀ ⦃name' : SSAVal⦄,
        name' ≠ name →
          ∀ ⦃τ' : MLIRType Δ⦄ ⦃v' : MLIRType.eval τ'⦄,
            get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
intros τ name env r env' H name' Hne τ' v'
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H : get τ name env = Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H : get τ name env = Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ get τ name (SSAEnv.set name' τ' v' env) = Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
rw [TopM.get_unfold] at *
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H :
  Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ Except.ok
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
        | some v => v
        | none => default,
        SSAEnv.set name' τ' v' env) =
    Except.ok (r, SSAEnv.set name' τ' v' env')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
H :
  Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (r, env')
name' : SSAVal
Hne : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ Except.ok
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
        | some v => v
        | none => default,
        SSAEnv.set name' τ' v' env) =
    Except.ok (r, SSAEnv.set name' τ' v' env')
Tactic:
simp_monad at *
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
simp_ssaenv at *
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
H :
  (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    env = env'
⊢ (match SSAEnv.get name τ env with
      | some v => v
      | none => default) =
      r ∧
    SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
revert H
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      env = env' →
    (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
r : MLIRType.eval τ
env' : SSAEnv Δ
name' : SSAVal
Hne : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      env = env' →
    (match SSAEnv.get name τ env with
        | some v => v
        | none => default) =
        r ∧
      SSAEnv.set name' τ' v' env = SSAEnv.set name' τ' v' env'
Tactic:
cases (env.get name τ) <;> simp at * <;> intros H1 H2 <;> subst r <;> subst env <;> simp
State after:
no goals