internlm/Lean-Github huggingface dataset:
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case beta
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : e = VExpr.sort u ∨ e = VExpr.sort u → VLevel.WF U u
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
eq : app (lam A✝ e) e'✝ = VExpr.sort u ∨ inst e e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case beta.inr
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : e = VExpr.sort u ∨ e = VExpr.sort u → VLevel.WF U u
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
eq : inst e e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case beta.inr
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
e B✝ e'✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) e e B✝
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : e = VExpr.sort u ∨ e = VExpr.sort u → VLevel.WF U u
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
eq : inst e e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
cases e with
| bvar i =>
  cases i with simp [inst] at eq
  | zero => exact ih2 (.inl eq)
| _ => cases eq <;> exact ih1 (.inl rfl)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case beta.inr.bvar
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
i : Nat
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar i) (VExpr.bvar i) B✝
ih1 : VExpr.bvar i = VExpr.sort u ∨ VExpr.bvar i = VExpr.sort u → VLevel.WF U u
eq : inst (VExpr.bvar i) e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
cases i with simp [inst] at eq
| zero => exact ih2 (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case beta.inr.bvar.zero
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.bvar Nat.zero) (VExpr.bvar Nat.zero) B✝
ih1 : VExpr.bvar Nat.zero = VExpr.sort u ∨ VExpr.bvar Nat.zero = VExpr.sort u → VLevel.WF U u
eq : e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
exact ih2 (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case beta.inr.forallE
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
A✝ : VExpr
Γ✝ : List VExpr
B✝ e'✝ : VExpr
a✝ : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih2 : e'✝ = VExpr.sort u ∨ e'✝ = VExpr.sort u → VLevel.WF U u
binderType✝ body✝ : VExpr
h1 : IsDefEq env U (A✝ :: Γ✝) (VExpr.forallE binderType✝ body✝) (VExpr.forallE binderType✝ body✝) B✝
ih1 : VExpr.forallE binderType✝ body✝ = VExpr.sort u ∨ VExpr.forallE binderType✝ body✝ = VExpr.sort u → VLevel.WF U u
eq : inst (VExpr.forallE binderType✝ body✝) e'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
cases eq <;> exact ih1 (.inl rfl)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case eta
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : e✝ = VExpr.sort u ∨ e✝ = VExpr.sort u → VLevel.WF U u
eq : lam A✝ (app (lift e✝) (VExpr.bvar 0)) = VExpr.sort u ∨ e✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
obtain ⟨⟨⟩⟩ | eq := eq
Proof state after:
case eta.inr
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : e✝ = VExpr.sort u ∨ e✝ = VExpr.sort u → VLevel.WF U u
eq : e✝ = VExpr.sort u
⊢ VLevel.WF U u
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case eta.inr
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
e✝ A✝ B✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e✝ (VExpr.forallE A✝ B✝)
ih : e✝ = VExpr.sort u ∨ e✝ = VExpr.sort u → VLevel.WF U u
eq : e✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
exact ih (.inl eq)
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case extra
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
suffices ∀ e, VExpr.instL ls e = .sort u → HasType env df.uvars [] e df.type → u.WF U by
  have ⟨A1, A2⟩ := henv.defEqWF h1
  cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
case extra
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
⊢ ∀ (e : VExpr), VExpr.instL ls e = VExpr.sort u → HasType env df.uvars [] e df.type → VLevel.WF U u
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case extra
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
⊢ ∀ (e : VExpr), VExpr.instL ls e = VExpr.sort u → HasType env df.uvars [] e df.type → VLevel.WF U u
Tactic:
intro e eq IH
Proof state after:
case extra
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq✝ : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
e : VExpr
eq : VExpr.instL ls e = VExpr.sort u
IH : HasType env df.uvars [] e df.type
⊢ VLevel.WF U u
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case extra
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq✝ : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
e : VExpr
eq : VExpr.instL ls e = VExpr.sort u
IH : HasType env df.uvars [] e df.type
⊢ VLevel.WF U u
Tactic:
cases e <;> cases eq
Proof state after:
case extra.sort.refl
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
u✝ : VLevel
IH : HasType env df.uvars [] (VExpr.sort u✝) df.type
eq : VExpr.instL ls df.lhs = VExpr.sort (VLevel.inst ls u✝) ∨ VExpr.instL ls df.rhs = VExpr.sort (VLevel.inst ls u✝)
⊢ VLevel.WF U (VLevel.inst ls u✝)
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case extra.sort.refl
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
u✝ : VLevel
IH : HasType env df.uvars [] (VExpr.sort u✝) df.type
eq : VExpr.instL ls df.lhs = VExpr.sort (VLevel.inst ls u✝) ∨ VExpr.instL ls df.rhs = VExpr.sort (VLevel.inst ls u✝)
⊢ VLevel.WF U (VLevel.inst ls u✝)
Tactic:
rename_i u
Proof state after:
case extra.sort.refl
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
u : VLevel
IH : HasType env df.uvars [] (VExpr.sort u) df.type
eq : VExpr.instL ls df.lhs = VExpr.sort (VLevel.inst ls u) ∨ VExpr.instL ls df.rhs = VExpr.sort (VLevel.inst ls u)
⊢ VLevel.WF U (VLevel.inst ls u)
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case extra.sort.refl
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
u : VLevel
IH : HasType env df.uvars [] (VExpr.sort u) df.type
eq : VExpr.instL ls df.lhs = VExpr.sort (VLevel.inst ls u) ∨ VExpr.instL ls df.rhs = VExpr.sort (VLevel.inst ls u)
⊢ VLevel.WF U (VLevel.inst ls u)
Tactic:
exact VLevel.WF.inst h2
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
this : ∀ (e : VExpr), VExpr.instL ls e = VExpr.sort u → HasType env df.uvars [] e df.type → VLevel.WF U u
⊢ VLevel.WF U u
Tactic:
have ⟨A1, A2⟩ := henv.defEqWF h1
Proof state after:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
this : ∀ (e : VExpr), VExpr.instL ls e = VExpr.sort u → HasType env df.uvars [] e df.type → VLevel.WF U u
A1 : HasType env df.uvars [] df.lhs df.type
A2 : HasType env df.uvars [] df.rhs df.type
⊢ VLevel.WF U u
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
df : VDefEq
ls : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df
h2 : ∀ (l : VLevel), l ∈ ls → VLevel.WF U l
a✝ : List.length ls = df.uvars
eq : VExpr.instL ls df.lhs = VExpr.sort u ∨ VExpr.instL ls df.rhs = VExpr.sort u
this : ∀ (e : VExpr), VExpr.instL ls e = VExpr.sort u → HasType env df.uvars [] e df.type → VLevel.WF U u
A1 : HasType env df.uvars [] df.lhs df.type
A2 : HasType env df.uvars [] df.rhs df.type
⊢ VLevel.WF U u
Tactic:
cases eq <;> exact this _ ‹_› ‹_›
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.sort_inv'
Proof state before:
case forallEDF
env : VEnv
henv : Ordered env
U : Nat
Γ : List VExpr
e1 e2 V : VExpr
u : VLevel
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
a✝¹ : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
a_ih✝¹ : A✝ = VExpr.sort u ∨ A'✝ = VExpr.sort u → VLevel.WF U u
a_ih✝ : body✝ = VExpr.sort u ∨ body'✝ = VExpr.sort u → VLevel.WF U u
eq : VExpr.forallE A✝ body✝ = VExpr.sort u ∨ VExpr.forallE A'✝ body'✝ = VExpr.sort u
⊢ VLevel.WF U u
Tactic:
nomatch eq
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
hΓ : OnCtx Γ (IsType env U)
H : IsDefEq env U Γ e1 e2 A
⊢ IsType env U Γ A
Tactic:
induction H with
| bvar h => exact .lookup henv hΓ  h
| proofIrrel h1 => exact ⟨_, h1⟩
| extra h1 h2 =>
  have ⟨_, _, _, h⟩ := envIH.2 h1
  exact ⟨_, (h.instL h2).weak0 henv⟩
| sortDF h1 => exact ⟨_, .sort h1⟩
| constDF h1 h2 =>
  let ⟨_, h, _⟩ := envIH.1 h1
  exact ⟨_, (h.instL h2).weak0 henv⟩
| symm _ ih => exact ih hΓ
| trans _ _ ih1 => exact ih1 hΓ
| appDF _ h2 ih1 => exact ((ih1 hΓ).forallE_inv henv).2.instN henv .zero h2.hasType.1
| lamDF h1 _ _ ih2 =>
  let ⟨_, h⟩ := ih2 ⟨hΓ, _, h1.hasType.1⟩
  exact ⟨_, .forallE h1.hasType.1 h⟩
| forallEDF h1 _ ih1 ih2 =>
  exact ⟨_, .sort ⟨(ih1 hΓ).sort_inv henv, (ih2 ⟨hΓ, _, h1.hasType.1⟩).sort_inv henv⟩⟩
| defeqDF h1 => exact ⟨_, h1.hasType.2⟩
| beta _ h2 ih1 ih2 =>
  have ⟨_, h⟩ := ih2 hΓ
  exact (ih1 ⟨hΓ, _, h.hasType.2⟩).instN henv .zero h2
| eta _ ih => exact ih hΓ
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case bvar
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
i✝ : Nat
A✝ : VExpr
h : Lookup Γ✝ i✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ A✝
Tactic:
exact .lookup henv hΓ  h
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case proofIrrel
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
p✝ h✝ h'✝ : VExpr
h1 : IsDefEq env U Γ✝ p✝ p✝ (VExpr.sort VLevel.zero)
a✝¹ : IsDefEq env U Γ✝ h✝ h✝ p✝
a✝ : IsDefEq env U Γ✝ h'✝ h'✝ p✝
a_ih✝² : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort VLevel.zero)
a_ih✝¹ a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ p✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ p✝
Tactic:
exact ⟨_, h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ df✝.type)
Tactic:
have ⟨_, _, _, h⟩ := envIH.2 h1
Proof state after:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : OnCtx Γ✝ (IsType env U)
left✝¹ : (fun U e A => HasType env U [] e A ∧ IsType env U [] A) df✝.uvars df✝.lhs df✝.type
left✝ : HasType env df✝.uvars [] df✝.rhs df✝.type
w✝ : VLevel
h : HasType env df✝.uvars [] df✝.type (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ df✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case extra
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
df✝ : VDefEq
ls✝ : List VLevel
Γ✝ : List VExpr
h1 : env.defeqs df✝
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝ : List.length ls✝ = df✝.uvars
hΓ : OnCtx Γ✝ (IsType env U)
left✝¹ : (fun U e A => HasType env U [] e A ∧ IsType env U [] A) df✝.uvars df✝.lhs df✝.type
left✝ : HasType env df✝.uvars [] df✝.rhs df✝.type
w✝ : VLevel
h : HasType env df✝.uvars [] df✝.type (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ df✝.type)
Tactic:
exact ⟨_, (h.instL h2).weak0 henv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case sortDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
l✝ l'✝ : VLevel
Γ✝ : List VExpr
h1 : VLevel.WF U l✝
a✝¹ : VLevel.WF U l'✝
a✝ : l✝ ≈ l'✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (VExpr.sort (VLevel.succ l✝))
Tactic:
exact ⟨_, .sort h1⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ ci✝.type)
Tactic:
let ⟨_, h, _⟩ := envIH.1 h1
Proof state after:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env ci✝.uvars [] ci✝.type (VExpr.sort w✝)
right✝ : IsType env ci✝.uvars [] (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ ci✝.type)
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case constDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
c✝ : Name
ci✝ : VConstant
ls✝ ls'✝ : List VLevel
Γ✝ : List VExpr
h1 : env.constants c✝ = some (some ci✝)
h2 : ∀ (l : VLevel), l ∈ ls✝ → VLevel.WF U l
a✝² : ∀ (l : VLevel), l ∈ ls'✝ → VLevel.WF U l
a✝¹ : List.length ls✝ = ci✝.uvars
a✝ : List.Forall₂ (fun x x_1 => x ≈ x_1) ls✝ ls'✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env ci✝.uvars [] ci✝.type (VExpr.sort w✝)
right✝ : IsType env ci✝.uvars [] (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.instL ls✝ ci✝.type)
Tactic:
exact ⟨_, (h.instL h2).weak0 henv⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case symm
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e✝ e'✝ A✝ : VExpr
a✝ : IsDefEq env U Γ✝ e✝ e'✝ A✝
ih : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ A✝
Tactic:
exact ih hΓ
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case trans
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
e₁✝ e₂✝ A✝ e₃✝ : VExpr
a✝¹ : IsDefEq env U Γ✝ e₁✝ e₂✝ A✝
a✝ : IsDefEq env U Γ✝ e₂✝ e₃✝ A✝
ih1 a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ A✝
Tactic:
exact ih1 hΓ
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case appDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
f✝ f'✝ A✝ B✝ a✝¹ a'✝ : VExpr
a✝ : IsDefEq env U Γ✝ f✝ f'✝ (VExpr.forallE A✝ B✝)
h2 : IsDefEq env U Γ✝ a✝¹ a'✝ A✝
ih1 : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.forallE A✝ B✝)
a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (inst B✝ a✝¹)
Tactic:
exact ((ih1 hΓ).forallE_inv henv).2.instN henv .zero h2.hasType.1
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (VExpr.forallE A✝ B✝)
Tactic:
let ⟨_, h⟩ := ih2 ⟨hΓ, _, h1.hasType.1⟩
Proof state after:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U (A✝ :: Γ✝) B✝ (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.forallE A✝ B✝)
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case lamDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ B✝ : VExpr
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ B✝
a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U (A✝ :: Γ✝) B✝ (VExpr.sort w✝)
⊢ IsType env U Γ✝ (VExpr.forallE A✝ B✝)
Tactic:
exact ⟨_, .forallE h1.hasType.1 h⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case forallEDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ A'✝ : VExpr
u✝ : VLevel
body✝ body'✝ : VExpr
v✝ : VLevel
h1 : IsDefEq env U Γ✝ A✝ A'✝ (VExpr.sort u✝)
a✝ : IsDefEq env U (A✝ :: Γ✝) body✝ body'✝ (VExpr.sort v✝)
ih1 : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort u✝)
ih2 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) (VExpr.sort v✝)
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (VExpr.sort (VLevel.imax u✝ v✝))
Tactic:
exact ⟨_, .sort ⟨(ih1 hΓ).sort_inv henv, (ih2 ⟨hΓ, _, h1.hasType.1⟩).sort_inv henv⟩⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case defeqDF
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A : VExpr
Γ✝ : List VExpr
A✝ B✝ : VExpr
u✝ : VLevel
e1✝ e2✝ : VExpr
h1 : IsDefEq env U Γ✝ A✝ B✝ (VExpr.sort u✝)
a✝ : IsDefEq env U Γ✝ e1✝ e2✝ A✝
a_ih✝¹ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ (VExpr.sort u✝)
a_ih✝ : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ B✝
Tactic:
exact ⟨_, h1.hasType.2⟩
Proof state after:
no goals
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
ih2 : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
⊢ IsType env U Γ✝ (inst B✝ e'✝)
Tactic:
have ⟨_, h⟩ := ih2 hΓ
Proof state after:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
ih2 : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ IsType env U Γ✝ (inst B✝ e'✝)
Theorem: Lean4Lean.VEnv.IsDefEq.isType'
Proof state before:
case beta
env : VEnv
henv : Ordered env
envIH : OnTypes env fun U e A => HasType env U [] e A ∧ IsType env U [] A
Γ : List VExpr
U : Nat
e1 e2 A A✝ : VExpr
Γ✝ : List VExpr
e✝ B✝ e'✝ : VExpr
a✝ : IsDefEq env U (A✝ :: Γ✝) e✝ e✝ B✝
h2 : IsDefEq env U Γ✝ e'✝ e'✝ A✝
ih1 : OnCtx (A✝ :: Γ✝) (IsType env U) → IsType env U (A✝ :: Γ✝) B✝
ih2 : OnCtx Γ✝ (IsType env U) → IsType env U Γ✝ A✝
hΓ : OnCtx Γ✝ (IsType env U)
w✝ : VLevel
h : HasType env U Γ✝ A✝ (VExpr.sort w✝)
⊢ IsType env U Γ✝ (inst B✝ e'✝)
Tactic:
exact (ih1 ⟨hΓ, _, h.hasType.2⟩).instN henv .zero h2
Proof state after:
no goals