Theorem: TopM.set_env_set_commutes (MLIR/Semantics/Semantics.lean)

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
⊢ ∀ ⦃τ : MLIRType Δ⦄ ⦃name : SSAVal⦄ ⦃v : MLIRType.eval τ⦄ ⦃env : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env' : SSAEnv Δ⦄,
    set τ name v env = Except.ok (r, env') →
      ∀ ⦃name' : SSAVal⦄,
        name' ≠ name →
          ∀ (τ' : MLIRType Δ) (v' : MLIRType.eval τ'),
            ∃ env'',
              SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
                set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
Tactic:
intros τ name v env r env' H name' Hname τ' v'
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H : set τ name v env = Except.ok (r, env')
name' : SSAVal
Hname : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧ set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H : set τ name v env = Except.ok (r, env')
name' : SSAVal
Hname : name' ≠ name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧ set τ name v (SSAEnv.set name' τ' v' env) = Except.ok (r, env'')
Tactic:
simp [set] at *
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      bind StateT.get
          (fun s =>
            match SSAEnv.get name τ s with
            | some val => raiseUB "setting to SSA value twice!"
            | none => StateT.set (SSAEnv.set name τ v s))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some val => raiseUB "setting to SSA value twice!"
        | none => StateT.set (SSAEnv.set name τ v s))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      bind StateT.get
          (fun s =>
            match SSAEnv.get name τ s with
            | some val => raiseUB "setting to SSA value twice!"
            | none => StateT.set (SSAEnv.set name τ v s))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
simp_monad at *
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
H :
  (match SSAEnv.get name τ env with
      | some val => raiseUB "setting to SSA value twice!"
      | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
      env =
    Except.ok (r, env')
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
revert H
State after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        env =
      Except.ok (r, env') →
    ∃ env'',
      SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
        (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
            | some val => raiseUB "setting to SSA value twice!"
            | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
            (SSAEnv.set name' τ' v' env) =
          Except.ok (r, env'')

State before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
⊢ (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v env))
        env =
      Except.ok (r, env') →
    ∃ env'',
      SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
        (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
            | some val => raiseUB "setting to SSA value twice!"
            | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
            (SSAEnv.set name' τ' v' env) =
          Except.ok (r, env'')
Tactic:
cases Hget: (env.get name τ) <;> simp <;> intros H <;> try contradiction
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
simp_ssaenv
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ env with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
H : SSAEnv.set name τ v env = env'
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ env with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
subst env'
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) env'' ∧
      (match SSAEnv.get name τ env with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) env'' ∧
      (match SSAEnv.get name τ env with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
exists (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)) ∧
    (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
        (SSAEnv.set name' τ' v' env) =
      Except.ok (r, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)) ∧
    (match SSAEnv.get name τ env with
        | some val => raiseUB "setting to SSA value twice!"
        | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
        (SSAEnv.set name' τ' v' env) =
      Except.ok (r, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Tactic:
simp[Hget]
State after:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))

State before:
case none
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ SSAEnv.equiv (SSAEnv.set name' τ' v' (SSAEnv.set name τ v env)) (SSAEnv.set name τ v (SSAEnv.set name' τ' v' env))
Tactic:
apply SSAEnv.set_commutes
State after:
case none.a
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ name ≠ name'

State before:
case none.a
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
Hget : SSAEnv.get name τ env = none
⊢ name ≠ name'
Tactic:
simp [Ne.symm Hname]
State after:
no goals

State before:
case some
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
v : MLIRType.eval τ
env : SSAEnv Δ
r : Unit
env' : SSAEnv Δ
name' : SSAVal
Hname : ¬name' = name
τ' : MLIRType Δ
v' : MLIRType.eval τ'
val✝ : MLIRType.eval τ
Hget : SSAEnv.get name τ env = some val✝
H : raiseUB "setting to SSA value twice!" env = Except.ok (r, env')
⊢ ∃ env'',
    SSAEnv.equiv (SSAEnv.set name' τ' v' env') env'' ∧
      (match SSAEnv.get name τ (SSAEnv.set name' τ' v' env) with
          | some val => raiseUB "setting to SSA value twice!"
          | none => fun x => Except.ok (PUnit.unit, SSAEnv.set name τ v (SSAEnv.set name' τ' v' env)))
          (SSAEnv.set name' τ' v' env) =
        Except.ok (r, env'')
Tactic:
contradiction
State after:
no goals