Theorem: denoteOpArgs_equiv
Proof state before:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env₂ : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR✝ : List (TypedArg Δ) × SSAEnv Δ
tailR : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 headEnv =
    Except.ok (tailR, tailEnv)
AOEU : ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv headEnv env₂ → denoteOpArgs Δ tail env₂ = Except.ok (tailR, env₂)
Henv₂ : SSAEnv.equiv headEnv env₂
left✝ :
  (match SSAEnv.get headName headτ headEnv with
    | some v => v
    | none => default) =
    headR
HInd :
  mapM
      (fun x => do
        let __do_lift ← TopM.get x.snd x.fst
        pure { fst := x.snd, snd := __do_lift })
      tail env₂ =
    Except.ok (tailR, env₂)
⊢ (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 env₂ with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headR } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headR } :: (tailR, tailEnv).fst, env₂)
Tactic:
simp_monad at *
Proof state after:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
env₂ : SSAEnv Δ
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR✝ : List (TypedArg Δ) × SSAEnv Δ
tailR : List (TypedArg Δ)
tailEnv : SSAEnv Δ
HTailR :
  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 headEnv =
    Except.ok (tailR, tailEnv)
AOEU : ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv headEnv env₂ → denoteOpArgs Δ tail env₂ = Except.ok (tailR, env₂)
Henv₂ : SSAEnv.equiv headEnv env₂
left✝ :
  (match SSAEnv.get headName headτ headEnv with
    | some v => v
    | none => default) =
    headR
HInd :
  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 (tailR, env₂)
⊢ (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 env₂ with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headR } :: v.fst, v.snd)) =
    Except.ok ({ fst := headτ, snd := headR } :: tailR, env₂)