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

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃env₁ env₂ : SSAEnv Δ⦄,
    SSAEnv.equiv env₁ env₂ →
      ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃v : MLIRType.eval τ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
        set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
intros env₁ env₂ Hequiv τ name v r env₁'
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ set τ name v env₁ = Except.ok (r, env₁') → set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
repeat rw [TopM.set_unfold]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, 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₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, 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₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
rw [Hequiv]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, 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₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₂ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, 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₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
cases (SSAEnv.get name τ env₂) <;> simp
State after:
no goals

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, env₁') →
    set τ name v env₂ = Except.ok (r, SSAEnv.set name τ v env₂)
Tactic:
rw [TopM.set_unfold]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
r : Unit
env₁' : SSAEnv Δ
⊢ (match SSAEnv.get name τ env₁ with
      | some val => Except.error ("setting to SSA value twice!", env₁)
      | none => Except.ok ((), SSAEnv.set name τ v env₁)) =
      Except.ok (r, 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₂)) =
      Except.ok (r, SSAEnv.set name τ v env₂)