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

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

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 Δ⦄,
    (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₂')
Tactic:
simp_monad
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 Δ⦄,
    (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₂')

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

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 Δ
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₂')
Tactic:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : 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 Δ)
v✝ : List (TypedArg Δ) × SSAEnv Δ
heq✝ : denoteOpArgs Δ args env = Except.ok v✝
H :
  (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.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₂')

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 Δ
HargsRes : denoteOpArgs Δ args env = Except.ok argsRes
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) argsRes.fst (OpM.denoteRegions regions 0) attrs))
        argsRes.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.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:
case h_2 _ argsRes HargsRes =>
have ⟨argRes, argResEnv⟩ := argsRes
have _ := denoteOpArgs_res HargsRes; subst argResEnv
simp [denoteOpArgs_equiv HargsRes Henv₂]
split at H <;> try contradiction
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
State after:
no goals

State before:
case h_1
α₁ σ₁ : 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 Δ)
err✝ : String × SSAEnv Δ
heq✝ : denoteOpArgs Δ args env = Except.error err✝
H : Except.error err✝ = Except.ok (r, 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:
contradiction
State after:
no goals

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 Δ
HargsRes : denoteOpArgs Δ args env = Except.ok argsRes
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) argsRes.fst (OpM.denoteRegions regions 0) attrs))
        argsRes.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.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:
have ⟨argRes, argResEnv⟩ := argsRes
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' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
argsRes : List (TypedArg Δ) × SSAEnv Δ
argRes : List (TypedArg Δ)
argResEnv : SSAEnv Δ
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, argResEnv)
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) (argRes, argResEnv).fst (OpM.denoteRegions regions 0) attrs))
        (argRes, argResEnv).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.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₂')

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 Δ)
argResEnv : SSAEnv Δ
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, argResEnv)
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) (argRes, argResEnv).fst (OpM.denoteRegions regions 0) attrs))
        (argRes, argResEnv).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.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:
have _ := denoteOpArgs_res HargsRes
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' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝¹ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
argsRes : List (TypedArg Δ) × SSAEnv Δ
argRes : List (TypedArg Δ)
argResEnv : SSAEnv Δ
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, argResEnv)
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) (argRes, argResEnv).fst (OpM.denoteRegions regions 0) attrs))
        (argRes, argResEnv).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')
x✝ : argResEnv = 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₂')

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 Δ)
argResEnv : SSAEnv Δ
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, argResEnv)
H :
  (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op
          (IOp.mk op_name (List.map Prod.snd res) (argRes, argResEnv).fst (OpM.denoteRegions regions 0) attrs))
        (argRes, argResEnv).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')
x✝ : argResEnv = 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:
subst argResEnv
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' 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)
H :
  (match
      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 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.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₂')

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)
H :
  (match
      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 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.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:
simp [denoteOpArgs_equiv HargsRes Henv₂]
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' 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)
H :
  (match
      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 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.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₂')

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)
H :
  (match
      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 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.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:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : 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 Δ)
v✝ : List (TypedArg Δ) × SSAEnv Δ
heq✝ :
  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 v✝
H :
  (match res with
      | [] => fun s => Except.ok (v✝.fst, s)
      | [res] =>
        match v✝.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 (v✝.fst, v.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 => Except.ok (v✝.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 (v✝.fst, v.snd))
      v✝.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₂')

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
State after:
no goals

State before:
case h_1
α₁ σ₁ : 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 Δ)
err✝ : String × SSAEnv Δ
heq✝ :
  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.error err✝
H : Except.error err✝ = 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:
contradiction
State after:
no goals

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:
have ⟨regR, regEnv⟩ := regR
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' 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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).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₂')

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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).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:
have HRegInd := OpM.toTopM_regions_equiv (TopM.mapDenoteRegion Δ regions)
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' 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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, 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₂')

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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, 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:
have ⟨regEnv₂, HregEnv₂, HregR₂⟩ := HRegInd (by sorry) HregR Henv₂
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' 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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
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))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ 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₂')

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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
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))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ 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:
cases res
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [] ++ toString "'") s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name (List.map Prod.snd []) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [] 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 [] ++ 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₂')

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match head✝ :: tail✝ with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (head✝ :: tail✝) ++ toString "'") s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (head✝ :: tail✝)) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match head✝ :: tail✝ 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 (head✝ :: tail✝) ++ 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₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [] ++ toString "'") s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name (List.map Prod.snd []) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [] 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 [] ++ 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 nil =>
  simp at *; cases H; exists regEnv₂
  subst r env'; simp [HregEnv₂]
  sorry
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
tailRes : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match headRes :: tailRes with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: tailRes) ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match headRes :: tailRes 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 (headRes :: tailRes) ++ 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 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
State after:
no goals

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 Δ
regR : List (TypedArg Δ)
regEnv : 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, regEnv)
H :
  (match res with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).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, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions)
Tactic:
sorry
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [] ++ toString "'") s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd []) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name (List.map Prod.snd []) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [] 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 [] ++ 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:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
H : regR = r ∧ regEnv = env'
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok v) =
        Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
H : regR = r ∧ regEnv = env'
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok v) =
        Except.ok (r, env₂')
Tactic:
cases H
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
left✝ : regR = r
right✝ : regEnv = env'
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok v) =
        Except.ok (r, env₂')

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
left✝ : regR = r
right✝ : regEnv = env'
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok v) =
        Except.ok (r, env₂')
Tactic:
exists regEnv₂
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
left✝ : regR = r
right✝ : regEnv = env'
⊢ SSAEnv.equiv env' regEnv₂ ∧
    (match
        OpM.toTopM (TopM.mapDenoteRegion Δ regions)
          (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok v) =
      Except.ok (r, regEnv₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
left✝ : regR = r
right✝ : regEnv = env'
⊢ SSAEnv.equiv env' regEnv₂ ∧
    (match
        OpM.toTopM (TopM.mapDenoteRegion Δ regions)
          (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok v) =
      Except.ok (r, regEnv₂)
Tactic:
subst r env'
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
⊢ SSAEnv.equiv regEnv regEnv₂ ∧
    (match
        OpM.toTopM (TopM.mapDenoteRegion Δ regions)
          (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok v) =
      Except.ok (regR, regEnv₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
⊢ SSAEnv.equiv regEnv regEnv₂ ∧
    (match
        OpM.toTopM (TopM.mapDenoteRegion Δ regions)
          (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
      | Except.error err => Except.error err
      | Except.ok v => Except.ok v) =
      Except.ok (regR, regEnv₂)
Tactic:
simp [HregEnv₂]
State after:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
⊢ (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok v) =
    Except.ok (regR, regEnv₂)

State before:
case intro
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (regR, regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok (regR, regEnv₂)
⊢ (match
      OpM.toTopM (TopM.mapDenoteRegion Δ regions)
        (Semantics.semantics_op (IOp.mk op_name [] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok v) =
    Except.ok (regR, regEnv₂)
Tactic:
sorry
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
tailRes : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match headRes :: tailRes with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: tailRes) ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (headRes :: tailRes)) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match headRes :: tailRes 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 (headRes :: tailRes) ++ 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:
cases tailRes
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd [headRes]) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [headRes] 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 [headRes] ++ 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₂')

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match headRes :: head✝ :: tail✝ with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++
              toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) argRes (OpM.denoteRegions regions 0)
                attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match headRes :: head✝ :: tail✝ 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 (headRes :: head✝ :: tail✝) ++
                    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₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match headRes :: head✝ :: tail✝ with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++
              toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) argRes (OpM.denoteRegions regions 0)
                attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match headRes :: head✝ :: tail✝ 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 (headRes :: head✝ :: tail✝) ++
                    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 cons _ _ => simp at *; cases H
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd [headRes]) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [headRes] 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 [headRes] ++ 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 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
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match headRes :: head✝ :: tail✝ with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB
            (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++
              toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) (argRes, env).fst (OpM.denoteRegions regions 0)
          attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd (headRes :: head✝ :: tail✝)) argRes (OpM.denoteRegions regions 0)
                attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match headRes :: head✝ :: tail✝ 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 (headRes :: head✝ :: tail✝) ++
                    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:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
          attrs))
      env =
    Except.ok (regR, regEnv)
H :
  (match
      TopM.raiseUB
        (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++ toString "'")
        regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok (regR, v.snd)) =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
          attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
                attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++
                toString "'")
              v.snd with
          | Except.error err => Except.error err
          | Except.ok v_1 => Except.ok (v.fst, v_1.snd)) =
        Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes head✝ : TypedSSAVal Δ
tail✝ : List (TypedSSAVal Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
          attrs))
      env =
    Except.ok (regR, regEnv)
H :
  (match
      TopM.raiseUB
        (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++ toString "'")
        regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok (regR, v.snd)) =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
          attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (headRes.snd :: head✝.snd :: List.map Prod.snd tail✝) argRes (OpM.denoteRegions regions 0)
                attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 0 or 1 results, got '" ++ toString (headRes :: head✝ :: tail✝) ++
                toString "'")
              v.snd with
          | Except.error err => Except.error err
          | Except.ok v_1 => Except.ok (v.fst, v_1.snd)) =
        Except.ok (r, env₂')
Tactic:
cases H
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op
              (IOp.mk op_name (List.map Prod.snd [headRes]) argRes (OpM.denoteRegions regions 0) attrs))
            env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match [headRes] 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 [headRes] ++ 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:
simp
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regR : List (TypedArg Δ)
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (regR, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((regR, regEnv).fst, s)
      | [res] =>
        match (regR, regEnv).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, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (regR, regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((regR, regEnv).fst, v.snd))
      (regR, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (regR, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')
Tactic:
cases regR
State after:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok ([], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([], regEnv).fst, s)
      | [res] =>
        match ([], regEnv).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 (([], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([], regEnv).fst ++ toString "'") s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([], regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok (([], regEnv).fst, v.snd))
      ([], regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok ([], regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')

case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
head✝ : TypedArg Δ
tail✝ : List (TypedArg Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (head✝ :: tail✝, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((head✝ :: tail✝, regEnv).fst, s)
      | [res] =>
        match (head✝ :: tail✝, regEnv).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 ((head✝ :: tail✝, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (head✝ :: tail✝, regEnv).fst ++
                toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((head✝ :: tail✝, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((head✝ :: tail✝, regEnv).fst, v.snd))
      (head✝ :: tail✝, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (head✝ :: tail✝, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok ([], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([], regEnv).fst, s)
      | [res] =>
        match ([], regEnv).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 (([], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([], regEnv).fst ++ toString "'") s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([], regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok (([], regEnv).fst, v.snd))
      ([], regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok ([], regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')
Tactic:
case nil => simp at *; cases H
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
opRHead : TypedArg Δ
opRTail : List (TypedArg Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok (opRHead :: opRTail, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((opRHead :: opRTail, regEnv).fst, s)
      | [res] =>
        match (opRHead :: opRTail, regEnv).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 ((opRHead :: opRTail, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString (opRHead :: opRTail, regEnv).fst ++
                toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((opRHead :: opRTail, regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok ((opRHead :: opRTail, regEnv).fst, v.snd))
      (opRHead :: opRTail, regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok (opRHead :: opRTail, regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')
Tactic:
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
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      (argRes, env).snd =
    Except.ok ([], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([], regEnv).fst, s)
      | [res] =>
        match ([], regEnv).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 (([], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([], regEnv).fst ++ toString "'") s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([], regEnv).fst, v.snd)
      | x => fun s =>
        match
          TopM.raiseUB (toString "denoteOp: expected 0 or 1 results, got '" ++ toString [headRes] ++ toString "'")
            s with
        | Except.error err => Except.error err
        | Except.ok v => Except.ok (([], regEnv).fst, v.snd))
      ([], regEnv).snd =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op
        (IOp.mk op_name (List.map Prod.snd [headRes]) (argRes, env).fst (OpM.denoteRegions regions 0) attrs))
      env₂ =
    Except.ok ([], regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')
Tactic:
simp at *
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
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 Δ
regEnv : SSAEnv Δ
HRegInd :
  denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions) →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂',
              SSAEnv.equiv env' env₂' ∧ OpM.toTopM (TopM.mapDenoteRegion Δ regions) opM env₂ = Except.ok (res, env₂')
regEnv₂ : SSAEnv Δ
HregEnv₂ : SSAEnv.equiv regEnv regEnv₂
headRes : TypedSSAVal Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([], regEnv)
H :
  (match TopM.raiseUB (toString "denoteOp: expected 1 return value, got '" ++ toString [] ++ toString "'") regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ([], v.snd)) =
    Except.ok (r, env')
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok ([], regEnv₂)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match
          OpM.toTopM (TopM.mapDenoteRegion Δ regions)
            (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ with
        | Except.error err => Except.error err
        | Except.ok v =>
          (match v.fst with
            | [{ fst := τ, snd := v_1 }] => fun s =>
              match TopM.set τ headRes.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))
            v.snd) =
        Except.ok (r, env₂')