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 Δ⦄,
    (match denoteOpArgs Δ args env with
        | Except.error err => Except.error err
        | Except.ok v =>
          match
            OpM.toTopM (TopM.mapDenoteRegion Δ regions)
              (Semantics.semantics_op
                (IOp.mk op_name (List.map Prod.snd res) v.fst (OpM.denoteRegions regions 0) attrs))
              v.snd with
          | Except.error err => Except.error err
          | Except.ok v =>
            (match res with
              | [] => fun s => Except.ok (v.fst, s)
              | [res] =>
                match v.fst with
                | [{ fst := τ, snd := v_1 }] => fun s =>
                  match TopM.set τ res.fst v_1 s with
                  | Except.error err => Except.error err
                  | Except.ok v_2 => Except.ok (v.fst, v_2.snd)
                | x => fun s =>
                  match
                    TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString v.fst ++ toString "'")
                      s with
                  | Except.error err => Except.error err
                  | Except.ok v_1 => Except.ok (v.fst, v_1.snd)
              | x => fun s =>
                match
                  TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
                    s with
                | Except.error err => Except.error err
                | Except.ok v_1 => Except.ok (v.fst, v_1.snd))
              v.snd) =
        Except.ok (r, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂',
            SSAEnv.equiv env' env₂' ∧
              (match denoteOpArgs Δ args env₂ with
                | Except.error err => Except.error err
                | Except.ok v =>
                  match
                    OpM.toTopM (TopM.mapDenoteRegion Δ regions)
                      (Semantics.semantics_op
                        (IOp.mk op_name (List.map Prod.snd res) v.fst (OpM.denoteRegions regions 0) attrs))
                      v.snd with
                  | Except.error err => Except.error err
                  | Except.ok v =>
                    (match res with
                      | [] => fun s => Except.ok (v.fst, s)
                      | [res] =>
                        match v.fst with
                        | [{ fst := τ, snd := v_1 }] => fun s =>
                          match TopM.set τ res.fst v_1 s with
                          | Except.error err => Except.error err
                          | Except.ok v_2 => Except.ok (v.fst, v_2.snd)
                        | x => fun s =>
                          match
                            TopM.raiseUB
                              (toString "denoteOp: expected 1 return value, got '" ++ toString v.fst ++ toString "'")
                              s with
                          | Except.error err => Except.error err
                          | Except.ok v_1 => Except.ok (v.fst, v_1.snd)
                      | x => fun s =>
                        match
                          TopM.raiseUB
                            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'") s with
                        | Except.error err => Except.error err
                        | Except.ok v_1 => Except.ok (v.fst, v_1.snd))
                      v.snd) =
                Except.ok (r, env₂')
Tactic:
intros env r env' H env₂ Henv₂
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 Δ
H :
  (match denoteOpArgs Δ args env with
    | Except.error err => Except.error err
    | Except.ok v =>
      match
        OpM.toTopM (TopM.mapDenoteRegion Δ regions)
          (Semantics.semantics_op (IOp.mk op_name (List.map Prod.snd res) v.fst (OpM.denoteRegions regions 0) attrs))
          v.snd with
      | Except.error err => Except.error err
      | Except.ok v =>
        (match res with
          | [] => fun s => Except.ok (v.fst, s)
          | [res] =>
            match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ res.fst v_1 s with
              | Except.error err => Except.error err
              | Except.ok v_2 => Except.ok (v.fst, v_2.snd)
            | x => fun s =>
              match
                TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString v.fst ++ toString "'")
                  s with
              | Except.error err => Except.error err
              | Except.ok v_1 => Except.ok (v.fst, v_1.snd)
          | x => fun s =>
            match
              TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'") s with
            | Except.error err => Except.error err
            | Except.ok v_1 => Except.ok (v.fst, v_1.snd))
          v.snd) =
    Except.ok (r, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match denoteOpArgs Δ args env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          match
            OpM.toTopM (TopM.mapDenoteRegion Δ regions)
              (Semantics.semantics_op
                (IOp.mk op_name (List.map Prod.snd res) v.fst (OpM.denoteRegions regions 0) attrs))
              v.snd with
          | Except.error err => Except.error err
          | Except.ok v =>
            (match res with
              | [] => fun s => Except.ok (v.fst, s)
              | [res] =>
                match v.fst with
                | [{ fst := τ, snd := v_1 }] => fun s =>
                  match TopM.set τ res.fst v_1 s with
                  | Except.error err => Except.error err
                  | Except.ok v_2 => Except.ok (v.fst, v_2.snd)
                | x => fun s =>
                  match
                    TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString v.fst ++ toString "'")
                      s with
                  | Except.error err => Except.error err
                  | Except.ok v_1 => Except.ok (v.fst, v_1.snd)
              | x => fun s =>
                match
                  TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString res ++ toString "'")
                    s with
                | Except.error err => Except.error err
                | Except.ok v_1 => Except.ok (v.fst, v_1.snd))
              v.snd) =
        Except.ok (r, env₂')