Theorem: denoteOpArgs_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x => do
            let __do_lift ← TopM.get x.snd x.fst
            pure { fst := x.snd, snd := __do_lift })
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x => do
                  let __do_lift ← TopM.get x.snd x.fst
                  pure { fst := x.snd, snd := __do_lift })
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)
Tactic:
simp [bind, StateT.bind, Except.bind, pure, StateT.pure, Except.pure] at HInd
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env : SSAEnv Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
headName : SSAVal
headτ : MLIRType Δ
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃resEnv : SSAEnv Δ⦄,
    mapM
          (fun x s =>
            match TopM.get x.snd x.fst s with
            | Except.error err => Except.error err
            | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
          tail env =
        Except.ok (r, resEnv) →
      ∀ ⦃name : SSAVal⦄,
        (∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a) →
          ∀ (τ : MLIRType Δ) (v : MLIRType.eval τ),
            mapM
                (fun x s =>
                  match TopM.get x.snd x.fst s with
                  | Except.error err => Except.error err
                  | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
                tail (SSAEnv.set name τ v env) =
              Except.ok (r, SSAEnv.set name τ v resEnv)
Hname : ¬name = headName ∧ ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
headRes : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headRes
Hname_head : ¬name = headName
right✝ : ∀ (a : SSAVal) (b : MLIRType Δ), (a, b) ∈ tail → ¬name = a
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
rTail : List (TypedArg Δ) × SSAEnv Δ
rTailRes : List (TypedArg Δ)
rTailEnv : SSAEnv Δ
Htail :
  mapM
      (fun x s =>
        match TopM.get x.snd x.fst s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
      tail headRes.snd =
    Except.ok (rTailRes, rTailEnv)
H : True
⊢ (match
      mapM
        (fun x s =>
          match TopM.get x.snd x.fst s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ({ fst := x.snd, snd := v.fst }, v.snd))
        tail (SSAEnv.set name τ v headRes.snd) with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headRes.fst } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headRes.fst } :: rTailRes, SSAEnv.set name τ v rTailEnv)