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

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : τ' = τ
⊢ MLIRType.eval τ' = MLIRType.eval τ
Tactic:
simp [H]
State after:
no goals

State before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v' τ' val env) =
    if v' = v then
      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)
            val)
      else none
    else get v τ env
Tactic:
byCases H: v' = v
State after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v τ' val env) =
    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)
          val)
    else none

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env

State before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v τ (set v τ' val env) =
    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)
          val)
    else none

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
. simp [get_set_eq_val]
State after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env

State before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ τ' : MLIRType δ
env : SSAEnv δ
v v' : SSAVal
val : MLIRType.eval τ'
H : ¬v' = v
⊢ get v τ (set v' τ' val env) = get v τ env
Tactic:
. rw [get_set_ne_val]
  assumption
State after:
no goals