internlm/Lean-Github huggingface dataset:
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) Nat.zero args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
simp at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) 0 args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) 0 args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
specialize (H (by constructor) (by assumption))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H :
  ∃ env₂', SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ head args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) 0 args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H :
  ∃ env₂', SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ head args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) 0 args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ?m.2077032 ∈ head :: tail
Tactic:
constructor
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ head ?m.2077034 ?m.2077035 = Except.ok (?m.2077036, ?m.2077037)
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
specialize (HInd (by
  intros region Hregions args env res env' Hrun
  specialize (H (.tail _ Hregions) (by assumption))
  assumption
))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd :
  ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
      ∃ env₂',
        SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
          TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd :
  ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
      ∃ env₂',
        SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
          TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
apply (HInd Hrun)
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ denoteRegionsSetCommutesInvariant name τ v tail
Tactic:
intros region Hregions args env res env' Hrun
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ : SSAEnv Δ
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ : SSAEnv Δ
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
specialize (H (.tail _ Hregions) (by assumption))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ : SSAEnv Δ
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
H :
  ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ : SSAEnv Δ
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
H :
  ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧ region args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_set_commutes
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsSetCommutesInvariant name τ v tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx tail idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
H : denoteRegionsSetCommutesInvariant name τ v (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ : SSAEnv Δ
idx' : ℕ
Hrun✝ : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args✝ env✝ = Except.ok (res✝, env'✝)
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
Hregions : region ∈ tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : region args env = Except.ok (res, env')
⊢ region ?m.2077124 ?m.2077125 = Except.ok (?m.2077126, ?m.2077127)
Tactic:
assumption
Proof state after:
no goals
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
⊢ run
      (do
        ma
        mb)
      env =
    match run ma env with
    | Except.ok (PUnit.unit, env') => run mb env'
    | Except.error e => Except.error e
Tactic:
simp[run]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run mb p.snd) =
    match StateT.run ma env with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
⊢ (do
      let p ← StateT.run ma env
      StateT.run mb p.snd) =
    match StateT.run ma env with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
cases H : StateT.run ma env
Proof state after:
case error
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
a✝ : String × SSAEnv Δ
H : StateT.run ma env = Except.error a✝
⊢ (do
      let p ← Except.error a✝
      StateT.run mb p.snd) =
    match Except.error a✝ with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e

case ok
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
a✝ : Unit × SSAEnv Δ
H : StateT.run ma env = Except.ok a✝
⊢ (do
      let p ← Except.ok a✝
      StateT.run mb p.snd) =
    match Except.ok a✝ with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    match Except.error err with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
case error err => {
  simp[H];
  simp[bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
out : Unit × SSAEnv Δ
H : StateT.run ma env = Except.ok out
⊢ (do
      let p ← Except.ok out
      StateT.run mb p.snd) =
    match Except.ok out with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
case ok out => {
  simp[H, bind, Except.bind];
}
Proof state after:
no goals
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    match Except.error err with
    | Except.ok (PUnit.unit, env') => StateT.run mb env'
    | Except.error e => Except.error e
Tactic:
simp[H]
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    Except.error err
Theorem: run_seq
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
β : Type
Δ : Dialect α σ ε
ma : TopM Δ Unit
mb : TopM Δ β
env : SSAEnv Δ
err : String × SSAEnv Δ
H : StateT.run ma env = Except.error err
⊢ (do
      let p ← Except.error err
      StateT.run mb p.snd) =
    Except.error err
Tactic:
simp[bind, Except.bind]
Proof state after:
no goals