internlm/Lean-Github huggingface dataset:
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
have ⟨env₂', Henv₂', HIx⟩ := denoteRegionByIx_equiv regions Hregs HReg Henv₂
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
specialize (HInd resReg (by assumption) (by assumption))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧
      (match TopM.denoteRegionsByIx regions idx args env₂ with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂')
Tactic:
rw [HIx]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1,
    SSAEnv.equiv env' env₂'_1 ∧
      (match Except.ok (resReg, env₂') with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂'_1)
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1,
    SSAEnv.equiv env' env₂'_1 ∧
      (match Except.ok (resReg, env₂') with
        | Except.error err => Except.error err
        | Except.ok v => toTopM regions (continuation v.fst) v.snd) =
        Except.ok (res, env₂'_1)
Tactic:
simp
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
HInd : ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
⊢ ∃ env₂'_1, SSAEnv.equiv env' env₂'_1 ∧ toTopM regions (continuation resReg) env₂' = Except.ok (res, env₂'_1)
Tactic:
assumption
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ toTopM regions (continuation resReg) ?m.1084400 = Except.ok (?m.1084401, ?m.1084402)
Tactic:
assumption
Proof state after:
no goals
Theorem: OpM.toTopM_regions_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
idx : ℕ
args : TypedArgs Δ
continuation : TypedArgs Δ → OpM Δ (TypedArgs Δ)
HInd :
  ∀ (a : TypedArgs Δ) ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions (continuation a) env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions (continuation a) env₂ = Except.ok (res, env₂')
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
resReg : TypedArgs Δ
envReg : SSAEnv Δ
H : toTopM regions (continuation resReg) envReg = Except.ok (res, env')
HReg : TopM.denoteRegionsByIx regions idx args env = Except.ok (resReg, envReg)
env₂' : SSAEnv Δ
Henv₂' : SSAEnv.equiv envReg env₂'
HIx : TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (resReg, env₂')
⊢ SSAEnv.equiv envReg ?m.1084404
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteOp_equiv
Proof 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
Proof state after:
no goals
Theorem: denoteOp_equiv
Proof 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
Proof state after:
no goals
Theorem: denoteOp_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
op_name : String
res args : List (TypedSSAVal Δ)
regions : List (Region Δ)
attrs : AttrDict Δ
env : SSAEnv Δ
r : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
x✝¹ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
argsRes : List (TypedArg Δ) × SSAEnv Δ
argRes : List (TypedArg Δ)
HargsRes : denoteOpArgs Δ args env = Except.ok (argRes, env)
x✝ : Except (String × SSAEnv Δ) (List (TypedArg Δ) × SSAEnv Δ)
regR✝ : List (TypedArg Δ) × SSAEnv Δ
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
Proof state after:
no goals
Theorem: denoteOp_equiv
Proof 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
Proof state after:
no goals