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

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
scope : SSAScope δ
τ : MLIRType δ
val : MLIRType.eval τ
⊢ get v (set v τ val scope) τ = some val
Tactic:
induction scope with
| nil => simp;
| cons head nil =>
  simp
  byCases H: head.fst = v <;> try apply cast_eq
  assumption
State after:
no goals

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

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

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v τ val nil) τ = some val
⊢ get v (if head.fst = v then (head.fst, { fst := τ, snd := val }) :: nil else head :: set v τ val nil) τ = some val
Tactic:
byCases H: head.fst = v <;> try apply cast_eq
State after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v τ val nil) τ = some val
H : ¬head.fst = v
⊢ get v (set v τ val nil) τ = some val

State before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
nil : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : get v (set v τ val nil) τ = some val
H : ¬head.fst = v
⊢ get v (set v τ val nil) τ = some val
Tactic:
assumption
State after:
no goals