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

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

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ get τ name env₁ = Except.ok (r, env₁') → get τ name env₂ = Except.ok (r, env₂)
Tactic:
repeat rw [TopM.get_unfold]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₁ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Tactic:
rw [Hequiv]
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₁) =
      Except.ok (r, env₁') →
    Except.ok
        (match SSAEnv.get name τ env₂ with
          | some v => v
          | none => default,
          env₂) =
      Except.ok (r, env₂)
Tactic:
simp_monad
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ (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

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
⊢ (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
Tactic:
intros H _
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
a✝ : env₁ = env₁'
⊢ (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
env₁ env₂ : SSAEnv Δ
Hequiv : SSAEnv.equiv env₁ env₂
τ : MLIRType Δ
name : SSAVal
r : MLIRType.eval τ
env₁' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
a✝ : env₁ = env₁'
⊢ (match SSAEnv.get name τ env₂ with
    | some v => v
    | none => default) =
    r
Tactic:
rw [H]
State after:
no goals

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