Theorem: SSAScope.getT_set_ne (MLIR/Semantics/SSAEnv.lean)

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v → ∀ ⦃scope : SSAScope δ⦄ ⦃τ : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄, getT v (set v' τ val scope) = getT v scope
Tactic:
intros Hne scope τ val
State after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val scope) = getT v scope

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val scope) = getT v scope
Tactic:
induction scope with
| nil => simp [Hne]
| cons head tail =>
  simp
  byCases H: head.fst = v'
  . simp [Hne]
  . byCases H2: head.fst = v
    assumption
State after:
no goals

State before:
case nil
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v' τ val []) = getT v []
Tactic:
simp [Hne]
State after:
no goals

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (set v' τ val (head :: tail)) = getT v (head :: tail)
Tactic:
simp
State after:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (if head.fst = v' then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v' τ val tail) =
    if head.fst = v then some head.2 else getT v tail

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
⊢ getT v (if head.fst = v' then (head.fst, { fst := τ, snd := val }) :: tail else head :: set v' τ val tail) =
    if head.fst = v then some head.2 else getT v tail
Tactic:
byCases H: head.fst = v'
State after:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hne : head.fst ≠ v
tail_ih✝ : getT v (set head.fst τ val tail) = getT v tail
⊢ (if head.fst = v then some { fst := τ, snd := val } else getT v tail) =
    if head.fst = v then some head.2 else getT v tail

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail

State before:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hne : head.fst ≠ v
tail_ih✝ : getT v (set head.fst τ val tail) = getT v tail
⊢ (if head.fst = v then some { fst := τ, snd := val } else getT v tail) =
    if head.fst = v then some head.2 else getT v tail

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Tactic:
. simp [Hne]
State after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail

State before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT v (set v' τ val tail) = getT v tail
H : ¬head.fst = v'
⊢ (if head.fst = v then some head.2 else getT v (set v' τ val tail)) = if head.fst = v then some head.2 else getT v tail
Tactic:
. byCases H2: head.fst = v
  assumption
State after:
no goals