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

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ denoteRegionsSetCommutesInvariant name τ v regions →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx regions idx args env = Except.ok (res, env') →
        ∃ env₂',
          SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
            TopM.denoteRegionsByIx regions idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
induction regions <;> intros H idx args env res env' Hrun <;> try contradiction
State after:
case cons
α₁ σ₁ : 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 Δ))
tail_ih✝ :
  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✝)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head✝ :: tail✝) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head✝ :: tail✝) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')

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)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
case cons head tail HInd =>
  cases idx
  case zero =>
    simp at *
    specialize (H (by constructor) (by assumption))
    assumption
  case succ idx' =>
    specialize (HInd (by
      intros region Hregions args env res env' Hrun
      specialize (H (.tail _ Hregions) (by assumption))
      assumption
    ))
    simp at Hrun
    apply (HInd Hrun)
State after:
no goals

State before:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
name : SSAVal
τ : MLIRType Δ
v : MLIRType.eval τ
H : denoteRegionsSetCommutesInvariant name τ v []
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx [] idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx [] idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
contradiction
State after:
no goals

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)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) idx args (SSAEnv.set name τ v env) = Except.ok (res, env₂')
Tactic:
cases idx
State after:
case zero
α₁ σ₁ : 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₂')

case succ
α₁ σ₁ : 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 Δ
n✝ : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv (SSAEnv.set name τ v env') env₂' ∧
      TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args (SSAEnv.set name τ v env) = Except.ok (res, env₂')

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:
case zero =>
  simp at *
  specialize (H (by constructor) (by assumption))
  assumption
State after:
no goals

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:
case succ idx' =>
  specialize (HInd (by
    intros region Hregions args env res env' Hrun
    specialize (H (.tail _ Hregions) (by assumption))
    assumption
  ))
  simp at Hrun
  apply (HInd Hrun)
State after:
no goals

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

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

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

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

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

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

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

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

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

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

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