Theorem: denoteOpArgs_equiv
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 Δ)⦄ ⦃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
Proof 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₂)