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' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝¹ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
argsRes : List (TypedArg Δ) × SSAEnv Δ
argRes : List (TypedArg Δ)
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, env)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
regR : List (TypedArg Δ) × SSAEnv Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd res) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok regR
H :
  (match res with
      | [] => fun s => Except.ok (regR.fst, s)
      | [res] =>
        match regR.fst with
        | [{ fst := τ, snd := v }] => fun s =>
          match TopM.set τ res.fst v s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (regR.fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString regR.fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (regR.fst, v.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 => Except.ok (regR.fst, v.snd))
      regR.snd =
    Except.ok (r, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name (List.map Prod.snd res) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ 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:
case h_2 regR HregR =>
have ⟨regR, regEnv⟩ := regR
have HRegInd := OpM.toTopM_regions_equiv (TopM.mapDenoteRegion Δ regions)
have ⟨regEnv₂, HregEnv₂, HregR₂⟩ := HRegInd (by sorry) HregR Henv₂ simp [HregR₂]
cases res
case nil =>
  simp at *; cases H; exists regEnv₂
  subst r env'; simp [HregEnv₂]
  sorry case cons headRes tailRes =>
  cases tailRes
  case cons _ _ => simp at *; cases H
  case nil =>
    simp
    cases regR
    case nil => simp at *; cases H
    case cons opRHead opRTail =>
      cases opRTail
      case cons _ _ =>  simp at *; cases H
      case nil =>
          simp at *
          split at H <;> try contradiction
          case h_2 setRes HSetRes =>
          sorry
Proof state after:
no goals