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

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

State before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
scope : SSAScope δ
v : SSAVal
val : MLIRType.eval τ'
⊢ get v (set v τ' val scope) τ = none
Tactic:
induction scope with
| nil => simp [Hne]
| cons head tail Hind =>
  simp
  byCases H: head.fst = v
  . simp [Hne]
  . byCases H2: head.fst = v <;> try assumption
State after:
no goals

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

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

State before:
case cons
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
⊢ get v (if head.fst = v then (head.fst, { fst := τ', snd := val }) :: tail else head :: set v τ' val tail) τ = none
Tactic:
byCases H: head.fst = v
State after:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get head.fst (set head.fst τ' val tail) τ = none
⊢ τ' = τ → False

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
H : ¬head.fst = v
⊢ get v (set v τ' val tail) τ = none

State before:
case cons.h1
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get head.fst (set head.fst τ' val tail) τ = none
⊢ τ' = τ → False

case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
H : ¬head.fst = v
⊢ get v (set v τ' val tail) τ = none
Tactic:
. simp [Hne]
State after:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
H : ¬head.fst = v
⊢ get v (set v τ' val tail) τ = none

State before:
case cons.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
H : ¬head.fst = v
⊢ get v (set v τ' val tail) τ = none
Tactic:
. byCases H2: head.fst = v <;> try assumption
State after:
no goals

State before:
case cons.h2.h2
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
τ τ' : MLIRType δ
Hne : τ' ≠ τ
v : SSAVal
val : MLIRType.eval τ'
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
Hind : get v (set v τ' val tail) τ = none
H H2 : ¬head.fst = v
⊢ get v (set v τ' val tail) τ = none
Tactic:
assumption
State after:
no goals