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

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 [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₂')
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 Δ
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:
cases opRTail
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 Δ
opRHead : 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], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([opRHead], regEnv).fst, s)
      | [res] =>
        match ([opRHead], 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], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([opRHead], regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([opRHead], 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], regEnv).fst, v.snd))
      ([opRHead], 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], 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 Δ
opRHead 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 (opRHead :: head✝ :: tail✝, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((opRHead :: head✝ :: tail✝, regEnv).fst, s)
      | [res] =>
        match (opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++
                  toString (opRHead :: head✝ :: tail✝, regEnv).fst ++
                toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd))
      (opRHead :: 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 (opRHead :: 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 Δ
opRHead 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 (opRHead :: head✝ :: tail✝, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((opRHead :: head✝ :: tail✝, regEnv).fst, s)
      | [res] =>
        match (opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++
                  toString (opRHead :: head✝ :: tail✝, regEnv).fst ++
                toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd))
      (opRHead :: 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 (opRHead :: 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₂')
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 Δ
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 Δ
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], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([opRHead], regEnv).fst, s)
      | [res] =>
        match ([opRHead], 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], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([opRHead], regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([opRHead], 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], regEnv).fst, v.snd))
      ([opRHead], 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], 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 *
    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 Δ
opRHead 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 (opRHead :: head✝ :: tail✝, regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok ((opRHead :: head✝ :: tail✝, regEnv).fst, s)
      | [res] =>
        match (opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++
                  toString (opRHead :: head✝ :: tail✝, regEnv).fst ++
                toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok ((opRHead :: 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 ((opRHead :: head✝ :: tail✝, regEnv).fst, v.snd))
      (opRHead :: 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 (opRHead :: 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₂')
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 Δ
opRHead head✝ : TypedArg Δ
tail✝ : List (TypedArg Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (opRHead :: head✝ :: tail✝, regEnv)
H :
  (match
      TopM.raiseUB
        (toString "denoteOp: expected 1 return value, got '" ++ toString (opRHead :: head✝ :: tail✝) ++ toString "'")
        regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok (opRHead :: head✝ :: tail✝, 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 (opRHead :: 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 Δ
opRHead head✝ : TypedArg Δ
tail✝ : List (TypedArg Δ)
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok (opRHead :: head✝ :: tail✝, regEnv)
H :
  (match
      TopM.raiseUB
        (toString "denoteOp: expected 1 return value, got '" ++ toString (opRHead :: head✝ :: tail✝) ++ toString "'")
        regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok (opRHead :: head✝ :: tail✝, 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 (opRHead :: 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₂')
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 Δ
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 Δ
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], regEnv)
H :
  (match [headRes] with
      | [] => fun s => Except.ok (([opRHead], regEnv).fst, s)
      | [res] =>
        match ([opRHead], 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], regEnv).fst, v.snd)
        | x => fun s =>
          match
            TopM.raiseUB
              (toString "denoteOp: expected 1 return value, got '" ++ toString ([opRHead], regEnv).fst ++ toString "'")
              s with
          | Except.error err => Except.error err
          | Except.ok v => Except.ok (([opRHead], 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], regEnv).fst, v.snd))
      ([opRHead], 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], 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 Δ
opRHead : TypedArg Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
H :
  (match TopM.set opRHead.fst headRes.fst opRHead.snd regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ([opRHead], 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 ([opRHead], 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 Δ
opRHead : TypedArg Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
H :
  (match TopM.set opRHead.fst headRes.fst opRHead.snd regEnv with
    | Except.error err => Except.error err
    | Except.ok v => Except.ok ([opRHead], 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 ([opRHead], 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:
split at H <;> try contradiction
State after:
case h_2
α₁ σ₁ : 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 Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok ([opRHead], regEnv₂)
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
v✝ : Unit × SSAEnv Δ
heq✝ : TopM.set opRHead.fst headRes.fst opRHead.snd regEnv = Except.ok v✝
H : Except.ok ([opRHead], v✝.snd) = Except.ok (r, env')
⊢ ∃ 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 Δ
opRHead : TypedArg Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok ([opRHead], regEnv₂)
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
setRes : Unit × SSAEnv Δ
HSetRes : TopM.set opRHead.fst headRes.fst opRHead.snd regEnv = Except.ok setRes
H : Except.ok ([opRHead], setRes.snd) = Except.ok (r, env')
⊢ ∃ 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 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
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 Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok ([opRHead], regEnv₂)
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
err✝ : String × SSAEnv Δ
heq✝ : TopM.set opRHead.fst headRes.fst opRHead.snd regEnv = 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 [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:
contradiction
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 Δ
HregR :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env =
    Except.ok ([opRHead], regEnv)
HregR₂ :
  OpM.toTopM (TopM.mapDenoteRegion Δ regions)
      (Semantics.semantics_op (IOp.mk op_name [headRes.snd] argRes (OpM.denoteRegions regions 0) attrs)) env₂ =
    Except.ok ([opRHead], regEnv₂)
x✝ : Except (String × SSAEnv Δ) (Unit × SSAEnv Δ)
setRes : Unit × SSAEnv Δ
HSetRes : TopM.set opRHead.fst headRes.fst opRHead.snd regEnv = Except.ok setRes
H : Except.ok ([opRHead], setRes.snd) = Except.ok (r, env')
⊢ ∃ 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:
sorry
State after:
no goals