internlm/Lean-Github huggingface dataset:
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
case succ idx' =>
  specialize (HInd (by
    intros region Hregions args env res env' Hrun env₂ Henv₂
    specialize (H (.tail _ Hregions) (by assumption) (by assumption))
    assumption
  ))
  simp at Hrun
  specialize (HInd Hrun Henv₂)
  assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) Nat.zero args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) Nat.zero args env₂ = Except.ok (res, env₂')
Tactic:
simp at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Tactic:
specialize (H (by constructor) (by assumption) (by assumption))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ head args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ head args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) 0 args env₂ = Except.ok (res, env₂')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ ?m.1012060 ∈ head :: tail
Tactic:
constructor
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ head ?m.1012062 ?m.1012063 = Except.ok (?m.1012064, ?m.1012065)
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
Hrun : TopM.denoteRegionsByIx (head :: tail) 0 args env = Except.ok (res, env')
⊢ SSAEnv.equiv env ?m.1012067
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
specialize (HInd (by
  intros region Hregions args env res env' Hrun env₂ Henv₂
  specialize (H (.tail _ Hregions) (by assumption) (by assumption))
  assumption
))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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 Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
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 Δ⦄,
        SSAEnv.equiv env env₂ →
          ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
specialize (HInd Hrun Henv₂)
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd : ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx' args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
HInd : ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx' args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env₂ = Except.ok (res, env₂')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
idx' : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ idx') args env = Except.ok (res, env')
⊢ denoteRegionsEquivInvariant tail
Tactic:
intros region Hregions args env res env' Hrun env₂ Henv₂
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
specialize (H (.tail _ Hregions) (by assumption) (by assumption))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
H : ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ region ?m.1012165 ?m.1012166 = Except.ok (?m.1012167, ?m.1012168)
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
HInd :
  denoteRegionsEquivInvariant tail →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx tail idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx tail idx args env₂ = Except.ok (res, env₂')
H : denoteRegionsEquivInvariant (head :: tail)
args✝ : TypedArgs Δ
env✝ : SSAEnv Δ
res✝ : TypedArgs Δ
env'✝ env₂✝ : SSAEnv Δ
Henv₂✝ : SSAEnv.equiv env✝ env₂✝
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 Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ SSAEnv.equiv env ?m.1012170
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 Δ))
⊢ denoteRegionsEquivInvariant regions →
    ∀ ⦃opM : OpM Δ (TypedArgs Δ)⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      toTopM regions opM env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions opM env₂ = Except.ok (res, env₂')
Tactic:
intros Hregs opM
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
Hregs : denoteRegionsEquivInvariant regions
opM : OpM Δ (TypedArgs Δ)
⊢ ∀ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
    toTopM regions opM env = Except.ok (res, env') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env env₂ → ∃ env₂', SSAEnv.equiv env' env₂' ∧ toTopM regions opM env₂ = Except.ok (res, env₂')