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

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

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

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

State before:
case One
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ SSAScope.getT v (SSAScope.set v' τ val s) = SSAScope.getT v s
Tactic:
rw [SSAScope.getT_set_ne]
State after:
case One.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ v' ≠ v

State before:
case One.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
s : SSAScope δ
⊢ v' ≠ v
Tactic:
assumption
State after:
no goals

State before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ getT v (set v' τ val (Cons head tail)) = getT v (Cons head tail)
Tactic:
simp [getT, set, HOrElse.hOrElse, OrElse.orElse, Option.orElse]
State after:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : 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 ()) =
    match SSAScope.getT v head, fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()

State before:
case Cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : 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 ()) =
    match SSAScope.getT v head, fun x => getT v tail with
    | some a, x => some a
    | none, b => b ()
Tactic:
rw [SSAScope.getT_set_ne]
State after:
case Cons.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ v' ≠ v

State before:
case Cons.a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
τ : MLIRType δ
val : MLIRType.eval τ
head : SSAScope δ
tail : SSAEnv δ
⊢ v' ≠ v
Tactic:
assumption
State after:
no goals