Theorem: SSAEnv.equiv_set (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
⊢ equiv env₁ env₂ →
    ∀ ⦃name : SSAVal⦄ ⦃τ : MLIRType δ⦄ ⦃v : MLIRType.eval τ⦄, equiv (set name τ v env₁) (set name τ v env₂)
Tactic:
intros HEnv name τ v name' τ'
State after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
byCases Hname: name = name'
State after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name' τ v env₁) = get name' τ' (set name' τ v env₂)

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)

State before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name' τ v env₁) = get name' τ' (set name' τ v env₂)

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
. simp [get_set_eq_val]
State after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)

State before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
. repeat rw [get_set_ne_val] <;> try assumption
  apply HEnv
State after:
no goals

State before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' env₁ = get name' τ' (set name τ v env₂)
Tactic:
rw [get_set_ne_val] <;> try assumption
State after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' env₁ = get name' τ' env₂

State before:
case h2.a
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ name ≠ name'
Tactic:
assumption
State after:
no goals