internlm/Lean-Github huggingface dataset:
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : pure () env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁' env₂ ∧ pure () env₂ = Except.ok (r, env₂)
Tactic:
simp_monad at *
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
H : env₁ = env₁'
⊢ SSAEnv.equiv env₁' env₂
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
H : env₁ = env₁'
⊢ SSAEnv.equiv env₁' env₂
Tactic:
subst H
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ SSAEnv.equiv env₁ env₂
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
val : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ 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₂')
⊢ ∀ ⦃vals : List SSAVal⦄ ⦃env₁ : SSAEnv Δ⦄ ⦃r : Unit⦄ ⦃env₁' : SSAEnv Δ⦄,
    denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁') →
      ∀ ⦃env₂ : SSAEnv Δ⦄,
        SSAEnv.equiv env₁ env₂ →
          ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
intros vals env₁ r env₁' H env₂ Henv₂
Proof state after:
α₁ σ₁ : 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₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
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₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
have ⟨valsHead, valsTail, HVals, HHead, HTail⟩ := denoteTypedArgs_cons_args H
Proof state after:
α₁ σ₁ : 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₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HVals : vals = valsHead :: valsTail
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₁')
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
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₂')
vals : List SSAVal
env₁ : SSAEnv Δ
r : Unit
env₁' : SSAEnv Δ
H : denoteTypedArgs (argsHead :: argsTail) vals env₁ = Except.ok (r, env₁')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env₁ env₂
valsHead : SSAVal
valsTail : List SSAVal
HVals : vals = valsHead :: valsTail
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₁')
⊢ ∃ env₂', SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) vals env₂ = Except.ok (r, env₂')
Tactic:
subst vals
Proof state after:
α₁ σ₁ : 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₁')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
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₁')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
have HHead₂ := TopM.set_equiv Henv₂ HHead
Proof state after:
α₁ σ₁ : 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₂)
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
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₂)
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
specialize (HInd HTail (by apply SSAEnv.equiv_set Henv₂))
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
HInd :
  ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧
      denoteTypedArgs argsTail valsTail (SSAEnv.set valsHead argsHead.fst argsHead.snd env₂) = Except.ok ((), env₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
have ⟨env₂', Hequiv₂', Henv₂'⟩ := HInd
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
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₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
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₂')
⊢ ∃ env₂',
    SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
exists env₂'
Proof state after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
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₂')
⊢ SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Theorem: denoteTypedArgs_equiv
Proof state before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
argsHead : TypedArg Δ
argsTail : List (TypedArg Δ)
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₂)
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₂')
⊢ SSAEnv.equiv env₁' env₂' ∧ denoteTypedArgs (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (r, env₂')
Tactic:
cases r
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 (argsHead :: argsTail) (valsHead :: valsTail) 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 (argsHead :: argsTail) (valsHead :: valsTail) env₂ = Except.ok (PUnit.unit, env₂')
Tactic:
rw [denoteTypedArgs_cons_unfold]
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₂' ∧
    bind (TopM.set argsHead.fst valsHead argsHead.snd) (fun x => denoteTypedArgs argsTail valsTail) env₂ =
      Except.ok (PUnit.unit, env₂')