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

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
env : SSAEnv δ
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
⊢ getT v (set v τ val env) = some { fst := τ, snd := val }
Tactic:
cases env with
| One s =>
  simp [getT, set]
  rw [SSAScope.getT_set_eq]
| Cons head tail =>
  simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
  simp [SSAScope.getT_set_eq]
State after:
no goals

State before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ getT v (set v τ val (One s)) = some { fst := τ, snd := val }
Tactic:
simp [getT, set]
State after:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v τ val s) = some { fst := τ, snd := val }

State before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v τ val s) = some { fst := τ, snd := val }
Tactic:
rw [SSAScope.getT_set_eq]
State after:
no goals

State before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ getT v (set v τ val (Cons head tail)) = some { fst := τ, snd := val }
Tactic:
simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
State after:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    some { fst := τ, snd := val }

State before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v : SSAVal
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ (match SSAScope.getT v (SSAScope.set v τ val head), fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()) =
    some { fst := τ, snd := val }
Tactic:
simp [SSAScope.getT_set_eq]
State after:
no goals