Theorem: denoteOpArgs_equiv (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
args : List (TypedSSAVal Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ args env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ args env₂ = Except.ok (r, env₂)
Tactic:
induction args <;> intros env r env' H
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
tail_ih✝ :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail✝ env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail✝ env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head✝ :: tail✝) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head✝ :: tail✝) env₂ = Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)
Tactic:
case nil =>
  simp [denoteOpArgs] at *
  simp_monad at *
  cases H; subst r env
  simp
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)
Tactic:
case cons head tail HInd =>
  intros env₂ Henv₂
  simp [denoteOpArgs]; simp [denoteOpArgs] at H
  have ⟨headName, headτ⟩ := head
  simp_monad at *
  revert H
  cases Hhead: TopM.get headτ headName env <;> simp <;> intros H <;> try contradiction
  case ok headR =>
  have ⟨headR, headEnv⟩ := headR
  simp [TopM.get_equiv Henv₂ Hhead]
  split at H <;> try contradiction
  case h_2 tailR HTailR =>
  simp at H; cases H; subst env' r
  have ⟨tailR, tailEnv⟩ := tailR; simp at HTailR
  have AOEU := HInd HTailR
  rw [TopM.get_unfold] at Hhead; simp at Hhead; cases Hhead; subst env
  specialize HInd HTailR Henv₂
  simp [denoteOpArgs] at HInd
  simp_monad at *
  simp [HInd]
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ [] env₂ = Except.ok (r, env₂)
Tactic:
simp [denoteOpArgs] at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : pure [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → pure [] env₂ = Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : pure [] env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → pure [] env₂ = Except.ok (r, env₂)
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : [] = r ∧ env = env'
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → [] = r

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : [] = r ∧ env = env'
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → [] = r
Tactic:
cases H
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
left✝ : [] = r
right✝ : env = env'
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → [] = r

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
left✝ : [] = r
right✝ : env = env'
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → [] = r
Tactic:
subst r env
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env' : SSAEnv Δ
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env' env₂ → [] = []

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
env' : SSAEnv Δ
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env' env₂ → [] = []
Tactic:
simp
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
⊢ ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)
Tactic:
intros env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ denoteOpArgs Δ (head :: tail) env₂ = Except.ok (r, env₂)
Tactic:
simp [denoteOpArgs]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ 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, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' : SSAEnv Δ
H : denoteOpArgs Δ (head :: tail) env = Except.ok (r, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ 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, env₂)
Tactic:
simp [denoteOpArgs] at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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, env')
⊢ 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, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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, env')
⊢ 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, env₂)
Tactic:
have ⟨headName, headτ⟩ := head
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
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, env')
⊢ 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, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
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, env')
⊢ 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, env₂)
Tactic:
simp_monad at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
H :
  (match TopM.get headτ headName env with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)
Tactic:
revert H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
⊢ (match TopM.get headτ headName env with
      | Except.error err => Except.error err
      | Except.ok v =>
        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 v.snd with
        | Except.error err => Except.error err
        | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
      Except.ok (r, env') →
    (match TopM.get headτ headName env₂ with
      | Except.error err => Except.error err
      | Except.ok v =>
        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 v.snd with
        | Except.error err => Except.error err
        | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
      Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
⊢ (match TopM.get headτ headName env with
      | Except.error err => Except.error err
      | Except.ok v =>
        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 v.snd with
        | Except.error err => Except.error err
        | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
      Except.ok (r, env') →
    (match TopM.get headτ headName env₂ with
      | Except.error err => Except.error err
      | Except.ok v =>
        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 v.snd with
        | Except.error err => Except.error err
        | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
      Except.ok (r, env₂)
Tactic:
cases Hhead: TopM.get headτ headName env <;> simp <;> intros H <;> try contradiction
State after:
case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
a✝ : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok a✝
H :
  (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 a✝.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := a✝.fst } :: v.fst, v.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headR
H :
  (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 headR.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headR.fst } :: v.fst, v.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)
Tactic:
case ok headR =>
have ⟨headR, headEnv⟩ := headR
simp [TopM.get_equiv Henv₂ Hhead]
split at H <;> try contradiction
case h_2 tailR HTailR =>
simp at H; cases H; subst env' r
have ⟨tailR, tailEnv⟩ := tailR; simp at HTailR
have AOEU := HInd HTailR
rw [TopM.get_unfold] at Hhead; simp at Hhead; cases Hhead; subst env
specialize HInd HTailR Henv₂
simp [denoteOpArgs] at HInd
simp_monad at *
simp [HInd]
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR : MLIRType.eval headτ × SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok headR
H :
  (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 headR.snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := headR.fst } :: v.fst, v.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)
Tactic:
have ⟨headR, headEnv⟩ := headR
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
H :
  (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 (headR, headEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
H :
  (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 (headR, headEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r, env')
⊢ (match TopM.get headτ headName env₂ with
    | Except.error err => Except.error err
    | Except.ok v =>
      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 v.snd with
      | Except.error err => Except.error err
      | Except.ok v_1 => Except.ok ({ fst := headτ, snd := v.fst } :: v_1.fst, v_1.snd)) =
    Except.ok (r, env₂)
Tactic:
simp [TopM.get_equiv Henv₂ Hhead]
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
H :
  (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 (headR, headEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r, 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 (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
H :
  (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 (headR, headEnv).snd with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: v.fst, v.snd)) =
    Except.ok (r, 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 (r, env₂)
Tactic:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
v✝ : List (TypedArg Δ) × SSAEnv Δ
heq✝ :
  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 (headR, headEnv).snd =
    Except.ok v✝
H : Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: v✝.fst, v✝.snd) = Except.ok (r, 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 (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
H : Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: tailR.fst, tailR.snd) = Except.ok (r, 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 (r, env₂)
Tactic:
case h_2 tailR HTailR =>
simp at H; cases H; subst env' r
have ⟨tailR, tailEnv⟩ := tailR; simp at HTailR
have AOEU := HInd HTailR
rw [TopM.get_unfold] at Hhead; simp at Hhead; cases Hhead; subst env
specialize HInd HTailR Henv₂
simp [denoteOpArgs] at HInd
simp_monad at *
simp [HInd]
State after:
no goals

State before:
case h_1
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ :
  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 (headR, headEnv).snd =
    Except.error err✝
H : Except.error err✝ = Except.ok (r, 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 (r, env₂)
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
H : Except.ok ({ fst := headτ, snd := (headR, headEnv).fst } :: tailR.fst, tailR.snd) = Except.ok (r, 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 (r, env₂)
Tactic:
simp at H
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
H : { fst := headτ, snd := headR } :: tailR.fst = r ∧ tailR.snd = 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 (r, env₂)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
H : { fst := headτ, snd := headR } :: tailR.fst = r ∧ tailR.snd = 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 (r, env₂)
Tactic:
cases H
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
left✝ : { fst := headτ, snd := headR } :: tailR.fst = r
right✝ : tailR.snd = 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 (r, env₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env : SSAEnv Δ
r : List (TypedArg Δ)
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
left✝ : { fst := headτ, snd := headR } :: tailR.fst = r
right✝ : tailR.snd = 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 (r, env₂)
Tactic:
subst env' r
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
⊢ (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.fst, env₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
tailR : List (TypedArg Δ) × 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 (headR, headEnv).snd =
    Except.ok tailR
⊢ (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.fst, env₂)
Tactic:
have ⟨tailR, tailEnv⟩ := tailR
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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 (headR, headEnv).snd =
    Except.ok (tailR, tailEnv)
⊢ (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₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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 (headR, headEnv).snd =
    Except.ok (tailR, tailEnv)
⊢ (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 at HTailR
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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)
⊢ (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₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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)
⊢ (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:
have AOEU := HInd HTailR
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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₂)
⊢ (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₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead : TopM.get headτ headName env = Except.ok (headR, headEnv)
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₂)
⊢ (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:
rw [TopM.get_unfold] at Hhead
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (headR, headEnv)
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₂)
⊢ (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₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
headName : SSAVal
headτ : MLIRType Δ
headR✝ : MLIRType.eval headτ × SSAEnv Δ
headR : MLIRType.eval headτ
headEnv : SSAEnv Δ
Hhead :
  Except.ok
      (match SSAEnv.get headName headτ env with
        | some v => v
        | none => default,
        env) =
    Except.ok (headR, headEnv)
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₂)
⊢ (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 at Hhead
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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₂)
Hhead :
  (match SSAEnv.get headName headτ env with
      | some v => v
      | none => default) =
      headR ∧
    env = headEnv
⊢ (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₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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₂)
Hhead :
  (match SSAEnv.get headName headτ env with
      | some v => v
      | none => default) =
      headR ∧
    env = headEnv
⊢ (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:
cases Hhead
State after:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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₂)
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    headR
right✝ : env = headEnv
⊢ (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₂)

State before:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
env env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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₂)
left✝ :
  (match SSAEnv.get headName headτ env with
    | some v => v
    | none => default) =
    headR
right✝ : env = headEnv
⊢ (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:
subst env
State after:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
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
⊢ (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₂)

State before:
case intro.intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α✝ σ✝ : Type
ε✝ : σ✝ → Type
Δ : Dialect α✝ σ✝ ε✝
S : Semantics Δ
head : TypedSSAVal Δ
tail : List (TypedSSAVal Δ)
HInd :
  ∀ ⦃env : SSAEnv Δ⦄ ⦃r : List (TypedArg Δ)⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOpArgs Δ tail env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄, SSAEnv.equiv env env₂ → denoteOpArgs Δ tail env₂ = Except.ok (r, env₂)
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
⊢ (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:
specialize HInd HTailR Henv₂
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 : denoteOpArgs Δ 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₂)

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 : denoteOpArgs Δ 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 [denoteOpArgs] at HInd
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 => 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₂)

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 *
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₂)

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 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₂)
Tactic:
simp [HInd]
State after:
no goals