Theorem: denoteOp_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
res args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    denoteOp Δ (Op.mk op_name res args regions attrs) env = Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂',
            SSAEnv.equiv env' env₂' ∧ denoteOp Δ (Op.mk op_name res args regions attrs) env₂ = Except.ok (r, env₂')
Tactic:
unfold denoteOp
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
res args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃r : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    (let resTy := List.map Prod.snd res;
          do
          let args ← denoteOpArgs Δ args
          let iop : IOp Δ := IOp.mk op_name resTy args (OpM.denoteRegions regions 0) attrs
          let ret ← OpM.toTopM (TopM.mapDenoteRegion Δ regions) (Semantics.semantics_op iop)
          let __do_jp : Unit → TopM Δ (TypedArgs Δ) := fun y => pure ret
          match res with
            | [] => do
              let y ← pure ()
              __do_jp y
            | [res] =>
              match ret with
              | [{ fst := τ, snd := v }] => do
                let y ← TopM.set τ res.fst v
                __do_jp y
              | x => do
                let y ←
                  TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString ret ++ toString "'")
                __do_jp y
            | x => do
              let y ← TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
              __do_jp y)
          env =
        Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂',
            SSAEnv.equiv env' env₂' ∧
              (let resTy := List.map Prod.snd res;
                  do
                  let args ← denoteOpArgs Δ args
                  let iop : IOp Δ := IOp.mk op_name resTy args (OpM.denoteRegions regions 0) attrs
                  let ret ← OpM.toTopM (TopM.mapDenoteRegion Δ regions) (Semantics.semantics_op iop)
                  let __do_jp : Unit → TopM Δ (TypedArgs Δ) := fun y => pure ret
                  match res with
                    | [] => do
                      let y ← pure ()
                      __do_jp y
                    | [res] =>
                      match ret with
                      | [{ fst := τ, snd := v }] => do
                        let y ← TopM.set τ res.fst v
                        __do_jp y
                      | x => do
                        let y ←
                          TopM.raiseUB
                              (toString "denoteOp: expected 1 return value, got '" ++ toString ret ++ toString "'")
                        __do_jp y
                    | x => do
                      let y ←
                        TopM.raiseUB
                            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
                      __do_jp y)
                  env₂ =
                Except.ok (r, env₂')