Theorem: SSAEnv.refines_set (MLIR/Semantics/Refinement.lean)

State before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ refines env1 env2 → refines (set name τ val env1) (set name τ val env2)
Tactic:
simp [refines, SSAEnv.refines]
State after:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ (∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }) →
    ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v (set name τ val env2) = some { fst := a, snd := b } →
        getT v (set name τ val env1) = some { fst := a, snd := b }

State before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ (∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }) →
    ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v (set name τ val env2) = some { fst := a, snd := b } →
        getT v (set name τ val env1) = some { fst := a, snd := b }
Tactic:
intros Href name' val' Hget
State after:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

State before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
by_cases H: name = name'
State after:
case pos
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

State before:
case pos
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
. subst H;
  rw [SSAEnv.getT_set_eq] <;> try assumption
  rw [SSAEnv.getT_set_eq] <;> try assumption
  intros K; assumption;
State after:
case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

State before:
case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
. rw [SSAEnv.getT_set_ne] <;> try assumption
  rw [SSAEnv.getT_set_ne] <;> try assumption
  intros K;
  apply Href; assumption;
State after:
no goals

State before:
case neg.a
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ name ≠ name'
Tactic:
assumption
State after:
no goals