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

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v → ∀ ⦃env : SSAEnv δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ'⦄, get v τ (set v' τ' val env) = get 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 τ'
⊢ get v τ (set v' τ' val env) = get v τ env

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
simp [get]
State after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ (match getT v (set v' τ' val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ (match getT v (set v' τ' val env) with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none) =
    match getT v env with
    | none => none
    | some { fst := τ', snd := v' } =>
      if h : τ' = τ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            v')
      else none
Tactic:
rw [SSAEnv.getT_set_ne]
State after:
case a
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ'
⊢ v' ≠ v

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