Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
Hname : (List.all (head :: tail) fun arg => decide (name ≠ arg.fst)) = true
τ : MLIRType Δ
v : MLIRType.eval τ
H :
  bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get head.snd head.fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := head.snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)
Tactic:
have ⟨headName, headτ⟩ := head
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (List.all tail fun arg => decide (name ≠ arg.fst)) = true →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            denoteOpArgs Δ tail (SSAEnv.set name τ v env) = Except.ok (r, SSAEnv.set name τ v resEnv)
env : SSAEnv Δ
r : List (TypedArg Δ)
resEnv : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
Hname : (List.all ((headName, headτ) :: tail) fun arg => decide (name ≠ arg.fst)) = true
H :
  bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      env =
    Except.ok (r, resEnv)
⊢ bind (TopM.get (headName, headτ).snd (headName, headτ).fst)
      (fun x => do
        let __do_lift ←
          mapM
              (fun x => do
                let __do_lift ← TopM.get x.snd x.fst
                pure { fst := x.snd, snd := __do_lift })
              tail
        pure ({ fst := (headName, headτ).snd, snd := x } :: __do_lift))
      (SSAEnv.set name τ v env) =
    Except.ok (r, SSAEnv.set name τ v resEnv)