internlm/Lean-Github huggingface dataset:
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    bind (TopM.set argsHead.fst valsHead argsHead.snd) (fun x => denoteTypedArgs argsTail valsTail) env₂ =
      Except.ok (PUnit.unit, env₂')
Tactic:
simp_monad
Proof state after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match TopM.set argsHead.fst valsHead argsHead.snd env₂ with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match TopM.set argsHead.fst valsHead argsHead.snd env₂ with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Tactic:
rw [HHead₂]
Proof state after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    (match Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) with
      | Except.error err => Except.error err
      | Except.ok v => denoteTypedArgs argsTail valsTail v.snd) =
      Except.ok (PUnit.unit, env₂')
Tactic:
simp
Proof state after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) =
      Except.ok (PUnit.unit, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧
    denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) =
      Except.ok (PUnit.unit, env₂')
Tactic:
rw [Henv₂']
Proof state after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧ Except.ok ((), env₂') = Except.ok (PUnit.unit, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂' ∧ Except.ok ((), env₂') = Except.ok (PUnit.unit, env₂')
Tactic:
simp
Proof state after:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂'
Theorem: denoteTypedArgs_equiv
Proof state before:
case unit
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
env₁ env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
env₂' : SSAEnv Δ
Hequiv₂' : SSAEnv.equiv env₁' env₂'
Henv₂' : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (PUnit.unit, env₁')
⊢ SSAEnv.equiv env₁' env₂'
Tactic:
assumption
Proof state after:
no goals
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
HInd :
  ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs argsTail vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs argsTail vals env₂ = Except.ok (r, env₂')
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HHead :
  TopM.set argsHead.fst valsHead argsHead.snd env₁ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₁)
HTail : denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) = Except.ok ((), env₁')
H : denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₁ = Except.ok (r, env₁')
HHead₂ :
  TopM.set argsHead.fst valsHead argsHead.snd env₂ = Except.ok ((), SSAEnv.set valsHead argsHead.fst argsHead.snd env₂)
⊢ SSAEnv.equiv (SSAEnv.set valsHead argsHead.fst argsHead.snd env₁) ?m.958985
Tactic:
apply SSAEnv.equiv_set Henv₂
Proof state after:
no goals
Theorem: denoteRegionByIx_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
regions : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
⊢ denoteRegionsEquivInvariant regions →
    ∀ ⦃idx : ℕ⦄ ⦃args : TypedArgs Δ⦄ ⦃env : SSAEnv Δ⦄ ⦃res : TypedArgs Δ⦄ ⦃env' : SSAEnv Δ⦄,
      TopM.denoteRegionsByIx regions idx args env = Except.ok (res, env') →
        ∀ ⦃env₂ : SSAEnv Δ⦄,
          SSAEnv.equiv env env₂ →
            ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx regions idx args env₂ = Except.ok (res, env₂')
Tactic:
induction regions <;> intros H idx args env res env' Hrun env₂ Henv₂ <;> try contradiction
Proof state after:
case cons
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
head✝ : TypedArgs Δ → TopM Δ (TypedArgs Δ)
tail✝ : List (TypedArgs Δ → TopM Δ (TypedArgs Δ))
tail_ih✝ :
  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✝)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head✝ :: tail✝) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head✝ :: tail✝) 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 Δ))
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)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) idx args env₂ = Except.ok (res, env₂')
Tactic:
case cons head tail HInd =>
  cases idx
  case zero =>
    simp at *
    specialize (H (by constructor) (by assumption) (by assumption))
    assumption
  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:
case nil
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
H : denoteRegionsEquivInvariant []
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx [] idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx [] idx args env₂ = Except.ok (res, env₂')
Tactic:
contradiction
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)
idx : ℕ
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
Hrun : TopM.denoteRegionsByIx (head :: tail) idx args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) idx args env₂ = Except.ok (res, env₂')
Tactic:
cases idx
Proof state after:
case zero
α₁ σ₁ : 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₂')

case succ
α₁ σ₁ : 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₂
n✝ : ℕ
Hrun : TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) args env = Except.ok (res, env')
⊢ ∃ env₂',
    SSAEnv.equiv env' env₂' ∧ TopM.denoteRegionsByIx (head :: tail) (Nat.succ n✝) 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) 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:
case zero =>
  simp at *
  specialize (H (by constructor) (by assumption) (by assumption))
  assumption
Proof state after:
no goals